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 <>
Submitted on : Tuesday, September 26, 2006 - 8:52:36 AM
Last modification on : Friday, February 26, 2021 - 3:28:03 PM


  • 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