* Proof by Reflection

  • Yves Bertot
  • Pierre Castéran
Part of the Texts in Theoretical Computer Science An EATCS Series book series (TTCS)

Abstract

Proof by reflection is a characteristic feature of proving in type theory. There is a programming language embedded inside the logical language and it can be used to describe decision procedures or systematic reasoning methods. We already know that programming in Coq is a costly task and this approach is only worth the effort because the proof process is made much more efficient. In some cases, dozens of rewrite operations can be replaced with a few theorem applications and a convertibility test of the Calculus of Inductive Constructions. Since the computations of this programming language do not appear in the proof terms, we obtain proofs that are smaller and often quicker to check.

Keywords

Sorting Prefix Ctac 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Yves Bertot
    • 1
  • Pierre Castéran
    • 2
  1. 1.Inria Sophia AntipolisSophia Antipolis CedexFrance
  2. 2.LaBRI and Inria Futurs LabRIUniversité Bordeaux ITalence CedexFrance

Personalised recommendations