Beyond notations: hygienic macro expansion for theorem proving languages

MaRDI QIDQ5094129zbMATH OpenFDO

Authors Sebastian Ullrich, Leonardo de Moura

Publication date 2 August 2022

Full work available at URL https://arxiv.org/abs/2001.10490, https://lmcs.episciences.org/9362

zbMATH Keywords

lean macro hygiene

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Recommendations

• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
• The Lean 4 theorem prover and programming language
• The Lean theorem prover (system description)
• Mtac: a monad for typed tactic programming in Coq
• A Theory of Hygienic Macros

Cites work

• Beyond notations: hygienic macro expansion for theorem proving languages
• Eisbach: a proof method language for Isabelle
• scientific article; zbMATH DE number 1696760 (Why is no real title available?)
• MetaML and multi-stage programming with explicit annotations
• Notions of computation and monads
• The Lean 4 theorem prover and programming language

Cited in

(3)

• Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
• Beyond notations: hygienic macro expansion for theorem proving languages
• Teaching mathematics using Lean and controlled natural language

Describes a project that uses

Uses Software

• Eisbach
• Lean

This page was built for publication: Beyond notations: hygienic macro expansion for theorem proving languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5094129)