Operational interpretations of an extension of Fω with control operators

1996 ◽  
Vol 6 (3) ◽  
pp. 393-418 ◽  
Author(s):  
Robert Harper ◽  
Mark Lillibridge
Keyword(s):  
Operational Semantics ◽  
Current Control ◽  
Computation Step ◽  
Evaluation Strategies ◽  
Transformation Algorithms ◽  
System F ◽  
Control Operators

AbstractWe study the operational semantics of an extension of Girard's System Fω with two control operators: an abort operation that abandons the current control context, and a callcc operation that captures the current control context. Two classes of operational semantics are considered, each with a call-by-value and a call-by-name variant, differing in their treatment of polymorphic abstraction and instantiation. Under the standard semantics, polymorphic abstractions are values and polymorphic instantiation is a significant computation step; under the ML-like semantics evaluation proceeds beneath polymorphic abstractions and polymorphic instantiation is computationally insignificant. Compositional, type-preserving continuation-passing style (cps) transformation algorithms are given for the standard semantics, resulting in terms on which all four evaluation strategies coincide. This has as a corollary the soundness and termination of well-typed programs under the standard evaluation strategies. In contrast, such results are obtained for the call-by-value ML-like strategy only for a restricted sub-language in which constructor abstractions are limited to values. The ML-like call-by-name semantics is indistinguishable from the standard call-by-name semantics when attention is limited to complete programs.

scholarly journals From Interpreter to Logic Engine by Defunctionalization

2003 ◽  
Vol 10 (25) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Transition System ◽  
Abstract Machine ◽  
Logic Programming Language ◽  
Delimited Continuations ◽  
Simple Logic ◽  
Control Operators

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.

scholarly journals CPS transformation with affine types for call-by-value implicit polymorphism

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-30
Author(s):  
Taro Sekiyama ◽  
Takeshi Tsukada
Keyword(s):  
Fundamental Property ◽  
The Other ◽  
Target Language ◽  
Logical Relation ◽  
Contextual Equivalence ◽  
Type Preservation ◽  
System F ◽  
Control Operators

Transformation of programs into continuation-passing style (CPS) reveals the notion of continuations, enabling many applications such as control operators and intermediate representations in compilers. Although type preservation makes CPS transformation more beneficial, achieving type-preserving CPS transformation for implicit polymorphism with call-by-value (CBV) semantics is known to be challenging. We identify the difficulty in the problem that we call scope intrusion. To address this problem, we propose a new CPS target language Λ open that supports two additional constructs for polymorphism: one only binds and the other only generalizes type variables. Unfortunately, their unrestricted use makes Λ open unsafe due to undesired generalization of type variables. We thus equip Λ open with affine types to allow only the type-safe generalization. We then define a CPS transformation from Curry-style CBV System F to type-safe Λ open and prove that the transformation is meaning and type preserving. We also study parametricity of Λ open as it is a fundamental property of polymorphic languages and plays a key role in applications of CPS transformation. To establish parametricity, we construct a parametric, step-indexed Kripke logical relation for Λ open and prove that it satisfies the Fundamental Property as well as soundness with respect to contextual equivalence.

scholarly journals An Operational Foundation for Delimited Continuations in the CPS Hierarchy

2004 ◽  
Vol 11 (29) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Explicit Representation ◽  
Small Step ◽  
Abstract Machine ◽  
Delimited Continuations ◽  
New Applications ◽  
Control Operators

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. At level n of the CPS hierarchy, programs can use the control operators shift_i and reset_i for 1 <= i <= n, the evaluator has n + 1 layers of continuations, the abstract machine has n + 1 layers of control stacks, and the reduction semantics has n + 1 layers of evaluation contexts.<br /> <br /> We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

scholarly journals From Interpreter to Logic Engine by Defunctionalization

2004 ◽  
Vol 11 (5) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Logic Programming ◽  
Programming Language ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Transition System ◽  
Abstract Machine ◽  
Logic Programming Language ◽  
Delimited Continuations ◽  
Simple Logic ◽  
Control Operators

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.

scholarly journals Delimited control and computational effects

2014 ◽  
Vol 24 (1) ◽  
pp. 1-55 ◽  
Author(s):  
PAUL DOWNEN ◽  
ZENA M. ARIOLA
Keyword(s):  
Operational Semantics ◽  
Expressive Power ◽  
Reduction Theory ◽  
Level Control ◽  
Abstract Machine ◽  
Fine Grained ◽  
Control Operators

AbstractWe give a framework for delimited control with multiple prompts, in the style of Parigot's λμ-calculus, through a series of incremental extensions by starting with the pure λ-calculus. Each language inherits the semantics and reduction theory of its parent, giving a systematic way to describe each level of control. For each language of interest, we fully characterize its semantics in terms of a reduction semantics, operational semantics, continuation-passing style transform, and abstract machine. Furthermore, the control operations are expressed in terms of fine-grained primitives that can be used to build well-known, higher-level control operators. In order to illustrate the expressive power provided by various languages, we show how other computational effects can be encoded in terms of these control operators.

scholarly journals Some Lambda Calculus and Type Theory Formalized

1997 ◽  
Vol 4 (51) ◽  
Author(s):  
James McKinna ◽  
Robert Pollack
Keyword(s):  
Type Theory ◽  
Operational Semantics ◽  
Lambda Calculus ◽  
Type Systems ◽  
Formal Proof ◽  
Type Checking ◽  
Formal Development ◽  
Formal Definitions ◽  
Pure Type Systems ◽  
System F

"This paper is about our hobby." That is the first sentence of [MP93], the first report on our formal development of lambda calculus and type theory, written in autumn 1992. We have continued to pursue this hobby on and off ever since, and have developed a substantial body of formal knowledge, including Church-Rosser and standardization<br />theorems for beta reduction, and the basic theory of<br />Pure Type Systems (PTS) leading to the strengthening theorem and type checking algorithms for PTS. Some of this work is reported in [MP93, vBJMP94, Pol94b, Pol95]. In the present paper we survey this work, including some new proofs, and point out what we feel has been learned about the general issues of formalizing mathematics. On the technical side, we describe an abstract, and simplified, proof of standardization for beta reduction, not previously published, that does<br />not mention redex positions or residuals. On the general issues, we emphasize the search for formal definitions that are convenient for formal proof and convincingly represent the intended informal concepts. The LEGO Proof Development System [LP92] was used to check the work in an implementation of the Extended Calculus of Constructions<br />(ECC) with inductive types [Luo94]. LEGO is a refinement style<br />proof checker, publicly available by ftp and WWW, with a User's Manual [LP92] and a large collection of examples. Section 1.3 contains information on accessing the formal development described in this paper. Other interesting examples formalized in LEGO include program specification and data refinement [Luo91], strong normalization of System F [Alt93], synthetic domain theory [Reu95, Reu96], and operational semantics for imperative programs [Sch97].

scholarly journals Proving termination of evaluation for System F with control operators

2013 ◽  
Vol 127 ◽  
pp. 15-29
Author(s):  
Małgorzata Biernacka ◽  
Dariusz Biernacki ◽  
Sergueï Lenglet ◽  
Marek Materzok
Keyword(s):  
System F ◽  
Control Operators

scholarly journals A Simple Proof of a Folklore Theorem about Delimited Control

2005 ◽  
Vol 12 (25) ◽  
Author(s):  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Simple Proof ◽  
Operational Semantics ◽  
Small Step ◽  
Control Operators

We formalize and prove the folklore theorem that the static delimited-control operators shift and reset can be simulated in terms of the dynamic delimited-control operators control and prompt. The proof is based on small-step operational semantics.

scholarly journals An Operational Foundation for Delimited Continuations in the CPS Hierarchy

2005 ◽  
Vol 12 (24) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Explicit Representation ◽  
Small Step ◽  
Abstract Machine ◽  
Delimited Continuations ◽  
New Applications ◽  
Control Operators

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. At level n of the CPS hierarchy, programs can use the control operators shift_i and reset_i for 1 <= i <= n, the evaluator has n + 1 layers of continuations, the abstract machine has n + 1 layers of control stacks, and the reduction semantics has n + 1 layers of evaluation contexts.<br /> <br /> We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

scholarly journals An Operational Foundation for Delimited Continuations in the CPS Hierarchy

2005 ◽  
Vol 12 (11) ◽  
Author(s):  
Malgorzata Biernacka ◽  
Dariusz Biernacki ◽  
Olivier Danvy
Keyword(s):  
Operational Semantics ◽  
Lambda Calculus ◽  
Explicit Representation ◽  
Small Step ◽  
Abstract Machine ◽  
Delimited Continuations ◽  
New Applications ◽  
Control Operators

We present an abstract machine and a reduction semantics for the lambda-calculus extended with control operators that give access to delimited continuations in the CPS hierarchy. The abstract machine is derived from an evaluator in continuation-passing style (CPS); the reduction semantics (i.e., a small-step operational semantics with an explicit representation of evaluation contexts) is constructed from the abstract machine; and the control operators are the shift and reset family. At level n of the CPS hierarchy, programs can use the control operators shift_i and reset_i for 1 <= i <= n , the evaluator has n + 1 layers of continuations, the abstract machine has n + 1 layers of control stacks, and the reduction semantics has n + 1 layers of evaluation contexts.<br /> <br /> We also present new applications of delimited continuations in the CPS hierarchy: finding list prefixes and normalization by evaluation for a hierarchical language of units and products.

Sign in / Sign up

Export Citation Format

Share Document