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

CoqPL-2020-papers
14:00 - 15:05: CoqPL - Invited Talk at Maurepas
Chair(s): Yves BertotINRIA
CoqPL-2020-papers14:00 - 15:00
Talk
Kathrin StarkSaarland University, Germany