A Small-Step Operational Semantics for GP 2

2021 ◽  
Vol 350 ◽  
pp. 89-110
Author(s):  
Brian Courtehoute ◽  
Detlef Plump
Keyword(s):  
Operational Semantics ◽  
Small Step

scholarly journals Set constraints for destructive array update optimization

2001 ◽  
Vol 11 (3) ◽  
pp. 319-346 ◽  
Author(s):  
MITCHELL WAND ◽  
WILLIAM D. CLINGER
Keyword(s):  
Polynomial Time ◽  
Program Transformation ◽  
Operational Semantics ◽  
Functional Languages ◽  
Small Step ◽  
Set Constraints ◽  
Correct Program

Destructive array update optimization is critical for writing scientific codes in functional languages. We present set constraints for an interprocedural update optimization that runs in polynomial time. This is a multi-pass optimization, involving interprocedural flow analyses for aliasing and liveness. We characterize and prove the soundness of these analyses using small-step operational semantics. We also prove that any sound liveness analysis induces a correct program transformation.

scholarly journals High-level small-step operational semantics for transactions

2008 ◽  
Vol 43 (1) ◽  
pp. 51-62 ◽  
Author(s):  
Katherine F. Moore ◽  
Dan Grossman
Keyword(s):  
Operational Semantics ◽  
Small Step ◽  
High Level

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 Compilation and equivalence of imperative objects

1999 ◽  
Vol 9 (4) ◽  
pp. 373-426 ◽  
Author(s):  
ANDREW D. GORDON ◽  
PAUL D. HANKIN ◽  
SØREN B. LASSEN
Keyword(s):  
Operational Semantics ◽  
Direct Proof ◽  
Object Oriented ◽  
Small Step ◽  
Abstract Machine ◽  
Program Equivalence ◽  
Contextual Equivalence ◽  
Object Oriented Languages

We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling object-oriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus. Our first two results are theorems asserting the equivalence of our substitution-based semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.

scholarly journals Formal Semantics for Java-like Languages and Research Opportunities

2018 ◽  
Vol 25 (3) ◽  
pp. 62
Author(s):  
Samuel Da Silva Feitosa ◽  
Rodrigo Geraldo Ribeiro ◽  
Andre Rauber Du Bois
Keyword(s):  
Formal Specification ◽  
Formal Semantics ◽  
Operational Semantics ◽  
Object Oriented ◽  
The State ◽  
Small Step ◽  
Research Opportunities ◽  
Type Safety ◽  
State Of Art ◽  
Object Oriented Languages

The objective of this paper is twofold: first, we discuss the state of art on Java-like semantics, focusing on those that provide formal specification using operational semantics (big-step or small-step), studying in detail the most cited projects and presenting some derivative works that extend the originals aggregating useful features. Also, we filter our research for those that provide some insights in type-safety proofs. Furthermore, we provide a comparison between the most used projects in order to show which functionalities are covered in such projects. Second, our effort is focused towards the research opportunities in this area, showing some important works that can be applied to the previously presented projects to study features of object-oriented languages, and pointing for some possibilities to explore in future researches.

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 Compilation and Equivalence of Imperative Objects (Revised Report)

1998 ◽  
Vol 5 (55) ◽  
Author(s):  
Andrew D. Gordon ◽  
Paul D. Hankin ◽  
Søren B. Lassen
Keyword(s):  
Operational Semantics ◽  
Direct Proof ◽  
Object Oriented ◽  
Small Step ◽  
Abstract Machine ◽  
Program Equivalence ◽  
Contextual Equivalence

We adopt the untyped imperative object calculus of Abadi and<br />Cardelli as a minimal setting in which to study problems of compilation<br />and program equivalence that arise when compiling object oriented<br />languages. We present both a big-step and a small-step<br />substitution-based operational semantics for the calculus. Our first<br />two results are theorems asserting the equivalence of our substitution based semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott's CIU<br />equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in<br />our prototype compiler, for statically resolving method offsets. This is<br />the first study of correctness of an object-oriented abstract machine,<br />and of operational equivalence for the imperative object calculus.

Sign in / Sign up

Export Citation Format

Share Document