One method of defining the semantics of programming language constructs in terms of lambda calculus. II

Cybernetics ◽  
1984 ◽  
Vol 19 (3) ◽  
pp. 325-333
Author(s):  
V. N. Domrachev ◽  
Yu. V. Kapitonova ◽  
L. G. Samoilenko
2003 ◽  
Vol 10 (25) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy

Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds's defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink in previous work (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.<br /><br />Superseded by BRICS-RS-04-5.


Cybernetics ◽  
1982 ◽  
Vol 17 (5) ◽  
pp. 590-595
Author(s):  
V. N. Domrachev ◽  
Yu. V. Kapitonova ◽  
L. G. Samoilenko

2000 ◽  
Vol 10 (3) ◽  
pp. 321-359 ◽  
Author(s):  
ANDREW M. PITTS

Studies of the mathematical properties of impredicative polymorphic types have for the most part focused on the polymorphic lambda calculus of Girard–Reynolds, which is a calculus of total polymorphic functions. This paper considers polymorphic types from a functional programming perspective, where the partialness arising from the presence of fixpoint recursion complicates the nature of potentially infinite (‘lazy’) data types. An approach to Reynolds' notion of relational parametricity is developed that works directly on the syntax of a programming language, using a novel closure operator to relate operational behaviour to parametricity properties of types. Working with an extension of Plotkin's PCF with ∀-types, lazy lists and existential types, we show by example how the resulting logical relation can be used to prove properties of polymorphic types up to operational equivalence.


2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-30
Author(s):  
Ningning Xie ◽  
Daan Leijen

This paper studies compilation techniques for algebraic effect handlers. In particular, we present a sequence of refinements of algebraic effects, going via multi-prompt delimited control, _generalized evidence passing_, yield bubbling, and finally a monadic translation into plain lambda calculus which can be compiled efficiently to many target platforms. Along the way we explore various interesting points in the design space. We provide two implementations of our techniques, one as a library in Haskell, and one as a C backend for the Koka programming language. We show that our techniques are effective, by comparing against three other best-in-class implementations of effect handlers: multi-core OCaml, the _Ev.Eff_ Haskell library, and the libhandler C library. We hope this work can serve as a basis for future designs and implementations of algebraic effects.


2004 ◽  
Vol 11 (5) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy

Starting from a continuation-based interpreter for a simple logic programming language, propositional Prolog with cut, we derive the corresponding logic engine in the form of an abstract machine. The derivation originates in previous work (our article at PPDP 2003) where it was applied to the lambda-calculus. The key transformation here is Reynolds's defunctionalization that transforms a tail-recursive, continuation-passing interpreter into a transition system, i.e., an abstract machine. Similar denotational and operational semantics were studied by de Bruin and de Vink (their article at TAPSOFT 1989), and we compare their study with our derivation. Additionally, we present a direct-style interpreter of propositional Prolog expressed with control operators for delimited continuations.


Sign in / Sign up

Export Citation Format

Share Document