TL;DR
DBGen is a tool that automates the generation of definitions and properties related to lifting and substitution in the De Bruijn setting for Coq developers, simplifying formalization tasks.
Contribution
It introduces an automated method for generating De Bruijn-related definitions and properties from annotated term structures in Coq.
Findings
Automates the generation of lifting and substitution definitions.
Provides a named syntax and translation to De Bruijn syntax.
Facilitates formal verification in Coq.
Abstract
DBGen is a tool for Coq developers. It takes as input the definition of a term structure with bindings annotations and generates definitions and properties for lifting and substitution in the De Bruijn setting, up to the substitution lemma. It provides also a named syntax and a translation function to the De Bruijn syntax.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems