1 citations · 1 across the 3 of their papers we have counts for
3 papers
cs.PL2024
Free Foil: Generating Efficient and Scope-Safe Abstract Syntax
Nikolai Kudasov, Renata Shakirova, Egor Shalagin +1
Handling bound identifiers correctly and efficiently is critical in implementations of compilers, proof assistants, and theorem provers. When choosing a representation for abstract…
cs.LO2023★ 1 cited
E-unification for Second-Order Abstract Syntax
Nikolai Kudasov
Higher-order unification (HOU) concerns unification of (extensions of) -calculus and can be seen as an instance of equational unification (-unification) modulo -equivalen…
cs.LO2022
Free Monads, Intrinsic Scoping, and Higher-Order Preunification
Nikolai Kudasov
Type checking algorithms and theorem provers rely on unification algorithms. In presence of type families or higher-order logic, higher-order (pre)unification (HOU) is required. Ma…