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
Times are displayed in time zone: Eastern Time (US & Canada) change

10:00 - 11:30: Session 1TyDe at TyDe
10:00 - 10:30
Practical Dependent Type Checking Using Twin Types
Víctor López JuanChalmers University of Technology, Nils Anders DanielssonUniversity of Gothenburg, Chalmers University of Technology
Media Attached
10:30 - 11:00
Shallowly Embedding Type Theories as Presheaf Models in Agda (Extended Abstract)
Joris CeulemansVrije Universiteit Brussel, Dominique DevrieseVrije Universiteit Brussel
File Attached
11:00 - 11:30
Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2 (Extended Abstract)
Ignacio TiraboschiNone, Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET