sle2020/paper09

SLE 2020 paper:
Untangling Mechanized Proofs

Clément Pit-Claudel

• DOI: 10.1145/3426425.3426940
• T1A: Design
  • The paper primarily contributes language design techniques or decisions.
• T5D: Formal Methods
  • It relies on formal methods (definitions/proofs/semantic properties) beyond informal description.
• T4C: Vertical Transformation
  • It uses compilation/generation/refinement to derive executable artefacts (vertical transformations).
• T4D: Interpretation
  • It concerns runtime interpretation/execution (interpreters, debuggers, runtime services).

---

The page is maintained by Dr. Vadim Zaytsev a.k.a. @grammarware. Last updated: June 2026.