# Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages

@article{Ullrich2020BeyondNH, title={Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages}, author={Sebastian Ullrich and Leonardo Mendonça de Moura}, journal={Automated Reasoning}, year={2020}, volume={12167}, pages={167 - 182} }

In interactive theorem provers (ITPs), extensible syntax is not only crucial to lower the cognitive burden of manipulating complex mathematical objects, but plays a critical role in developing reusable abstractions in libraries. Most ITPs support such extensions in the form of restrictive “syntax sugar” substitutions and other ad hoc mechanisms, which are too rudimentary to support many desirable abstractions. As a result, libraries are littered with unnecessary redundancy. Tactic languages in… Expand

#### Figures and Topics from this paper

#### 4 Citations

Lassie: HOL4 tactics by example

- Computer Science
- CPP
- 2021

Lassie is presented, a tactic framework for the HOL4 theorem prover that allows individual users to define their own tactic language by example and give frequently used tactics or tactic combinations easier-to-remember names. Expand

A bi-directional extensible interface between Lean and Mathematica

- Computer Science
- ArXiv
- 2021

We implement a user-extensible ad hoc connection between the Lean proof assistant and the computer algebra system Mathematica. By reflecting the syntax of each system in the other and providing a… Expand

A Graphical User Interface Framework for Formal Verification

- Computer Science
- ITP
- 2021

The ProofWidgets framework uses web technology and functional reactive programming, as well as metaprogramming features of advanced interactive theorem proving (ITP) systems to allow users to create arbitrary interactive UIs for representing the goal state. Expand

Verified Optimization

- Computer Science, Mathematics
- ArXiv
- 2021

Progress is described towards developing a framework, based on the Lean interactive proof assistant, for designing and applying reductions in reliable and flexible ways. Expand

#### References

SHOWING 1-10 OF 21 REFERENCES

D-Expressions : Lisp Power , Dylan Style

- 1999

syntax trees (AST’s) are highly structured representations of source code. In an object-oriented implementation, there would typically be one class per definition, statement, or other language… Expand

Elaboration in Dependent Type Theory

- Computer Science
- ArXiv
- 2015

An elaboration algorithm for dependent type theory that has been implemented in the Lean theorem prover is described, which supports higher-order unification, type class inference, ad hoc overloading, insertion of coercions, and the computational reduction of terms. Expand

Syntactic abstraction in scheme

- Computer Science
- LISP Symb. Comput.
- 1992

An efficient macro system is described that prevents inadvertent capturing while maintaining the correlation between source and object code. Expand

MetaML and multi-stage programming with explicit annotations

- Computer Science
- Theor. Comput. Sci.
- 2000

It is argued that multi-stage languages are useful as programming languages in their own right, that they supply a sound basis for high-level program generation technology, and that they should support features that make it possible for programmers to write staged computations without significantly changing their normal programming style. Expand

Honu: syntactic extension for algebraic notation through enforestation

- Computer Science
- GPCE '12
- 2012

A key element of Honu's design is an enforestation parsing step, which converts a flat stream of tokens into an S-expression-like tree in addition to the initial "read" phase of parsing and interleaved with the "macro-expand" phase. Expand

Macros that work

- Computer Science
- POPL '91
- 1991

A modified form of Kohlbecker’s algorithm for reliably hygienic macro expansion in block-structured languages, where macros are source-tosource transformations specified using a high-level pattern language is described. Expand

Dependent type systems as macros

- Computer Science
- Proc. ACM Program. Lang.
- 2020

This paper explains the implementation details of Turnstile+, as well as how it may be used to create a wide-variety of dependently typed languages, from a lightweight one with indexed types, to a full spectrum proof assistant, complete with a tactic system and extensions for features like sized types and SMT interaction. Expand

A metaprogramming framework for formal verification

- Computer Science
- Proc. ACM Program. Lang.
- 2017

We describe the metaprogramming framework currently used in Lean, an interactive theorem prover based on dependent type theory. This framework extends Lean's object language with an API to some of… Expand

A Tactic Language for the System Coq

- Computer Science
- LPAR
- 2000

A new tactic language for the system Coq is proposed, which is intended to enrich the current tactic combinators (tacticals) and is based on a functional core with recursors and matching operators for Coq terms but also for proof contexts. Expand

Hygienic Macros for ACL2

- Computer Science
- Trends in Functional Programming
- 2010

This paper demonstrates how the lack of hygiene in ACL2's macros interferes with theorem proving, and explains how to design and implement a hygienic macro system for ACL2. Expand