Proof-functional connectives and realizability

DOI10.1007/BF01203032zbMath0801.03035MaRDI QIDQ1330311

Franco Barbanera, Simone Martini

Publication date: 1 December 1994

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

zbMATH Keywords

realizabilityintuitionistic logicrelevant implicationstrong equivalencesemantical completenessproof-functional connectiveprovable isomorphisms in typed lambda- calculistrong conjunctiontype assignment system for lambda- terms with intersection types

Mathematics Subject Classification ID

Structure of proofs (03F07) Intuitionistic mathematics (03F55)

Related Items

A Realizability Interpretation for Intersection and Union Types, The ``relevance of intersection and union types, Unnamed Item, Unnamed Item, Plugging-in proof development environments usingLocksinLF

Cites Work

• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The completeness of provable realizability
• An extension of basic functionality theory for \(\lambda\)-calculus
• Intersection types for combinatory logic
• The semantics of entailment. III
• A filter lambda model and the completeness of type assignment
• Provable isomorphisms of types
• What is a model of the lambda calculus?
• Using types as search keys in function libraries
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item