** Infinite Objects and Proofs

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


Reasoning about infinite objects while staying in the finite world of a computer is one of the most fascinating uses of proof tools.


Recursive Call Inductive Type Recursive Definition Implicit Argument Guard Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


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