Inter-deriving semantic artifacts for object-oriented programming

We present a new abstract machine for Abadi and Cardelli's untyped non-imperative calculus of objects. This abstract machine mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (i.e., big-step operational semantics) specified in Abadi and Cardelli's monograph. To move closer to actual implementations, which use environments rather than actual substitutions, we then represent methods as closures and we present three new semantic artifacts for a version of Abadi and Cardelli's calculus with explicit substitutions: a reduction semantics, an environment-based abstract machine, and a natural semantics (i.e., an interpreter) with environments. These three new semantic artifacts mechanically correspond to each other, and the two abstract machines are bisimilar. Their significance lies in the fact that they have not been designed from scratch and then proved correct; instead, they have been inter-derived.To illustrate the inter-derivation and to make this article stand-alone, we also comprehensively treat the example of negational normalization over Boolean formulas, in appendix.     

A rewriting logic approach to operational semantics

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, continuation-based semantics, and the chemical abstract machine. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.     

A Rewriting Logic Approach to Operational Semantics (Extended Abstract)

This paper shows how rewriting logic semantics (RLS) can be used as a computational logic framework for operational semantic definitions of programming languages. Several operational semantics styles are addressed: big-step and small-step structural operational semantics (SOS), modular SOS, reduction semantics with evaluation contexts, and continuation-based semantics. Each of these language definitional styles can be faithfully captured as an RLS theory, in the sense that there is a one-to-one correspondence between computational steps in the original language definition and computational steps in the corresponding RLS theory. A major goal of this paper is to show that RLS does not force or pre-impose any given language definitional style, and that its flexibility and ease of use makes RLS an appealing framework for exploring new definitional styles.     

Coinductive big-step operational semantics

Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We formalize the connections between the coinductive big-step semantics and the standard small-step semantics, proving that both semantics are equivalent. We then study the use of coinductive big-step semantics in proofs of type soundness and proofs of semantic preservation for compilers. A methodological originality of this paper is that all results have been proved using the Coq proof assistant. We explain the proof-theoretic presentation of coinductive definitions and proofs offered by Coq, and show that it facilitates the discovery and the presentation of the results.     

Syntactic Type Soundness Results for the Region Calculus

The region calculus of Tofte and Talpin is a polymorphically typed lambda calculus with annotations that make memory allocation and deallocation explicit. It is intended as an intermediate language for implementing Hindley-Milner typed functional languages such as ML without traditional trace-based garbage collection. Static region and effect inference can be used to annotate a statically typed ML program with memory management primitives. Soundness of the calculus with respect to the region and effect system is crucial to guarantee safe deallocation of regions, i.e., deallocation should only take place for objects which are provably dead. The original soundness proof by Tofte and Talpin requires a complex co-inductive safety relation. In this paper, we present two small-step operational semantics for the region calculus and prove their type soundness with respect to the region and effect system. Following the standard syntactic approach of Wright, Felleisen, and Harper, we obtain simple inductive proofs. The first semantics is store-less. It is simple and elegant and gives rise to perspicuous proofs. The second semantics provides a store-based model for the region calculus. Albeit slightly more complicated, its additional expressiveness allows us to model operations on references with destructive update. A pure fragment of both small-step semantics is then proven equivalent to the original big-step operational approach of Tofte and Talpin. This leads to an alternative soundness proof for their evaluation-style formulation.     

Matrix Code

Matrix Code gives imperative programming a mathematical semantics and heuristic power comparable in quality to functional and logic programming. A program in Matrix Code is developed incrementally from a specification in pre/post-condition form. The computations of a code matrix are characterized by powers of the matrix when it is interpreted as a transformation in a space of vectors of logical conditions. Correctness of a code matrix is expressed in terms of a fixpoint of the transformation. The abstract machine for Matrix Code is the dual-state machine, which we present as a variant of the classical finite-state machine.     

一个机器检测的Micro-Dalvik虚拟机模型

给出了一个寄存器架构的虚拟机模型Micro-Dalvik,包括虚拟机指令集和虚拟机运行时状态的形式化,并以大步操作语义(big-step operational semantics)的方式给出了指令单步执行的状态转换以及定义在单步执行上的自反传递闭包来表达虚拟机程序的运行时状态转换.最后,以定理的形式描述了语义满足的性质,并得到证明.这个模型的指令集包括了大部分Dalvik虚拟机指令,为获得形式语义的清晰化,它在Dalvik VM指令集上进行了必要的抽象,对其实质没有改变,因而具有较大的实用性.该形式化模型通过了定理证明助手Isabelle/HOL的验证.     

Trace-Based Abstract Interpretation of Operational Semantics

We present trace-based abstract interpretation, a unification of severallines of research on applying Cousot-Cousot-style abstract interpretation a.i. tooperational semantics definitions (such as flowchart, big-step, and small-step semantics)that express a programs semantics as a concrete computation tree of trace paths. Aprograms trace-based a.i. is also a computation tree whose nodes contain abstractions ofstate and whose paths simulate the paths in the programs concrete computation tree.Using such computation trees, we provide a simple explanation of the central concept of collecting semantics, and we distinguish concrete from abstract collectingsemantics and state-based from path-based collecting semantics. We also expose therelationship between collecting semantics extraction and results garnered from flow-analytic and model-checking-based analysis techniques. We adapt concepts fromconcurrency theory to formalize safe and live a.i.s for computation trees; in particular, coinduction techniques help extend fundamental results to infinite computation trees.Problems specific to the various operational semantics methodologies are discussed: Big-step semantics cannot express divergence, so we employ a mixture of induction andcoinduction in response; small-step semantics generate sequences of programconfigurations unbounded in size, so we abstractly interpret source language syntax.Applications of trace-based a.i. to data-flow analysis, model checking, closure analysis,and concurrency theory are demonstrated.     

A syntactic theory of sequential control

Sequential control operators like J and call/cc are often found in implementations of the λ-calculus as a programming language. Their semantics is always defined by the evaluation function of an abstract machine. We show that, given such a machine semantics, one can derive an algebraic extension of the λ_υ-calculus. The extended calculus satisfies the diamond property and contains a Church-Rosser subcalculus. This underscores that the interpretation of control operators is to a certain degree independent of a specific evaluation strategy. We also prove a standardization theorem and use it to investigate the correspondence between the machine and the calculus. Together, the calculus and the rewriting machine form a syntactic theory of control, which provides a natural basis for reasoning about programs with nonfunctional control operators.     

A compact fixpoint semantics for term rewriting systems

This work is motivated by the fact that a “compact” semantics for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many “semantically useless” elements that can be retrieved from a smaller set of terms. Therefore, in this article, we present a compressed, goal-independent collecting fixpoint semantics that contains the smallest set of terms that are sufficient to describe, by semantic closure, all possible rewritings. We prove soundness and completeness under ascertained conditions. The compactness of the semantics makes it suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step. To support this claim we report several experiments performed with a prototypical implementation.     

Abstract interpretation of resolution-based semantics

We extend the abstract interpretation point of view on context-free grammars by Cousot and Cousot to resolution-based logic programs and proof systems. Starting from a transition-based small-step operational semantics of Prolog programs (akin to the Warren Machine), we consider maximal finite derivations for the transition system from most general goals. This semantics is abstracted by instantiation to terms and furthermore to ground terms, following the so-called c- and s-semantics approach. Orthogonally, these sets of derivations can be abstracted to SLD-trees, call patterns and models, as well as interpreters providing effective implementations (such as Prolog). These semantics can be presented in bottom–up fixpoint form. This abstract interpretation-based construction leads to classical bottom–up semantics (such as the s-semantics of computed answers, the c-semantics of correct answers of Keith Clark, and the minimal-model semantics of logical consequences of Maarten van Emden and Robert Kowalski). The approach is general and can be applied to infinite and top–down semantics in a straightforward way.     

Contextual Labelled Semantics for Higher-order Process Calculi

In this paper, we study a contextual labelled transition semantics for Higher-Order process calculi. The labelled transition semantics are relatively clean and simple, and corresponding bisimulation equivalence can be easily formulated based on it. Besides we develop a novel approach to reason about behaviours of a higher-order substituted process P{Q/X}, based on which we can directly prove a very important result – factorisation theorem. To show the correspondence between our semantics and the well-established ones, we characterize our bisimulation in a version of barbed equivalence.     

An Observation Approach to the Semantics of Agent Communication Languages

We show how a formal framework for the observation issue in computer systems can be used for the specification of an agent behavior, abstracting away from agent inner details while focusing on its interactive behavior. This model can also be used as a specification of agent communication languages (ACLs), providing the proper abstraction level to represent the conditions causing an agent to send a message, as well as its effect on the receiving agent. In particular, this approach generalizes upon existing ACL semantics, such as FIPA ACL, that relate agent communicative acts to the agent mental state. Since the observation framework induces a more abstract architecture than other known approaches, our semantics are likely to be applicable to a wider set of agent architectures, thus better supporting standardization aims. Some application examples are shown, describing how various aspects of ACL semantics can be specified within our framework.     

On generic context lemmas for higher-order calculi with sharing

This paper proves several generic variants of context lemmas and thus contributes to improving the tools for observational semantics of deterministic and non-deterministic higher-order calculi that use a small-step reduction semantics. The generic (sharing) context lemmas are provided for may- as well as two variants of must-convergence, which hold in a broad class of extended process- and extended lambda calculi, if the calculi satisfy certain natural conditions. As a guide-line, the proofs of the context lemmas are valid in call-by-need calculi, in call-by-value calculi if substitution is restricted to variable-by-variable and in process calculi like variants of the $\pi$-calculus. For calculi employing beta-reduction using a call-by-name or call-by-value strategy or similar reduction rules, some iu-variants of ciu-theorems are obtained from our context lemmas. Our results reestablish several context lemmas already proved in the literature, and also provide some new context lemmas as well as some new variants of the ciu-theorem. To make the results widely applicable, we use a higher-order abstract syntax that allows untyped calculi as well as certain simple typing schemes. The approach may lead to a unifying view of higher-order calculi, reduction, and observational equality.     

Natural Semantics-Directed Generation of Compilers and Abstract Machines

In this paper we present the motivation, theory and transformations of our semantics-directed compiler generator. The main novelty of our generator is that it generates compilers and abstract machines. The execution times of the abstract machine programs produced by our generated compiler compare well to those of target programs produced by compilers generated by other semantics-directed generators. The generated specifications of compilers and abstract machines are suitable as a starting point for handwriting compilers and abstract machines. Our generator is fully automated and its core transformations are proved correct. Received May 1997 / Accepted in revised form May 2000     

Towards a theory of bisimulation for the higher-order process calculi

In this paper, a labelled transition semantics for higher-order process calculi is studied. The labelled transition semantics is relatively clean and simple, and corresponding bisimulation equivalence can be easily formulated based on it. And the congruence properties of the bisimulation equivalence can be proved easily. To show the correspondence between the proposed semantics and the well-established ones, the bisimulation is characterized as a version of barbed equivalence and a version of context bisimulation.     

Distributed quantum programming

In this paper we explore the structure and applicability of the Distributed Measurement Calculus (DMC), an assembly language for distributed measurement-based quantum computations. We describe the formal language’s syntax and semantics, both operational and denotational, and state several properties that are crucial to the practical usability of our language, such as equivalence of our semantics, as well as compositionality and context-freeness of DMC programs. We show how to put these properties to use by constructing a composite program that implements distributed controlled operations, in the knowledge that the semantics of this program does not change under the various composition operations. Our formal model is the basis of a quantum virtual machine construction for distributed quantum computations, which we elaborate upon in the latter part of this work. This virtual machine embodies the formal semantics of DMC such that programming execution no longer needs to be analysed by hand. Far from a literal translation, it requires a substantial concretisation of the formal model at the level of data structures, naming conventions and abstraction mechanisms. At the same time we provide automatisation techniques for program specification where possible to obtain an expressive and user-friendly programming environment.