2026-07-22T10:45:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10535 2024-03-06T10:46:09Z ddc:004 open_access

The Delta-calculus: Syntax and Types Liquori, Luigi Stolze, Claude intersection types lambda calculus à la Church and à la Curry proof-functional logics We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T, e.g. the Coppo-Dezani, the Coppo-Dezani-Sallé, the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of Delta-calculi with related intersection typed systems. We prove the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems à la Curry and the corresponding intersection typed systems à la Church by means of an essence function translating an explicitly typed Delta-term into a pure lambda-term one. We finally translate a Delta-term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic Delta-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Luigi Liquori and Claude Stolze 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.28 urn:nbn:de:0030-drops-105354 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.28 eng https://creativecommons.org/licenses/by/3.0/legalcode