package coq-autosubst
Coq library for parallel de Bruijn substitutions
Install
Dune Dependency
Authors
Maintainers
Sources
v1.9.tar.gz
sha512=b78504da0cfae1e3368bc31d2cfcc63a5976b0dca2a47ce7887378cdcc6e08cba1325fac875c35562a680046f384d0379dd395422b5625bf511fa8ceb0911652
Description
Autosubst is a library for the Coq proof assistant which provides automation for formalizing syntactic theories with variable binders. Given an inductive definition of syntactic objects in de Bruijn representation augmented with binding annotations, Autosubst synthesizes the parallel substitution operation and automatically proves the basic lemmas about substitutions.
Tags
category:Computer Science/Lambda Calculi keyword:abstract syntax keyword:binders keyword:de Bruijn indices keyword:substitution logpath:Autosubst date:2024-07-12Published: 13 Jul 2024
On This Page