10.4230/LIPIcs.CSL.2011.51
Bernadet, Alexis
Lengrand, Stéphane
Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH, Wadern/Saarbruecken, Germany
2011
Computer Science
000 Computer science, knowledge, general works
Herbstritt, Marc
2011-08-31
eng
ConferencePaper
16 pages
application/pdf
1.0
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC-BY-NC-ND)
This paper revisits models of typed lambda calculus based on filters of intersection types:
By using non-idempotent intersections, we simplify a methodology that produces modular proofs of strong normalisation based on filter models. Building such a model for some type theory shows that typed terms can be typed with intersections only, and are therefore strongly normalising. Non-idempotent intersections provide a decreasing measure proving a key termination property, simpler than the reducibility techniques used with idempotent intersections.
Such filter models are shown to be captured by orthogonality techniques: we formalise an abstract notion of orthogonality model inspired by classical realisability, and express a filter model as one of its instances, along with two term-models (one of which captures a now common technique for strong normalisation).
Applying the above range of model constructions to Curry-style System F describes at different levels of detail how the infinite polymorphism of System F can systematically be reduced to the finite polymorphism of intersection types.