A completeness result for a realisability semantics for an intersection type system
From MaRDI portal
Publication:882122
DOI10.1016/j.apal.2007.02.001zbMath1127.03011arXiv0905.0354OpenAlexW1964013598MaRDI QIDQ882122
Fairouz Kamareddine, Karim Nour
Publication date: 23 May 2007
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/0905.0354
completenessnormalisationsoundnessintersection type systemspositive typesrealisability semanticssubject expansionsubject reduction
Related Items (2)
Nominal essential intersection types ⋮ A completeness result for the simply typed \(\lambda \mu \)-calculus
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A completeness result for the simply typed \(\lambda \mu \)-calculus
- An extension of basic functionality theory for \(\lambda\)-calculus
- The completeness theorem for typing lambda-terms
- Curry's type-rules are complete with respect to the F-semantics too
- Normalization without reducibility
- Intersection types and lambda models
- A new type assignment for λ-terms
- A filter lambda model and the completeness of type assignment
- Un résultat de complétude pour les types ∀+ du système F
- Principal Type Schemes for the Strict Type Assignment System
- Résultats de complétude pour des classes de types du système $\mathcal {AF}2$
- Typed Lambda Calculi and Applications
This page was built for publication: A completeness result for a realisability semantics for an intersection type system