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…