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. © Springer-Verlag Berlin Heidelberg 2002.
CITATION STYLE
Curien, P. L. (2002). Abstract machines, control, and sequents. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2395 LNCS, pp. 123–136). Springer Verlag. https://doi.org/10.1007/3-540-45699-6_3
Mendeley helps you to discover research relevant for your work.