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 AugDisplayed time zone: Eastern Time (US & Canada) change

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