HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 8:52:36 AM
Last modification on : Friday, February 4, 2022 - 3:30:02 AM


  • 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⟩



Record views