Abstract
We systematically derive a classical call-by-need sequent calculus, which does not require an unbounded search for the standard redex, by using the unity of semantic artifacts proposed by Danvy et al. The calculus serves as an intermediate step toward the generation of an environment-based abstract machine. The resulting abstract machine is context-free, so that each step is parametric in all but one component. The context-free machine elegantly leads to an environment-based CPS transformation. This transformation is observationally different from a natural classical extension of the transformation of Okasaki et al., due to duplication of un-evaluated bindings.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7(3), 265–301 (1997)
Ariola, Z.M., Herbelin, H.: Control reduction theories: the benefit of structural substitution. J. Funct. Program. 18(3), 373–419 (2008)
Ariola, Z.M., Herbelin, H., Saurin, A.: Classical Call-by-Need and Duality. In: Ong, L. (ed.) TLCA 2011. LNCS, vol. 6690, pp. 27–44. Springer, Heidelberg (2011)
Danvy, O.: From Reduction-Based to Reduction-Free Normalization. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 66–164. Springer, Heidelberg (2009)
Danvy, O., Millikin, K., Munk, J., Zerny, I.: Defunctionalized Interpreters for Call-by-Need Evaluation. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 240–256. Springer, Heidelberg (2010)
Garcia, R., Lumsdaine, A., Sabry, A.: Lazy evaluation and delimited control. In: Proceedings of POPL 2009, pp. 153–164. ACM, New York (2009)
Maraist, J., Odersky, M., Wadler, P.: The call-by-need λ-calculus. J. Funct. Program. 8(3), 275–317 (1998)
Okasaki, C., Lee, P., Tarditi, D.: Call-by-need and continuation-passing style. In: Lisp and Symbolic Computation, pp. 57–81. Kluwer Academic Publishers (1993)
Parigot, M.: λ μ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ariola, Z.M., Downen, P., Herbelin, H., Nakata, K., Saurin, A. (2012). Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. In: Schrijvers, T., Thiemann, P. (eds) Functional and Logic Programming. FLOPS 2012. Lecture Notes in Computer Science, vol 7294. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29822-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-642-29822-6_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-29821-9
Online ISBN: 978-3-642-29822-6
eBook Packages: Computer ScienceComputer Science (R0)