# Call-by-value Solvability

Luca Paolini; Simona Ronchi Della Rocca

RAIRO - Theoretical Informatics and Applications (2010)

- Volume: 33, Issue: 6, page 507-534
- ISSN: 0988-3754

## Access Full Article

top## Abstract

top## How to cite

topPaolini, Luca, and Simona Ronchi Della Rocca. "Call-by-value Solvability." RAIRO - Theoretical Informatics and Applications 33.6 (2010): 507-534. <http://eudml.org/doc/222050>.

@article{Paolini2010,

abstract = {
The notion of solvability in the call-by-value λ-calculus
is defined and completely characterized, both from an operational and a logical
point of view. The operational characterization is given through a reduction
machine, performing the classical β-reduction, according to an innermost strategy.
In fact, it turns out that the call-by-value
reduction rule is too weak for capturing the solvability property
of terms.
The logical characterization is given through an intersection type
assignment system, assigning types of a given shape to all and only the
call-by-value solvable terms.
},

author = {Paolini, Luca, Simona Ronchi Della Rocca},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {Models of computations; λ-calculus; call-by-value.; solvability; -calculus},

language = {eng},

month = {3},

number = {6},

pages = {507-534},

publisher = {EDP Sciences},

title = {Call-by-value Solvability},

url = {http://eudml.org/doc/222050},

volume = {33},

year = {2010},

}

TY - JOUR

AU - Paolini, Luca

AU - Simona Ronchi Della Rocca

TI - Call-by-value Solvability

JO - RAIRO - Theoretical Informatics and Applications

DA - 2010/3//

PB - EDP Sciences

VL - 33

IS - 6

SP - 507

EP - 534

AB -
The notion of solvability in the call-by-value λ-calculus
is defined and completely characterized, both from an operational and a logical
point of view. The operational characterization is given through a reduction
machine, performing the classical β-reduction, according to an innermost strategy.
In fact, it turns out that the call-by-value
reduction rule is too weak for capturing the solvability property
of terms.
The logical characterization is given through an intersection type
assignment system, assigning types of a given shape to all and only the
call-by-value solvable terms.

LA - eng

KW - Models of computations; λ-calculus; call-by-value.; solvability; -calculus

UR - http://eudml.org/doc/222050

ER -

## References

top- S. Abramsky and C.H.L. Ong, Full Abstraction in the Lazy Lambda Calculus. Information and Computation 105 (1993) 159-267. Zbl0779.03003
- H. Barendregt, The Lambda Calculus: Its syntax and semantics. North Holland (1984). Zbl0551.03007
- H. Barendregt, M. Coppo and M. Dezani-Ciancaglini, A filter Lambda Model and the completeness of type assignment. J. Symbolic Logic 48 (1983) 85-116. Zbl0545.03004
- L. Egidi, F. Honsell and S. Ronchi Della Rocca, Operational, denotational and logicals descriptions: A case study. Fund. Inform. (1992) 149-169.
- J.R. Hindley and J.P. Seldin, Introduction to Combinators and λ-Calculus. Cambridge University Press (1986). Zbl0614.03014
- F. Honsell and S. Ronchi Della Rocca, An Approximation Theorem for topological lambda models and the topological incompleteness of Lambda Calculus. J. Comput. Systems Sci. 45 (1992) 49-75. Zbl0763.03012
- M. Hyland, A syntactic characterization of the equalityin some Models for the Lambda Calculus. J. London Math. Soc. (1976) 361-370. Zbl0329.02010
- P.J. Landin, The mechanical evaluation of expressions. Comput. J. (1964). Zbl0122.36106
- R. Milner, M. Tofte and R. Harfen, The definition of standard ML, M.I.T. (1990).
- L. Paolini, La chiamata per valore e la valutazione pigra nel lambda calcolo. Tesi di Laurea, Universitá di Torino, Dip. Informatica (1997).
- G. Plotkin, Call by value, call by name and the λ-calculus. Theoret. Comput. Sci. (1975) 125-159. Zbl0325.68006
- S. Ronchi Della Rocca, Basic λ-calculus. Notes for the Summer School Proof and Types, Chambery (1993).
- G.L. Steele and G.J. Sussman, The revised report on Scheme, AI Memo 452, M.I.T. (1978).
- S. Thompson, HASKELL: The craft of functional programming. Addison-Wesley (1996).
- C.P. Wadsworth, The relation between computational and denotational properties for Scott D∞-models of the lambda calculus. SIAM J. Comput. 5 (1976) 488-522. Zbl0346.02013

## NotesEmbed ?

topTo embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.