DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2022.18

Solvability for Generalized Applications

Authors: Delia Kesner and Loïc Peyrot

Published in: LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

Abstract

Solvability is a key notion in the theory of call-by-name lambda-calculus, used in particular to identify meaningful terms. However, adapting this notion to other call-by-name calculi, or extending it to different models of computation - such as call-by-value - , is not straightforward. In this paper, we study solvability for call-by-name and call-by-value lambda-calculi with generalized applications, both variants inspired from von Plato’s natural deduction with generalized elimination rules. We develop an operational as well as a logical theory of solvability for each of them. The operational characterization relies on a notion of solvable reduction for generalized applications, and the logical characterization is given in terms of typability in an appropriate non-idempotent intersection type system. Finally, we show that solvability in generalized applications and solvability in the lambda-calculus are equivalent notions.

Cite as

Delia Kesner and Loïc Peyrot. Solvability for Generalized Applications. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kesner_et_al:LIPIcs.FSCD.2022.18,
  author =	{Kesner, Delia and Peyrot, Lo\"{i}c},
  title =	{{Solvability for Generalized Applications}},
  booktitle =	{7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  pages =	{18:1--18:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-233-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{228},
  editor =	{Felty, Amy P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.18},
  URN =		{urn:nbn:de:0030-drops-162994},
  doi =		{10.4230/LIPIcs.FSCD.2022.18},
  annote =	{Keywords: Lambda-calculus, Generalized applications, Solvability, CBN/CBV, Quantitative types}
}

Search Results

Documents authored by Peyrot, Loïc

Solvability for Generalized Applications

Abstract

Cite as

Thanks for your feedback!

Could not send message