3 Search Results for "Di Gianantonio, Pietro"

Document
DOI: 10.4230/LIPIcs.TYPES.2021.5
Principal Types as Lambda Nets

Authors: Pietro Di Gianantonio and Marina Lenisa

Published in: LIPIcs, Volume 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021)

Abstract
We show that there are connections between principal type schemata, cut-free λ-nets, and normal forms of the λ-calculus, and hence there are correspondences between the normalisation algorithms of the above structures, i.e. unification of principal types, cut-elimination of λ-nets, and normalisation of λ-terms. Once the above correspondences have been established, properties of the typing system, such as typability, subject reduction, and inhabitation, can be derived from properties of λ-nets, and vice-versa. We illustrate the above pattern on a specific type assignment system, we study principal types for this system, and we show that they correspond to λ-nets with a non-standard notion of cut-elimination. Properties of the type system are then derived from results on λ-nets.
Cite as

Pietro Di Gianantonio and Marina Lenisa. Principal Types as Lambda Nets. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{digianantonio_et_al:LIPIcs.TYPES.2021.5,
  author =	{Di Gianantonio, Pietro and Lenisa, Marina},
  title =	{{Principal Types as Lambda Nets}},
  booktitle =	{27th International Conference on Types for Proofs and Programs (TYPES 2021)},
  pages =	{5:1--5:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-254-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{239},
  editor =	{Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2021.5},
  URN =		{urn:nbn:de:0030-drops-167744},
  doi =		{10.4230/LIPIcs.TYPES.2021.5},
  annote =	{Keywords: Lambda calculus, Principal types, Linear logic, Lambda nets, Normalization, Cut elimination}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.15
lambda!-calculus, Intersection Types, and Involutions

Authors: Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
Abramsky’s affine combinatory algebras are models of affine combinatory logic, which refines standard combinatory logic in the direction of Linear Logic. Abramsky introduced various universal models of computation based on affine combinatory algebras, consisting of partial involutions over a suitable formal language {of moves}, in order to discuss reversible computation in a Geometry of Interaction setting. We investigate partial involutions from the point of view of the model theory of lambda!-calculus. The latter is a refinement of the standard lambda-calculus, corresponding to affine combinatory logic. We introduce intersection type systems for the lambda!-calculus, by extending standard intersection types with a !_u-operator. These induce affine combinatory algebras, and, via suitable quotients, models of the lambda!-calculus. In particular, we introduce an intersection type system for assigning principal types to lambda!-terms, and we state a correspondence between the partial involution interpreting a combinator and the principal type of the corresponding lambda!-term. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction.
Cite as

Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. lambda!-calculus, Intersection Types, and Involutions. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ciaffaglione_et_al:LIPIcs.FSCD.2019.15,
  author =	{Ciaffaglione, Alberto and Di Gianantonio, Pietro and Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan},
  title =	{{lambda!-calculus, Intersection Types, and Involutions}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.15},
  URN =		{urn:nbn:de:0030-drops-105228},
  doi =		{10.4230/LIPIcs.FSCD.2019.15},
  annote =	{Keywords: Affine Combinatory Algebra, Affine Lambda-calculus, Intersection Types, Geometry of Interaction}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.231
Innocent Game Semantics via Intersection Type Assignment Systems

Authors: Pietro Di Gianantonio and Marina Lenisa

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
The aim of this work is to correlate two different approaches to the semantics of programming languages: game semantics and intersection type assignment systems (ITAS). Namely, we present an ITAS that provides the description of the semantic interpretation of a typed lambda calculus in a game model based on innocent strategies. Compared to the traditional ITAS used to describe the semantic interpretation in domain theoretic models, the ITAS presented in this paper has two main differences: the introduction of a notion of labelling on moves, and the omission of several rules, i.e. the subtyping rules and some structural rules.
Cite as

Pietro Di Gianantonio and Marina Lenisa. Innocent Game Semantics via Intersection Type Assignment Systems. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 231-247, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{digianantonio_et_al:LIPIcs.CSL.2013.231,
  author =	{Di Gianantonio, Pietro and Lenisa, Marina},
  title =	{{Innocent Game Semantics via Intersection Type Assignment Systems}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{231--247},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.231},
  URN =		{urn:nbn:de:0030-drops-42005},
  doi =		{10.4230/LIPIcs.CSL.2013.231},
  annote =	{Keywords: Game Semantics, Intersection Type Assignment System, Lambda Calculus}
}
  • Refine by Author
  • 3 Di Gianantonio, Pietro
  • 3 Lenisa, Marina
  • 1 Ciaffaglione, Alberto
  • 1 Honsell, Furio
  • 1 Scagnetto, Ivan

  • Refine by Classification

  • Refine by Keyword
  • 1 Affine Combinatory Algebra
  • 1 Affine Lambda-calculus
  • 1 Cut elimination
  • 1 Game Semantics
  • 1 Geometry of Interaction
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2013
  • 1 2019
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact