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
Times are displayed in time zone: Saskatchewan, Central America change

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