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

Alberto Carraro; Giulio Guerrieri

doi:10.1007/978-3-642-54830-7_7

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

Alberto Carraro, Giulio Guerrieri

Department of Computer Science

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

46 Citations (SciVal)

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 language	English
Title of host publication	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.
Publisher	Springer Verlag
Pages	103-118
Number of pages	16
ISBN (Print)	9783642548291
DOIs	https://doi.org/10.1007/978-3-642-54830-7_7
Publication status	Published - 1 Jan 2014
Event	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 Duration: 5 Apr 2014 → 13 Apr 2014

Publication series

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

Conference

Conference	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
Country/Territory	France
City	Grenoble
Period	5/04/14 → 13/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
General Computer Science

Access to Document

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

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 or section in a book/report/conference proceeding › Chapter in a published conference proceeding

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)). doi: 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 = jan,

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.",

note = "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 ; Conference date: 05-04-2014 Through 13-04-2014",

}

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 - Chapter in a published conference proceeding

AN - SCOPUS:84900564002

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

T2 - 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

Y2 - 5 April 2014 through 13 April 2014

ER -

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

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this