Fixed point semantics and partial recursion in Coq

Yves Bertot 1, * Vladimir Komendantsky 1, *
* Auteur correspondant
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We propose to use the Knaster-Tarski least fixed point theorem as a basis to define recursive functions in the Calculus of Inductive Constructions. This widens the class of functions that can be modelled in type-theory based theorem proving tools to potentially non-terminating functions. This is only possible if we extend the logical framework by adding some axioms of classical logic. We claim that the extended framework makes it possible to reason about terminating or non-terminating computations and we show that extraction can also be extended to handle the new functions.
Type de document :
Communication dans un congrès
PPDP 2008, Jul 2008, Valencia, Spain. 2008
Liste complète des métadonnées


https://hal.inria.fr/inria-00190975
Contributeur : Vladimir Komendantsky <>
Soumis le : jeudi 24 juillet 2008 - 16:10:40
Dernière modification le : jeudi 24 juillet 2008 - 16:34:18
Document(s) archivé(s) le : vendredi 24 septembre 2010 - 16:06:12

Identifiants

  • HAL Id : inria-00190975, version 11

Collections

Citation

Yves Bertot, Vladimir Komendantsky. Fixed point semantics and partial recursion in Coq. PPDP 2008, Jul 2008, Valencia, Spain. 2008. <inria-00190975v11>

Partager

Métriques

Consultations de
la notice

711

Téléchargements du document

402