Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2602.18657 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917298369986560 |
|---|---|
| author | Rowney, Tate Ahuja, Riyaz Avigad, Jeremy Welleck, Sean |
| author_facet | Rowney, Tate Ahuja, Riyaz Avigad, Jeremy Welleck, Sean |
| contents | Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and such DSLs is a tedious engineering chore. To simplify this task, we present DSLean, a framework for bidirectional translation between expressions in the Lean proof assistant and external syntax. DSLean requires only a specification of an external language and its Lean equivalents, abstracting away meta-level implementation details. We demonstrate DSLean's capabilities by implementing three new automation tactics, providing access to external solvers for interval arithmetic, ordinary differential equations, and ring ideal membership. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_18657 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs Rowney, Tate Ahuja, Riyaz Avigad, Jeremy Welleck, Sean Logic in Computer Science Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and such DSLs is a tedious engineering chore. To simplify this task, we present DSLean, a framework for bidirectional translation between expressions in the Lean proof assistant and external syntax. DSLean requires only a specification of an external language and its Lean equivalents, abstracting away meta-level implementation details. We demonstrate DSLean's capabilities by implementing three new automation tactics, providing access to external solvers for interval arithmetic, ordinary differential equations, and ring ideal membership. |
| title | DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2602.18657 |