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

Alberto Carraro, Giulio Guerrieri

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

19 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