Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

Completeness and Decidability of de Bruijn Substitution Algebra in Coq

Steven Schäfer, Gert Smolka, Tobias Tebbi

Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pp. 67-73, ACM, 2015

We consider a two-sorted algebra over de Bruijn terms and de Bruijn substitutions equipped with the constants and operations from Abadi et al.'s sigma-calculus. We consider expressions with term variables and substitution variables and show that the semantic equivalence obtained with the algebra coincides with the axiomatic equivalence obtained with finitely many axioms based on the sigma-calculus. We prove this result with an informative decision algorithm for axiomatic equivalence, which in the negative case returns a variable assignment separating the given expressions in the algebra. The entire development is formalized in Coq.

Download PDF        Show BibTeX               

@INPROCEEDINGS{SchaeferEtAl:2015:Completeness,
  title = {Completeness and Decidability of de Bruijn Substitution Algebra in Coq},
  author = {Steven Schäfer and Gert Smolka and Tobias Tebbi},
  year = {2015},
  publisher = {ACM},
  booktitle = {Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015},
  pages = {67-73},
}

Login to edit