University of Sussex
Browse
1/1
3 files

Classical logic, continuation semantics and abstract machines

journal contribution
posted on 2023-06-07, 14:14 authored by Th Streicher, Bernhard ReusBernhard Reus
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 D8-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.

History

Publication status

  • Published

Journal

Journal of Functional Programming

ISSN

0956-7968

Publisher

Cambridge University Press

Issue

6

Volume

8

Page range

543-572

Department affiliated with

  • Informatics Publications

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2008-03-03

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC