2026-07-22T22:18:02Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23618 2025-10-27T10:30:17Z ddc:004 open_access

Unsolvable Terms in Filter Models (Invited Talk) Dezani-Ciancaglini, Mariangiola Giannini, Paola Honsell, Furio λ-calculus Intersection Types Unsolvable Terms Filter Models Intersection type theories (itt’s) and filter models, i.e. λ-calculus models generated by itt’s, are reviewed in full generality. In this framework, which subsumes most λ-calculus models in the literature based on Scott-continuous functions, we discuss the interpretation of unsolvable terms. We give a necessary, but not sufficient, condition on an itt for the interpretation of some unsolvable term to be non-trivial in the filter model it generates. This result is obtained building on a type theoretic characterisation of the fine structure of unsolvables. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mariangiola Dezani-Ciancaglini and Paola Giannini and Furio Honsell 2025 Is Part Of LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2025.3 urn:nbn:de:0030-drops-236181 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.3 eng https://creativecommons.org/licenses/by/4.0/legalcode