License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2021.7
URN: urn:nbn:de:0030-drops-142458
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14245/
Go to the corresponding LIPIcs Volume Portal

Kerinec, Axel ; Manzonetto, Giulio ; Ronchi Della Rocca, Simona

Call-By-Value, Again!

pdf-format:
LIPIcs-FSCD-2021-7.pdf (0.8 MB)

Abstract

The quest for a fully abstract model of the call-by-value λ-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically.
We study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many λ-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus - namely valuability, potential valuability and solvability - both semantically, through the notion of approximants, and logically, by means of the type assignment system. We mainly focus on the characterizations of solvability, as they constitute an original result. Finally, we prove the decidability of the inhabitation problem for our type system by exhibiting a non-deterministic algorithm, which is proven sound, correct and terminating.

BibTeX - Entry

@InProceedings{kerinec_et_al:LIPIcs.FSCD.2021.7,
  author =	{Kerinec, Axel and Manzonetto, Giulio and Ronchi Della Rocca, Simona},
  title =	{{Call-By-Value, Again!}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14245},
  URN =		{urn:nbn:de:0030-drops-142458},
  doi =		{10.4230/LIPIcs.FSCD.2021.7},
  annote =	{Keywords: \lambda-calculus, call-by-value, intersection types, solvability, inhabitation}
}

Keywords: λ-calculus, call-by-value, intersection types, solvability, inhabitation
Collection: 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)
Issue Date: 2021
Date of publication: 06.07.2021

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