2 Search Results for "Zacchi, Maddalena"

Document

Invited Talk

DOI: 10.4230/LIPIcs.FSCD.2025.3

Unsolvable Terms in Filter Models (Invited Talk)

Authors: Mariangiola Dezani-Ciancaglini, Paola Giannini, and Furio Honsell

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract

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.

Cite as

Mariangiola Dezani-Ciancaglini, Paola Giannini, and Furio Honsell. Unsolvable Terms in Filter Models (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 3:1-3:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dezaniciancaglini_et_al:LIPIcs.FSCD.2025.3,
  author =	{Dezani-Ciancaglini, Mariangiola and Giannini, Paola and Honsell, Furio},
  title =	{{Unsolvable Terms in Filter Models}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{3:1--3:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.3},
  URN =		{urn:nbn:de:0030-drops-236181},
  doi =		{10.4230/LIPIcs.FSCD.2025.3},
  annote =	{Keywords: \lambda-calculus, Intersection Types, Unsolvable Terms, Filter Models}
}

Document

DOI: 10.4230/LIPIcs.TYPES.2013.129

Isomorphism of "Functional" Intersection Types

Authors: Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi

Published in: LIPIcs, Volume 26, 19th International Conference on Types for Proofs and Programs (TYPES 2013)

Abstract

Type isomorphism for intersection types is quite odd, since it is not a congruence and it does not extend type equality in the standard interpretation of types. The lack of congruence is due to the proof theoretic nature of the intersection introduction rule, which requires the same term to be the subject of both premises. A partial congruence can be recovered by introducing a suitable notion of type similarity. Type equality in standard models becomes included in type isomorphism whenever atomic types have "functional" interpretations, i.e. they are equivalent to arrow types. This paper characterises type isomorphism for a type system in which the equivalence between atomic types and arrow types is induced by the initial projections of the Scott's model via the correspondence between inverse limit models and filter lambda-models.

Cite as

Mario Coppo, Mariangiola Dezani-Ciancaglini, Ines Margaria, and Maddalena Zacchi. Isomorphism of "Functional" Intersection Types. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 129-149, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{coppo_et_al:LIPIcs.TYPES.2013.129,
  author =	{Coppo, Mario and Dezani-Ciancaglini, Mariangiola and Margaria, Ines and Zacchi, Maddalena},
  title =	{{Isomorphism of "Functional" Intersection Types}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{129--149},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Matthes, Ralph and Schubert, Aleksy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.129},
  URN =		{urn:nbn:de:0030-drops-46296},
  doi =		{10.4230/LIPIcs.TYPES.2013.129},
  annote =	{Keywords: Type Isomorphism, Lambda calculus, Intersection Types}
}

Refine by Type
2 Document/PDF
1 Document/HTML

Refine by Publication Year
1 2025
1 2014

Refine by Author
2 Dezani-Ciancaglini, Mariangiola
1 Coppo, Mario
1 Giannini, Paola
1 Honsell, Furio
1 Margaria, Ines
Show More...

Refine by Series/Journal
2 LIPIcs

Refine by Classification
1 Theory of computation → Type theory

Refine by Keyword
2 Intersection Types
1 Filter Models
1 Lambda calculus
1 Type Isomorphism
1 Unsolvable Terms
Show More...

2 Search Results for "Zacchi, Maddalena"

Unsolvable Terms in Filter Models (Invited Talk)

Abstract

Cite as

Isomorphism of "Functional" Intersection Types

Abstract

Cite as

Thanks for your feedback!

Could not send message