Procedural representation of CIC proof terms

DOI10.1007/S10817-009-9137-6MaRDI QIDQ2655331zbMATH OpenOpenAlexFDO

Authors Ferruccio Guidi

Publication date 25 January 2010

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-009-9137-6

zbMATH Keywords

calculus of constructionsproof termsprocedural proofs

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• Declarative representation of proof terms
• Abstract cyclic proofs
• Structured proof procedures
• Cyclic proofs of program termination in separation logic
• Proof methods for corecursive programs
• A duality between proof systems for cyclic term graphs
• Labelled cyclic proofs for separation logic
• scientific article; zbMATH DE number 4164180
• Proofs, programs, processes

Cites work

• scientific article; zbMATH DE number 1701346 (Why is no real title available?)
• scientific article; zbMATH DE number 3624817 (Why is no real title available?)
• scientific article; zbMATH DE number 1104364 (Why is no real title available?)
• scientific article; zbMATH DE number 1951627 (Why is no real title available?)
• scientific article; zbMATH DE number 2247253 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• A modern perspective on type theory. From its origins until today
• Mathematical Knowledge Management
• Mathematical knowledge management in HELM
• Procedural representation of CIC proof terms
• The formal system λδ
• User interaction with the Matita proof assistant

Cited in

(2)

• Declarative representation of proof terms
• Procedural representation of CIC proof terms

Describes a project that uses

Uses Software

• Automath
• Matita
• Coq

This page was built for publication: Procedural representation of CIC proof terms

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