1 Search Results for "Peyrot, Loïc"

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-dev.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}
}
  • Refine by Author
  • 1 Kesner, Delia
  • 1 Peyrot, Loïc

  • Refine by Classification
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Rewrite systems
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 CBN/CBV
  • 1 Generalized applications
  • 1 Lambda-calculus
  • 1 Quantitative types
  • 1 Solvability

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 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 Imprint Privacy Contact