License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2019.28
URN: urn:nbn:de:0030-drops-105354
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/10535/
Go to the corresponding LIPIcs Volume Portal

Liquori, Luigi ; Stolze, Claude

The Delta-calculus: Syntax and Types

pdf-format:
LIPIcs-FSCD-2019-28.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{liquori_et_al:LIPIcs:2019:10535,
  author =	{Luigi Liquori and Claude Stolze},
  title =	{{The Delta-calculus: Syntax and Types}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Herman Geuvers},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/10535},
  URN =		{urn:nbn:de:0030-drops-105354},
  doi =		{10.4230/LIPIcs.FSCD.2019.28},
  annote =	{Keywords: intersection types, lambda calculus {\`a} la Church and {\`a} la Curry, proof-functional logics}
}

Keywords: intersection types, lambda calculus à la Church and à la Curry, proof-functional logics
Collection: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
Issue Date: 2019
Date of publication: 18.06.2019

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI