Name
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 nonterminating 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 |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1145/1389449.1389461 | PPDP |
Keywords | Field | DocType |
classical logic,non-terminating computation,partial recursion,new function,recursive function,inductive constructions,logical framework,fixed point semantics,nonterminating function,extended framework,fixed point theorem,fixed point,type theory,theorem proving,automated theorem proving | Algebra,Computer science,Brouwer fixed-point theorem,Automated theorem proving,Algorithm,Theoretical computer science,Least fixed point,Fundamental theorem,Fixed point,Kakutani fixed-point theorem,Logical framework,Fixed-point theorem | Conference |
Citations | PageRank | References |
9 | 0.58 | 14 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yves Bertot | 1 | 442 | 40.82 |
| Vladimir Komendantsky | 2 | 17 | 2.75 |