Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)

DOI10.1007/BF01792986MaRDI QIDQ923069zbMATH OpenFDO

Authors Jean-Louis Krivine

Publication date 1990

Published in Archive for Mathematical Logic (Search for Journal in Brave)

zbMATH Keywords

data type\(\lambda \) -calculuscall by nameleftmost reduction strategysecond order functional arithmeticstorage operators

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Abstract data types; algebraic specification (68Q65) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• scientific article; zbMATH DE number 458872
• On Storage Operators
• Strong storage operators and data types
• A semantical storage operator theorem for all types

Cites work

• scientific article; zbMATH DE number 4147469 (Why is no real title available?)
• scientific article; zbMATH DE number 46869 (Why is no real title available?)
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(22)

• Lambda-calcul, évaluation paresseuse et mise en mémoire
• Strong storage operators and data types
• Storage operators and directed lambda-calculus
• Opérateurs de mise en mémoire et types $\forall $-positifs
• A conjecture on numeral systems
• A semantical storage operator theorem for all types
• A general storage theorem for integers in call-by-name \(\lambda\)- calculus
• Bounded linear logic: A modular approach to polynomial-time computability
• On Storage Operators
• Gödelization in the lambda calculus
• Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
• Syntactical data types of system \(\mathcal F\)
• Classical logic, storage operators and second-order lambda-calculus
• Machine Deduction
• Krivine's classical realisability from a categorical perspective
• Negative translations not intuitionistically equivalent to the usual ones
• Une réponse négative à la conjecture de E. Tronci pour les systèmes numériques typés
• Injecting uniformities into Peano arithmetic
• A functional interpretation for nonstandard arithmetic
• Complete types in an extension of the system \({\mathcal A}{\mathcal F}2\)
• The Inf function in the system \(F\)
• About classical logic and imperative programming

This page was built for publication: Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q923069)