1 citations · 4 across the 10 of their papers we have counts for
5 papers · 1 filter
Implementing Dependent Type Theory Inhabitation and Unification
Chase Norman, Jeremy Avigad
Dependent type theory is the foundation of many modern proof assistants. Inhabitation and unification are undecidable problems that are useful for theorem proving and program synth…
DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs
Tate Rowney, Riyaz Ahuja, Jeremy Avigad +1
Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and…
Hint-Based SMT Proof Reconstruction
Joshua Clune, Haniel Barbosa, Jeremy Avigad
There are several paradigms for integrating interactive and automated theorem provers, combining the convenience of powerful automation with strong soundness guarantees. We introdu…
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
Yicheng Qian, Joshua Clune, Clark Barrett +1
Proof automation is crucial to large-scale formal mathematics and software/hardware verification projects in ITPs. Sophisticated tools called hammers have been developed to provide…
Canonical for Automated Theorem Proving in Lean
Chase Norman, Jeremy Avigad
Canonical is a solver for type inhabitation in dependent type theory, that is, the problem of producing a term of a given type. We present a Lean tactic which invokes Canonical to…