A monotone lambda-calculus: the example of ordinal terms

Guillaume Bonfante 1 François Lamarche 1
1 CALLIGRAMME - Linear logic, proof networks and categorial grammars
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present a new class of inductive definitions in type theory, which define binary relations instead of simple types (sets). The basic differen ce with ordinary inductive types is that the elimination rule (induction princip le) associated to such a type has two conclusions, one for elements and one for the pairs of the binary relation. In order for the calculus to be easier to use we develop a ``graph based'' calculus, which has many properties in common with the lambda calculus, including the possibility of abstraction. For example we gi ve the countable ordinal omega and a ``monotone'' system of ordinal notations.
Type de document :
[Intern report] A00-R-180 || bonfante00a, 2000, 15 p
Liste complète des métadonnées

Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:52:36
Dernière modification le : jeudi 11 janvier 2018 - 06:19:48


  • HAL Id : inria-00099304, version 1



Guillaume Bonfante, François Lamarche. A monotone lambda-calculus: the example of ordinal terms. [Intern report] A00-R-180 || bonfante00a, 2000, 15 p. 〈inria-00099304〉



Consultations de la notice