Intuitionistic integers and classical integers in the \(\lambda\) \(C\)-calculus. (Entiers intuitionnistes et entiers classiques en \(\lambda\) \(C\)-calcul.) (French) Zbl 0838.68062

Summary: We give a syntaxical proof of the J. L. Krivine’s operational characterization of classical integers (a closed terms typable, in a classical type system, by the type \(N[s^n(0)]\). We give later conditions on the classical type system in order to obtain the intuitionistic integers.


68W30 Symbolic computation and algebraic computation
Full Text: DOI EuDML


[1] 1. J. L. KRIVINE, Lambda calcul, types et modèle, Masson, Paris, 1990. Zbl0697.03004 MR1162977 · Zbl 0697.03004
[2] 2. J. L. KRIVINE, Classical logic, storage operators and second order lambda-calculus, à paraître dans Annals of pure and applied logic, 1994. Zbl0814.03009 MR1278549 · Zbl 0814.03009
[3] 3. K. NOUR, Opérateurs de mise en mémoire en lambda-calcul pur et typé, Thèse de doctorat, Université de Savoie, 1993.
[4] 4. K. NOUR, Opérateurs de mise en mémoire et types \forall -positifs, soumis à Informatique Théorique et Applications, 1993.
[5] 5. K. NOUR, Quelques résultats sur \lambda C-calcul, C. R. Acad. Sci., Paris, t. 320, série I, 1995, p. 259-262. Zbl0830.03006 MR1320367 · Zbl 0830.03006
[6] 6. M. PARIGOT, \lambda \mu -calculus: an algorithme interpretation of classical natural deduction. LNCS, 1992, 624, p. 190-201. Zbl0925.03092 MR1235373 · Zbl 0925.03092
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.