Abstract
We describe simple call-by-value and call-by-name abstract machines, expressed with the help of Felleisen’s evaluation contexts, for a toy functional language. Then we add a simple control operator and extend the abstract machines accordingly. We give some examples of their use. Then, restricting our attention to the sole core (typed) λ-calculus fragment augmented with the control operator, we give a logical status to the machinery. Evaluation contexts are typed “on the left”, as they are directed towards their hole, or their input, in contrast to terms, whose type is that of their output. A machine state consists of a term and a context, and corresponds logically to a cut between a formula on the left (context) and a formula on the right (term). Evaluation, viewed logically, is cut-elimination: this is the essence of the so-called Curry-Howard isomorphism. Control operators correspond to classical reasoning principles, as was first observed by Griffin.
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
Curien, P.-L., and Herbelin, H., The duality of computation, Proc. International Conference on Functional Programming 2000, IEEE (2000).
Danos, V., and Krivine, J.-L., Disjunctive tautologies and synchronisation schemes, Proc. Computer Science Logic 2000.
de Groote, Ph., On the relation between the λμ-calculus and the syntactic theory of sequential control, in Proc. Logic Programming and Automated Reasoning’ 94, Lecture Notes in Computer Science 822, Springer (1994).
Felleisen, M., and Friedman, D., Control operators, the SECD machine, and the λ-calculus, in Formal Description of Programming Concepts III, 193–217, North Holland (1986).
Girard, J.-Y., Lafont, Y., and Taylor, P., Proofs and Types, Cambridge University Press (1989).
Greussay, P., Contribution à la définition interprétative et à l’implémentation des lambda-langages, Thèse d’Etat, Université Paris VII (1977).
Griffin, T., A formula-as-types notion of control, in Proc. Principles of Programming Languages 1990, IEEE (1990).
Gunter, C., Rémy, D., and Riecke, J., A generalization of exceptions and control in ML-like languages, in Proc. Functional Programming and Computer Architecture’ 95, ACM Press (1995).
Parigot, M. λμ-calculus: An algorithmic interpretation of classical natural deduction, Proc. of the International Conference on Logic Programming and Automated Reasoning, St. Petersburg, Lecture Notes in Computer Science 624 (1992).
Prawitz, D., Natural deduction, a proof-theoretical study, Almqvist & Wiskell (1965).
Reynolds, J., Theories of programming languages, Cambridge University Press (1998).
Thielecke, H., Categorical structure of continuation passing style, PhD Thesis, Univ. of Edinburgh (1997).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Curien, PL. (2002). Abstract Machines, Control, and Sequents. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds) Applied Semantics. APPSEM 2000. Lecture Notes in Computer Science, vol 2395. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45699-6_3
Download citation
DOI: https://doi.org/10.1007/3-540-45699-6_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44044-4
Online ISBN: 978-3-540-45699-5
eBook Packages: Springer Book Archive