Two-level meta-reasoning in Coq

DOI10.1007/3-540-45685-6_14MaRDI QIDQ4484341zbMATH OpenFDO

Authors Amy P. Felty

Publication date 12 June 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2410/24100198.htm

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• Reasoning with higher-order abstract syntax in a logical framework
• scientific article; zbMATH DE number 1956525
• scientific article; zbMATH DE number 2185713
• scientific article; zbMATH DE number 2185657

Cited in

(9)

• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• A proof dedicated meta-language
• Two-level hybrid: a system for reasoning using higher-order abstract syntax
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• A two-level logic approach to reasoning about typed specification languages
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• scientific article; zbMATH DE number 1956525 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Two-level meta-reasoning in Coq

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