Skip to Main content Skip to Navigation
Conference papers

Fixed point semantics and partial recursion in Coq

Yves Bertot 1, * Vladimir Komendantsky 1, *
* Corresponding author
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We propose to use 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 modeled 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.
Complete list of metadatas

https://hal.inria.fr/inria-00190975
Contributor : Vladimir Komendantsky <>
Submitted on : Friday, November 23, 2007 - 1:54:42 PM
Last modification on : Monday, September 3, 2018 - 10:56:02 AM
Long-term archiving on: : Monday, April 12, 2010 - 4:49:17 AM

Files

tarski.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00190975, version 1

Citation

Yves Bertot, Vladimir Komendantsky. Fixed point semantics and partial recursion in Coq. MPC 2008, Jul 2008, Marseille, France. ⟨inria-00190975v1⟩

Share

Metrics

Record views

17

Files downloads

369