scientific article; zbMATH DE number 176126

MaRDI QIDQ4035227zbMATH OpenFDO

Authors Fabio Alessi, Franco Barbanera

Publication date 18 May 1993

zbMATH Keywords

\(\lambda\)-calculuscombinatory logicintersection typesprovable realizabilityrealizers of formulasstrong conjunctiontype inferenceuntyped \(\lambda\)-terms

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• A realizability interpretation for intersection and union types
• Proof-functional connectives and realizability
• Intersection-types à la Church
• scientific article; zbMATH DE number 1841834
• Intersection types for combinatory logic

Cited in

(11)

• Types with intersection: An introduction
• Proof-functional connectives and realizability
• The ``relevance of intersection and union types
• How to think of intersection types as Cartesian products
• Loader and Urzyczyn are logically related
• A realizability interpretation for intersection and union types
• Inhabitation of Low-Rank Intersection Types
• Completeness of type assignment systems with intersection, union, and type quantifiers
• YACC: Yet Another Church Calculus. A birthday present for Herman inspired by his supervisor activity
• The completeness of provable realizability
• A typed lambda calculus with intersection types

This page was built for publication:

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