package coq-autosubst
Coq library for parallel de Bruijn substitutions
Install
Dune Dependency
Authors
Maintainers
Sources
v1.8.tar.gz
sha512=15077c2b9ad6acf71bc7853e14c205dea49d948c25ff9d7c19b026745fbd029fa8135f18d94317976f281880589c8dfa87c8ddbd657b70ae2818b7502ae6adc5
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:2023-07-12Published: 12 Jul 2023
On This Page