Name
Abstract | ||
|---|---|---|
We propose to use Tarski's least fixpoint theorem as a ba- sis to define recursive functions in the calculus of inductive construc- tions. This widens the class of functions that can be modeled in type- theory based theorem proving tool to potentially non-terminating func- tions. This is only possible if we extend the logical framework by adding the axioms that correspond to classical logic. We claim that the ex- tended framework makes it possible to reason about terminating and non-terminating computations and we show that common facilities of the calculus of inductive construction, like program extraction can be extended to also handle the new functions. |
Year | Venue | Keywords |
|---|---|---|
2006 | Clinical Orthopaedics and Related Research | calculus of constructions,fixed point theorem,type theory,theorem proving,classical logic,logical framework |
Field | DocType | Volume |
Discrete mathematics,Natural deduction,Lambda cube,Automated theorem proving,Algorithm,First-order logic,Calculus of constructions,Fundamental theorem,Classical logic,Mathematics,Calculus,Logical framework | Journal | abs/cs/061 |
Citations | PageRank | References |
0 | 0.34 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Yves Bertot | 1 | 442 | 40.82 |
| inria sophia antipolis | 2 | 51 | 6.54 |