Streicher, Th and Reus, B (1998) Classical logic, continuation semantics and abstract machines. Journal of Functional Programming, 8 (6). pp. 543-572. ISSN 0956-7968

Preview

PDF Download (333kB) | Preview

Abstract

One of the goals of this paper is to demonstrate that denotational semantics is useful for operational issues like implementation of functional languages by abstract machines. This is exemplified in a tutorial way by studying the case of extensional untyped call-by-name λ-calculus with Felleisen's control operator 𝒞. We derive the transition rules for an abstract machine from a continuation semantics which appears as a generalization of the ¬¬-translation known from logic. The resulting abstract machine appears as an extension of Krivine's machine implementing head reduction. Though the result, namely Krivine's machine, is well known our method of deriving it from continuation semantics is new and applicable to other languages (as e.g. call-by-value variants). Further new results are that Scott's D∞-models are all instances of continuation models. Moreover, we extend our continuation semantics to Parigot's λμ-calculus from which we derive an extension of Krivine's machine for λμ-calculus. The relation between continuation semantics and the abstract machines is made precise by proving computational adequacy results employing an elegant method introduced by Pitts.

Item Type:	Article
Schools and Departments:	School of Engineering and Informatics > Informatics
Subjects:	Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User:	Chris Keene
Date Deposited:	03 Mar 2008
Last Modified:	02 Jul 2019 20:52
URI:	http://sro.sussex.ac.uk/id/eprint/1439
Google Scholar:	94 Citations

View download statistics for this item

📧 Request an update