Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Sun 23 Aug 2020 11:00 - 11:30 at TyDe - Session 1

Meta-languages are becoming an essential part of proof assistants, as they enable the proof developer to automate her proofs. Hence, an increasing number of provers are adopting different meta-languages. The Mtac and Mtac2 meta-languages code meta-programs within a monad in Coq to obtain typed meta-programs. That is, an Mtac2 meta-program with type M A will ensure that the value returned will indeed have type A.

However, the combination of monads and dependent types presents an interesting challenge: The convoy pattern—an extremely useful and often necessary tool for dependent programming in Coq—is not automatically supported. The convoy pattern is necessary when dependent pattern matching inspects values on which \emph{the types} of other values depend.

In this work we present a new meta-meta-program lift that provides a semi-automatic solution: given any meta-program or operator (like bind) and a list of dependencies (what lies behind the last -> in the type of mfix above), it generates a new operator that can be used in a context where such dependencies are expected. It is important to mention that \textbf{we use Mtac as is as its own meta-language!}

Sun 23 Aug

Displayed time zone: Eastern Time (US & Canada) change

10:00 - 11:30
Session 1TyDe at TyDe
Practical Dependent Type Checking Using Twin Types
Víctor López Juan Chalmers University of Technology, Nils Anders Danielsson University of Gothenburg, Chalmers University of Technology
Media Attached
Shallowly Embedding Type Theories as Presheaf Models in Agda (Extended Abstract)
Joris Ceulemans Vrije Universiteit Brussel, Dominique Devriese Vrije Universiteit Brussel
File Attached
Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2 (Extended Abstract)
Ignacio Tiraboschi None, Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET