Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq

DOI10.1007/978-3-540-74464-1_5zbMath1178.68525OpenAlexW1955878572MaRDI QIDQ3612436

Venanzio Capretta, Amy P. Felty

Publication date: 10 March 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74464-1_5

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (2)

The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax

Uses Software

• Coq
• Twelf

This page was built for publication: Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq