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

DOI10.1007/978-3-540-74464-1_5MaRDI QIDQ3612436zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Higher-order abstract syntax in type theory
• Higher-order abstract syntax in Isabelle/HOL
• scientific article; zbMATH DE number 2185657
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• scientific article; zbMATH DE number 1927423

Cited in

(11)

• Nested abstract syntax in Coq
• scientific article; zbMATH DE number 1696799 (Why is no real title available?)
• Nominal reasoning techniques in Coq (extended abstract)
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• Higher-order abstract syntax in type theory
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• A fully adequate shallow embedding of the π-calculus in Isabelle/HOL with mechanized syntax analysis
• Practical Programming with Higher-Order Encodings and Dependent Types
• Mechanized meta-reasoning using a hybrid HOAS/de Bruijn representation and reflection
• An improved implementation and abstract interface for Hybrid

Describes a project that uses

Uses Software

• Coq
• Twelf

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3612436)