Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Full Reduction at Full Throttle
verfasst von : Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire
Erschienen in: Certified Programs and Proofs
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Emerging trends in proof styles and new applications of interactive proof assistants exploit the computational facilities of the provided proof language, reaping enormous benefits in proof size and convenience to the user. However, the resulting proof objects really put the proof assistant to the test in terms of computational time required to check them. We present a novel translation of the terms of the full Calculus of (Co)Inductive Constructions to
OCaml
programs. Building on this translation, we further present a new fully featured version of
Coq
that offloads much of the computation required during proof checking to a vanilla, state of the art and fine tuned compiler. This modular scheme yields substantial performance improvements over existing systems at a reduced implementation cost.
The work presented here builds on previous work described in [11], but we place particular emphasis in this paper on the fact that this scheme is in fact an instance of untyped normalization by evaluation [8, 14, 1,4].