Classical logic, storage operators and second-order lambda-calculus

Annals of Pure and Applied Logic 68 (1):53-78 (1994)
  Copy   BIBTEX

Abstract

We describe here a simple method in order to obtain programs from proofs in second-order classical logic. Then we extend to classical logic the results about storage operators proved by Krivine for intuitionistic logic. This work generalizes previous results of Parigot

Categories

Keywords

Reprint years

DOI

10.1016/0168-0072(94)90047-7

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Mixed logic and storage operators.Karim Nour - 2000 - Archive for Mathematical Logic 39 (4):261-280.
A General Type for Storage Operators.Karim Nour - 1995 - Mathematical Logic Quarterly 41 (4):505-514.
Storage operators and directed lambda-calculus.René David & Karim Nour - 1995 - Journal of Symbolic Logic 60 (4):1054-1086.
Storage Operators and Second Order Lambda-Calculs.J. -L. Krivine Classical Logic - 1994 - Annals of Pure and Applied Logic 68:53-78.
Strong storage operators and data types.Karim Nour - 1995 - Archive for Mathematical Logic 34 (1):65-78.
Opérateurs de mise en mémoire et traduction de Gödel.Jean-Louis Krivine - 1990 - Archive for Mathematical Logic 30 (4):241-267.
La valeur d'un entier classique en $\lambda\mu$ -calcul.Karim Nour - 1997 - Archive for Mathematical Logic 36 (6):461-473.
Storage operators and forall-positive types of system TTR.Karim Nour - 1996 - Mathematical Logic Quarterly 42:349-368.
$lambdamu$-Calculus and Bohm's Theorem.Rene David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
S-Storage Operators.Karim Nour - 1998 - Mathematical Logic Quarterly 44 (1):99-108.
Lectures on the Curry-Howard isomorphism.Morten Heine Sørensen - 2007 - Boston: Elsevier. Edited by Paweł Urzyczyn.
Typed lambda-calculus in classical Zermelo-Frænkel set theory.Jean-Louis Krivine - 2001 - Archive for Mathematical Logic 40 (3):189-205.
Strong normalization of a symmetric lambda calculus for second-order classical logic.Yoriyuki Yamagata - 2002 - Archive for Mathematical Logic 41 (1):91-99.
Variable binding term operators in $\lambda $-calculus.M. W. Bunder - 1979 - Notre Dame Journal of Formal Logic 20 (4):876-878.
The abstract variable-binding calculus.Don Pigozzi & Antonino Salibra - 1995 - Studia Logica 55 (1):129 - 179.

Analytics

Added to PP
2014-01-16

Downloads
37 (#420,900)

6 months
4 (#790,687)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Uniform heyting arithmetic.Ulrich Berger - 2005 - Annals of Pure and Applied Logic 133 (1):125-148.

View all 8 citations / Add more citations

References found in this work

On the unity of logic.Jean-Yves Girard - 1993 - Annals of Pure and Applied Logic 59 (3):201-217.
Opérateurs de mise en mémoire et traduction de Gödel.Jean-Louis Krivine - 1990 - Archive for Mathematical Logic 30 (4):241-267.

Add more references