TY - GEN
T1 - Call-by-value solvability, revisited
AU - Accattoli, Beniamino
AU - Paolini, Luca
PY - 2012/6/6
Y1 - 2012/6/6
N2 - In the call-by-value lambda-calculus solvable terms have been characterised by means of call-by-name reductions, which is disappointing and requires complex reasonings. We introduce the value-substitution lambda-calculus, a simple calculus borrowing ideas from Herbelin and Zimmerman's call-by-value λ CBV calculus and from Accattoli and Kesner's substitution calculus λ sub . In this new setting, we characterise solvable terms as those terms having normal form with respect to a suitable restriction of the rewriting relation.
AB - In the call-by-value lambda-calculus solvable terms have been characterised by means of call-by-name reductions, which is disappointing and requires complex reasonings. We introduce the value-substitution lambda-calculus, a simple calculus borrowing ideas from Herbelin and Zimmerman's call-by-value λ CBV calculus and from Accattoli and Kesner's substitution calculus λ sub . In this new setting, we characterise solvable terms as those terms having normal form with respect to a suitable restriction of the rewriting relation.
U2 - 10.1007/978-3-642-29822-6_4
DO - 10.1007/978-3-642-29822-6_4
M3 - Conference contribution
AN - SCOPUS:84861722887
SN - 9783642298219
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 4
EP - 16
BT - Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Proceedings
T2 - 11th International Symposium onFunctional and Logic Programming, FLOPS 2012
Y2 - 23 May 2012 through 25 May 2012
ER -