A semantical storage operator theorem for all types

DOI10.1016/S0168-0072(97)00041-9zbMath0899.03014MaRDI QIDQ1382182

Christophe Raffalli

Publication date: 25 March 1998

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

zbMATH Keywords

lambda-calculusGödel translationAF2 type systemdata-typesstorage operator

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Second- and higher-order arithmetic and fragments (03F35) Combinatory logic and lambda calculus (03B40)

Related Items (2)

Résultats de complétude pour des classes de types du système $\mathcal {AF}2$ ⋮ Complete Types in an Extension of the System AF2

Cites Work

• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Opérateurs de mise en mémoire et traduction de Gödel. (Storage operators and Gödel translation)
• Recursive programming with proofs
• Classical logic, storage operators and second-order lambda-calculus
• Opérateurs de mise en mémoire et types $\forall $-positifs
• A General Type for Storage Operators
• Storage operators and directed lambda-calculus
• Storage Operators and ∀‐positive Types in TTR Type System

This page was built for publication: A semantical storage operator theorem for all types