5 citations · 8 across the 3 of their papers we have counts for
4 papers
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Sebastian Ullrich, Leonardo de Moura
In interactive theorem provers (ITPs), extensible syntax is not only crucial to lower the cognitive burden of manipulating complex mathematical objects, but plays a critical role i…
Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming
Sebastian Ullrich, Leonardo de Moura
Most functional languages rely on some garbage collection for automatic memory management. They usually eschew reference counting in favor of a tracing garbage collector, which has…
Congruence Closure in Intensional Type Theory
Daniel Selsam, Leonardo de Moura
Congruence closure procedures are used extensively in automated reasoning and are a core component of most satisfiability modulo theories solvers. However, no known congruence clos…
Elaboration in Dependent Type Theory
Leonardo de Moura, Jeremy Avigad, Soonho Kong +1
To be usable in practice, interactive theorem provers need to provide convenient and efficient means of writing expressions, definitions, and proofs. This involves inferring inform…