Strong conjunction and intersection types

DOI10.1007/3-540-54345-7_49MaRDI QIDQ4035227zbMATH OpenFDO

Authors Fabio Alessi, Franco Barbanera

Publication date 18 May 1993

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-54345-7_49

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: Strong conjunction and intersection types

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