A Realizability Interpretation for Intersection and Union Types

DOI10.1007/978-3-319-47958-3_11zbMath1485.03030OpenAlexW2519014191MaRDI QIDQ3179292

Daniel J. Dougherty, Claude Stolze, Ugo de'Liguoro, Luigi Liquori

Publication date: 21 December 2016

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01317213/file/0-paper.pdf

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (2)

Unnamed Item ⋮ Unnamed Item

Uses Software

• Coq
• Isabelle
• Forsythe

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The completeness of provable realizability
• An extension of basic functionality theory for \(\lambda\)-calculus
• Type inference, abstract interpretation and strictness analysis
• Proof-functional connectives and realizability
• The ``relevance of intersection and union types
• Intersection and union types: Syntax and semantics
• Intersection-types à la Church
• Intersection Typed λ-calculus
• Logic and Computation in a Lambda Calculus with Intersection and Union Types
• A filter lambda model and the completeness of type assignment
• An ideal model for recursive polymorphic types
• A framework for defining logics
• Theories of Programming Languages
• A calculus with polymorphic and polyvariant flow types
• Simple type-theoretic foundations for object-oriented programming
• Hyperformulae, Parallel Deductions and Intersection Types
• Elaborating intersection and union types

This page was built for publication: A Realizability Interpretation for Intersection and Union Types