Hostname: page-component-cd9895bd7-p9bg8 Total loading time: 0 Render date: 2024-12-26T05:46:55.700Z Has data issue: false hasContentIssue false

Classical logic, continuation semantics and abstract machines

Published online by Cambridge University Press:  01 November 1998

Th. STREICHER
Affiliation:
Fachbereich 4 Mathematik, TU Darmstadt, Schlossgartenstr. 7, 64289 Darmstadt, Germany (e-mail: [email protected])
B. REUS
Affiliation:
Institut für Informatik, Ludwig-Maximilians-Universität, Oettingenstr. 67, D-80538 München, Germany (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 [Cscr ]. 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.

Type
Research Article
Copyright
© 1998 Cambridge University Press
Submit a response

Discussions

No Discussions have been published for this article.