Zeitschriftenartikel:
G. Ebner, S. Ullrich, J. Roesch, J. Avigad, L. de Moura:
"A metaprogramming framework for formal verification";
Proceedings of the ACM on Programming Languages (PACMPL),
1
(2017),
ICFB, Artikel 34;
29 S.
Kurzfassung englisch:
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 Lean's internal structures and procedures, and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our implementation is performant, and that it provides a convenient and flexible way of writing not only small-scale interactive tactics, but also more substantial kinds of automation.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1145/3110278
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.