A generic strong normalization argument: Application to the Calculus of Constructions

We show how to incorporate rewriting into the Calculus of Constructions and we prove that the resulting system is strongly normalizing with respect to beta and rewrite reductions. An important novelty of this paper is the possibility to define rewriting rules over dependently typed function symbols. We prove strong normalization for any term rewriting system, such that all function symbols satisfy the, so called, star dependency condition, and every rule is accepted by the Higher Order Recursive Path Ordering (which is an extension of the method created by Jouannaud and Rubio for the setting of the simply typed lambda calculus). The proof of strong normalization is done by using a typed version of reducibility candidates due to Coquand and Gallier. Our criterion is general enough to accept definitions by rewriting of many well-known higher order functions, for example dependent recursors for inductive types or proof carrying functions. This makes it a very good candidate for inclusion in a proof assistant based on the Curry-Howard isomorphism.

Download Full-text

Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved

Conditional and Typed Rewriting Systems - Lecture Notes in Computer Science ◽

10.1007/3-540-54317-1_96 ◽

1991 ◽

pp. 259-271 ◽

Cited By ~ 7

Author(s):

Franco Barbanera

Keyword(s):

Strong Normalization ◽

Calculus Of Constructions

Download Full-text

A short and flexible proof of strong normalization for the calculus of constructions

Lecture Notes in Computer Science - Types for Proofs and Programs ◽

10.1007/3-540-60579-7_2 ◽

1995 ◽

pp. 14-38 ◽

Cited By ~ 18

Author(s):

Herman Geuvers

Keyword(s):

Strong Normalization ◽

Calculus Of Constructions

Download Full-text

Modular proof of strong normalization for the calculus of constructions

Journal of Functional Programming ◽

10.1017/s0956796800020037 ◽

1991 ◽

Vol 1 (2) ◽

pp. 155-189 ◽

Cited By ~ 64

Author(s):

Herman Geuvers ◽

Mark-Jan Nederhof

Keyword(s):

Fine Structure ◽

General Framework ◽

Type Systems ◽

Strong Normalization ◽

Calculus Of Constructions

AbstractWe present a modular proof of strong normalization for the Calculus of Constructions of Coquand and Huet (1985, 1988). This result was first proved by Coquand (1986), but our proof is more perspicious. The method consists of a little juggling with some systems in the cube of Barendregt (1989), which provides a fine structure of the calculus of constructions. It is proved that the strong normalization of the calculus of constructions is equivalent with the strong normalization of Fω.In order to give the proof, we first establish some properties of various type systems. Therefore, we present a general framework of typed lambda calculi, including many well-known ones.

Download Full-text

Well-founded recursion with copatterns and sized types

Journal of Functional Programming ◽

10.1017/s0956796816000022 ◽

2016 ◽

Vol 26 ◽

Cited By ~ 14

Author(s):

ANDREAS ABEL ◽

BRIGITTE PIENTKA

Keyword(s):

Pattern Matching ◽

Proof Assistants ◽

Strong Normalization ◽

Semantic Framework ◽

Size Information ◽

Infinite Trees ◽

Calculus Of Constructions ◽

Significant Step ◽

Core Language ◽

Finite Data

AbstractIn this paper, we study strong normalization of a core language based on System ${\mathsf{F}_\omega}$ which supports programming with finite and infinite structures. Finite data such as finite lists and trees is defined via constructors and manipulated via pattern matching, while infinite data such as streams and infinite trees is defined by observations and synthesized via copattern matching. Taking a type-based approach to strong normalization, we track size information about finite and infinite data in the type. We exploit the duality of pattern and copatterns to give a unifying semantic framework which allows us to elegantly and uniformly support both well-founded induction and coinduction by rewriting. The strong normalization proof is structured around Girard's reducibility candidates. As such, our system allows for non-determinism and does not rely on coverage. Since System ${\mathsf{F}_\omega}$ is general enough that it can be the target of compilation for the Calculus of Constructions, this work is a significant step towards representing observation-based infinite data in proof assistants such as Coq and Agda.

Download Full-text