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

DOI10.1016/0168-0072(94)90047-7zbMath0814.03009OpenAlexW2007974484MaRDI QIDQ1326769

Jean-Louis Krivine

Publication date: 13 June 1995

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(94)90047-7

zbMATH Keywords

classical logiccontinuationsSystem Fstorage operatorsdata type of natural numbershead reductionsecond-order lambda-calculus

Mathematics Subject Classification ID

Theory of programming languages (68N15) Combinatory logic and lambda calculus (03B40)

Related Items

A general storage theorem for integers in call-by-name \(\lambda\)- calculus ⋮ Normalization in the simply typed -calculus ⋮ The impact of higher-order state and control effects on local relational reasoning ⋮ A semantical storage operator theorem for all types ⋮ Machine Deduction ⋮ Entiers intuitionnistes et entiers classiques en $\lambda \, C$-calcul ⋮ Computation with classical sequents ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC ⋮ Verificationism and Classical Realizability ⋮ A new deconstructive logic: linear logic ⋮ Proving correctness of a compiler using step-indexed logical relations ⋮ A short proof of the strong normalization of classical natural deduction with disjunction ⋮ Résultats de complétude pour des classes de types du système $\mathcal {AF}2$ ⋮ Les types de données syntaxiques du système ${\cal F}$ ⋮ Uniform Heyting arithmetic ⋮ An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus ⋮ Completeness of continuation models for \(\lambda_\mu\)-calculus ⋮ Refined program extraction from classical proofs ⋮ Unnamed Item ⋮ About classical logic and imperative programming ⋮ Unnamed Item ⋮ Complete Types in an Extension of the System AF2 ⋮ From computation to foundations via functions and application: The \(\lambda\)-calculus and its webbed models ⋮ Proofs, Reasoning and the Metamorphosis of Logic ⋮ Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique ⋮ Logical Relations and Nondeterminism

Cites Work

• On the unity of logic
• Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• A new constructive logic: classic logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item