Procedural representation of CIC proof terms

DOI10.1007/S10817-009-9137-6zbMATH Open1185.68622OpenAlexW2100997280MaRDI QIDQ2655331FDOQ2655331

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)

Cites Work

• User interaction with the Matita proof assistant
• A modern perspective on type theory. From its origins until today
• Mathematical knowledge management in HELM
• Mathematical Knowledge Management
• The formal system λδ
• Procedural representation of CIC proof terms
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (2)

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

Uses Software

• Coq
• Matita
• Automath

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• A duality between proof systems for cyclic term graphs 👍 👎
• Proofs, programs, processes 👍 👎
• Cyclic proofs of program termination in separation logic 👍 👎
• Abstract cyclic proofs 👍 👎
• Structured proof procedures 👍 👎
• Declarative representation of proof terms 👍 👎
• Labelled cyclic proofs for separation logic 👍 👎

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)