关于这一集
Sebastian Ullrich (KIT, Germany), gives the fourth talk in the second panel, Dependently Typed Programming, on the 3rd day of the ICFP conference. Co-written by Gabriel Exner (Vienna University of Technology, Austria), Jared Roesch (University of Washington, USA), Jeremy Avigad (Carnegie Mellon University, USA), Leonardo De Moura (Microsoft Research).
Dependent type theory is a powerful framework for interactive theorem proving and automated reasoning, allowing us to encode mathematical objects, data type specifications, assertions, proofs, and programs, all in the same language.
Here we show that dependent type theory can also serve as its own metaprogramming language, that is, a language in which one can write programs that assist in the construction and manipulation of terms in dependent type theory itself. Specifically, we describe the metaprogramming language currently in use in the Lean theorem prover, which extends Lean's object language with an API for accessing natively implemented procedures and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our language 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.
Dependent type theory is a powerful framework for interactive theorem proving and automated reasoning, allowing us to encode mathematical objects, data type specifications, assertions, proofs, and programs, all in the same language.
Here we show that dependent type theory can also serve as its own metaprogramming language, that is, a language in which one can write programs that assist in the construction and manipulation of terms in dependent type theory itself. Specifically, we describe the metaprogramming language currently in use in the Lean theorem prover, which extends Lean's object language with an API for accessing natively implemented procedures and provides ways of reflecting object-level expressions into the metalanguage. We provide evidence to show that our language 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.
英语
英国
文字稿 🔗
Are you the producer of this podcast?
Add a podcast transcript
Need Audio-to-Text?
Transcribe with Listen411 in Just 60 Seconds
本播客中的其他单集
Martin Avanzini (University of Innsbruck, Austria) gives the second talk in the fifth panel, Inference and Analysis on the 3rd day of the ICFP conference. This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three ingredients: ...
Yuu Igarashi (Kyoto University, Japan) gives the second talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Taro Sekiyama (IBM Research, Japan), Atsushi Igarashi (Kyoto University, Japan).
We study an extension of gradual typin...
Richard A. Eisenberg (Bryn Mawr College, USA) gives the first talk in the fifth panel, Inference and Analysis, on the 3rd day of the ICFP conference. Co-written by J. Garrett Morris (University of Kansas, USA).
We present an approach to support partiality in type-level computation without com...
Victor Lanvin (ENS Cachan, France) gives the third talk in the fourth panel, Integrating Static and Dynamic Typing, on the 3rd day of the ICFP conference. Co-written by Giuseppe Castagna (CNRS, University of Paris Diderot).
We propose a type system for functional languages with gradual types ...
Justin Pombrio (Brown University, USA) gives the third talk in the fifth panel, Inference and Analysis on the 3rd day of the ICFP conference. Co-written by Shriram Krishnamurthi (Brown University, USA) and Mitchell Wand (Northeastern University, USA).
Many languages use syntactic sugar to def...
免责声明: 本页面嵌入的播客和封面图片来自 Oxford University，归其所有者所有，与 Listen Notes, Inc. 无关联，也未获得 Listen Notes, Inc. 背书。
