2026-07-20T14:51:25Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3222 2024-03-06T10:33:58Z ddc:004 open_access

Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism Bernadet, Alexis Lengrand, Stéphane non-idempotent intersections System F realisability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexis Bernadet and Stéphane Lengrand 2011 Is Part Of LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2011.51 urn:nbn:de:0030-drops-32226 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.51 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode