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 :
Reports
Liste complète des métadonnées

https://hal.inria.fr/inria-00099304
Contributor : Publications Loria <>
Submitted on : Tuesday, September 26, 2006 - 8:52:36 AM
Last modification on : Thursday, January 11, 2018 - 6:19:48 AM

Identifiers

  • HAL Id : inria-00099304, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

201