Write a Blog >>
Sat 25 Jan 2020 14:00 - 15:00 at Maurepas - Invited Talk Chair(s): Yves Bertot

Mechanising metatheory in the Coq proof assistant is often considered tedious as reasoning with binders without native support requires a lot of uninteresting technicalities. To relieve users from so-produced boilerplate, the Autosubst compiler automates working with de Bruijn terms. Autosubst translates second-order HOAS specifications into the corresponding pure or scoped de Bruijn algebra: It hence generates a corresponding instantiation operation for parallel substitutions, several equational substitution lemmas, and tactics that among others implement automation for assumption-free substitution lemmas. Recent extensions of the Autosubst compiler include support for first-order syntax, variadic syntax, and modular syntax.

In this talk, we outline the design and usage of Autosubst and in particular its recent extensions.

Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

14:00 - 15:05
Invited TalkCoqPL at Maurepas
Chair(s): Yves Bertot INRIA
Autosubst 2: Mechanising binders in Coq (Keynote)
Kathrin Stark Princeton University, USA
File Attached