A semantical and operational account of call-by-value solvability

Alberto Carraro, Giulio Guerrieri

Research output: Chapter in Book/Report/Conference proceedingConference contribution

16 Citations (Scopus)

Abstract

In Plotkin's call-by-value lambda-calculus, solvable terms are characterized syntactically by means of call-by-name reductions and there is no neat semantical characterization of such terms. Preserving confluence, we extend Plotkin's original reduction without adding extra syntactical constructors, and we get a call-by-value operational characterization of solvable terms. Moreover, we give a semantical characterization of solvable terms in a relational model, based on Linear Logic, satisfying the Taylor expansion formula. As a technical tool, we also use a resource-sensitive calculus (with tests) in which the elements of the model are definable.

Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures - 17th Int. Conf., FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proc.
PublisherSpringer Verlag
Pages103-118
Number of pages16
ISBN (Print)9783642548291
DOIs
Publication statusPublished - 1 Jan 2014
Event17th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 - Grenoble, France
Duration: 5 Apr 201413 Apr 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8412 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference17th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
CountryFrance
CityGrenoble
Period5/04/1413/04/14

Keywords

  • (resource) call-by-value lambda-calculus
  • potential valuability
  • relational semantics
  • solvability
  • tests
  • weak and stratified reductions

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Carraro, A., & Guerrieri, G. (2014). A semantical and operational account of call-by-value solvability. In Foundations of Software Science and Computation Structures - 17th Int. Conf., FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proc. (pp. 103-118). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8412 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-54830-7_7

A semantical and operational account of call-by-value solvability. / Carraro, Alberto; Guerrieri, Giulio.

Foundations of Software Science and Computation Structures - 17th Int. Conf., FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proc.. Springer Verlag, 2014. p. 103-118 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8412 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Carraro, A & Guerrieri, G 2014, A semantical and operational account of call-by-value solvability. in Foundations of Software Science and Computation Structures - 17th Int. Conf., FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proc.. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8412 LNCS, Springer Verlag, pp. 103-118, 17th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, 5/04/14. https://doi.org/10.1007/978-3-642-54830-7_7
Carraro A, Guerrieri G. A semantical and operational account of call-by-value solvability. In Foundations of Software Science and Computation Structures - 17th Int. Conf., FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proc.. Springer Verlag. 2014. p. 103-118. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-54830-7_7
Carraro, Alberto ; Guerrieri, Giulio. / A semantical and operational account of call-by-value solvability. Foundations of Software Science and Computation Structures - 17th Int. Conf., FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proc.. Springer Verlag, 2014. pp. 103-118 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{4012b6a706b64088813b1ae462c34f6c,
title = "A semantical and operational account of call-by-value solvability",
abstract = "In Plotkin's call-by-value lambda-calculus, solvable terms are characterized syntactically by means of call-by-name reductions and there is no neat semantical characterization of such terms. Preserving confluence, we extend Plotkin's original reduction without adding extra syntactical constructors, and we get a call-by-value operational characterization of solvable terms. Moreover, we give a semantical characterization of solvable terms in a relational model, based on Linear Logic, satisfying the Taylor expansion formula. As a technical tool, we also use a resource-sensitive calculus (with tests) in which the elements of the model are definable.",
keywords = "(resource) call-by-value lambda-calculus, potential valuability, relational semantics, solvability, tests, weak and stratified reductions",
author = "Alberto Carraro and Giulio Guerrieri",
year = "2014",
month = "1",
day = "1",
doi = "10.1007/978-3-642-54830-7_7",
language = "English",
isbn = "9783642548291",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "103--118",
booktitle = "Foundations of Software Science and Computation Structures - 17th Int. Conf., FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proc.",

}

TY - GEN

T1 - A semantical and operational account of call-by-value solvability

AU - Carraro, Alberto

AU - Guerrieri, Giulio

PY - 2014/1/1

Y1 - 2014/1/1

N2 - In Plotkin's call-by-value lambda-calculus, solvable terms are characterized syntactically by means of call-by-name reductions and there is no neat semantical characterization of such terms. Preserving confluence, we extend Plotkin's original reduction without adding extra syntactical constructors, and we get a call-by-value operational characterization of solvable terms. Moreover, we give a semantical characterization of solvable terms in a relational model, based on Linear Logic, satisfying the Taylor expansion formula. As a technical tool, we also use a resource-sensitive calculus (with tests) in which the elements of the model are definable.

AB - In Plotkin's call-by-value lambda-calculus, solvable terms are characterized syntactically by means of call-by-name reductions and there is no neat semantical characterization of such terms. Preserving confluence, we extend Plotkin's original reduction without adding extra syntactical constructors, and we get a call-by-value operational characterization of solvable terms. Moreover, we give a semantical characterization of solvable terms in a relational model, based on Linear Logic, satisfying the Taylor expansion formula. As a technical tool, we also use a resource-sensitive calculus (with tests) in which the elements of the model are definable.

KW - (resource) call-by-value lambda-calculus

KW - potential valuability

KW - relational semantics

KW - solvability

KW - tests

KW - weak and stratified reductions

UR - http://www.scopus.com/inward/record.url?scp=84900564002&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-54830-7_7

DO - 10.1007/978-3-642-54830-7_7

M3 - Conference contribution

SN - 9783642548291

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 103

EP - 118

BT - Foundations of Software Science and Computation Structures - 17th Int. Conf., FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proc.

PB - Springer Verlag

ER -