Write a Blog >>
Tue 21 Jan 2020 10:30 - 10:51 at Maurepas - Mechanized metatheory Chair(s): Benjamin C. Pierce

The mechanisation of the meta-theory of programming languages is still considered hard and requires considerable effort. When formalising properties of the extension of a language, one hence wants to reuse definitions and proofs. But type-theoretic proof assistants use inductive types and predicates to formalise syntax and type systems, and these definitions are closed to extensions. Available approaches for modular syntax are either inapplicable to type theory or add a layer of indirectness by requiring complicated encodings of types.

We present a concise, transparent, and accessible approach to modular syntax with binders by adapting Swierstra’s Data Types à la Carte approach to the Coq proof assistant in an ad-hoc way. Our approach relies on two phases of code generation: We extend the Autosubst~2 tool and allow users to specify modular syntax with binders in a HOAS-like input language. To state and automatically compose modular functions and lemmas, we implement commands based on MetaCoq. We support modular syntax, functions, predicates, and theorems.

We demonstrate the practicality of our approach by modular proofs of preservation, weak head normalisation, and strong normalisation for several variants of mini-ML.

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change

10:30 - 11:35: Mechanized metatheoryCPP at Maurepas
Chair(s): Benjamin C. PierceUniversity of Pennsylvania
10:30 - 10:51
Coq à la Carte - A Practical Approach to Modular Syntax with Binders
Yannick ForsterSaarland University, Kathrin StarkPrinceton University, USA
DOI Pre-print Media Attached
10:51 - 11:13
A Mechanized Formalization of GraphQL
Tomás DíazIMFD Chile, Federico OlmedoUniversity of Chile & IMFD Chile, Éric TanterUniversity of Chile
DOI Pre-print Media Attached File Attached
11:13 - 11:35
ConCert: A Smart Contract Certification Framework in Coq
Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University
DOI Pre-print Media Attached File Attached