Autosubst 2: Reasoning with de Bruijn Terms and Substitutions
summary
Introduces Autosubst 2, a Coq library for working with de Bruijn-variable representations and explicit substitutions; explains its design, API and tactics for mechanising syntax, variable binding, renaming and substitution lemmas in Coq; demonstrates how Autosubst 2 automates routine proofs about de Bruijn terms and integrates with Coq proofs to simplify formalisation of programming-language metatheory.
AI-written summary · about
related talks
15mSulfur: Substitution Generation using a Logical Framework
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
01h 34mFormal Logic Undressed
46mMechanizing Abstract Interpretation
30mFormal Metatheory of Second-Order Abstract Syntax
21mCompositional pre-processing for automated reasoning in dependent type theory
19mExtensible Metatheory Mechanization via Family Polymorphism
26mThe Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…)