2026-07-22T14:19:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5159 2024-03-06T10:36:10Z ddc:004 open_access

Observability for Pair Pattern Calculi Bucciarelli, Antonio Kesner, Delia Ronchi Della Rocca, Simona solvability pattern calculi intersection types inhabitation Inspired by the notion of solvability in the λ-calculus, we define a notion of observability for a calculus with pattern matching. We give an intersection type system for such a calculus which is based on non-idempotent types. The typing system is shown to characterize the set of terms having canonical form, which properly contains the set of observable terms, so that typability alone is not sufficient to characterize observability. However, the inhabitation problem associated with our typing system turns out to be decidable, a result which — together with typability — allows to obtain a full characterization of observability. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Antonio Bucciarelli and Delia Kesner and Simona Ronchi Della Rocca 2015 Is Part Of LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TLCA.2015.123 urn:nbn:de:0030-drops-51596 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.123 eng https://creativecommons.org/licenses/by/3.0/legalcode