Procedural representation of CIC proof terms
From MaRDI portal
Publication:2655331
DOI10.1007/S10817-009-9137-6zbMATH Open1185.68622OpenAlexW2100997280MaRDI QIDQ2655331FDOQ2655331
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
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
- Proofs, programs, processes
Cites Work
- User interaction with the Matita proof assistant
- Title not available (Why is that?)
- A modern perspective on type theory. From its origins until today
- Title not available (Why is that?)
- Title not available (Why is that?)
- Mathematical knowledge management in HELM
- Mathematical Knowledge Management
- The formal system λδ
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Procedural representation of CIC proof terms
Cited In (2)
Uses Software
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)
