We compare several reduction and conversion strategies for the Calculus of (co)Inductive Constructions by running benchmarks on the library of the Coq proof assistant. All the strategies have been implemented in an independent verifier for the proof objects of Coq that is part of the Matita proof assistant.

Reduction and Conversion Strategies for the Calculus of (co)Inductive Construtions: Part I

SACERDOTI COEN, CLAUDIO
2007

Abstract

We compare several reduction and conversion strategies for the Calculus of (co)Inductive Constructions by running benchmarks on the library of the Coq proof assistant. All the strategies have been implemented in an independent verifier for the proof objects of Coq that is part of the Matita proof assistant.
97
118
C. Sacerdoti Coen
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/48931
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact