CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions

2006 ◽  
pp. 257-271 ◽  
Author(s):  
Gilles Barthe ◽  
Benjamin Grégoire ◽  
Fernando Pastawski
Keyword(s):  
Calculus Of Inductive Constructions ◽  
Recursive Definitions

scholarly journals Residual theory in λ-calculus: a formal development

1994 ◽  
Vol 4 (3) ◽  
pp. 371-394 ◽  
Author(s):  
Gérard Huet
Keyword(s):  
Normal Forms ◽  
Data Types ◽  
The Coq Proof Assistant ◽  
Coq Proof Assistant ◽  
Concrete Syntax ◽  
Calculus Of Inductive Constructions ◽  
Recursive Definitions ◽  
Abstract Framework ◽  
Order Predicate Calculus ◽  
Standard Library

AbstractWe present the complete development, in Gallina, of the residual theory of β-reduction in pure λ-calculus. The main result is the Prism Theorem, and its corollary Lévy's Cube Lemma, a strong form of the parallel-moves lemma, itself a key step towards the confluence theorem and its usual corollaries (Church-Rosser, uniqueness of normal forms). Gallina is the specification language of the Coq Proof Assistant (Dowek et al., 1991; Huet 1992b). It is a specific concrete syntax for its abstract framework, the Calculus of Inductive Constructions (Paulin-Mohring, 1993). It may be thought of as a smooth mixture of higher-order predicate calculus with recursive definitions, inductively defined data types and inductive predicate definitions reminiscent of logic programming. The development presented here was fully checked in the current distribution version Coq V5.8. We just state the lemmas in the order in which they are proved, omitting the proof justifications. The full transcript is available as a standard library in the distribution of Coq.

scholarly journals Final coalgebras as greatest fixed points in ZF set theory

1999 ◽  
Vol 9 (5) ◽  
pp. 545-567 ◽  
Author(s):  
LAWRENCE C. PAULSON
Keyword(s):  
Fixed Points ◽  
Set Theory ◽  
Theorem Prover ◽  
Infinite Length ◽  
Special Cases ◽  
Definition Of ◽  
Recursive Definitions ◽  
Ordered Pairs

A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo–Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel's solution and substitution lemmas are proved in the style of Rutten and Turi (1993). The approach is less general than Aczel's, but the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint.Compared with previous work (Paulson, 1995a), iterated substitutions and solutions are considered, as well as final coalgebras defined with respect to parameters. The disjoint sum construction is replaced by a smoother treatment of urelements that simplifies many of the derivations.The theory facilitates machine implementation of recursive definitions by letting both inductive and coinductive definitions be represented as fixed points. It has already been applied to the theorem prover Isabelle (Paulson, 1994).

Sign in / Sign up

Export Citation Format

Share Document