Abstract
Software that can produce independently checkable evidence for the correctness of its output has received recent attention for use in certifying compilers and proof-carrying code. CVC (Cooperating Validity Checker) is a proof-producing validity checker for a decidable fragment of first-order logic enriched with background theories. This paper describes how proofs of valid formulas are produced from the decision procedure for linear real arithmetic implemented in CVC. It is shown how extensions to LF which support proof rules schematic in an arity ("elliptical" rules) are very convenient for this purpose.
Original language | English (US) |
---|---|
Pages (from-to) | 29-41 |
Number of pages | 13 |
Journal | Electronic Notes in Theoretical Computer Science |
Volume | 70 |
Issue number | 2 |
DOIs | |
State | Published - Dec 2002 |
Event | LFM 2002 International Workshop on Logical Frameworks and Meta-Languages (FLoC Satellite Event) - Copenhagen, Denmark Duration: Jul 26 2002 → Jul 26 2002 |
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science