Publication details

Saarland University Computer Science

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               

Login to edit

Webmaster, Wed Sep 16 10:47:00 2009