This document is also available as
Towards Compatible and Interderivable Semantic Specifications
for the Scheme Programming Language, Part I: Denotational Semantics, Natural
Semantics, and Abstract Machines.
Abstract: We derive two big-step abstract machines, a natural
semantics, and the valuation function of a denotational semantics based on
the small-step abstract machine for Core Scheme presented by Clinger at
PLDI'98. Starting from a functional implementation of this small-step
abstract machine, (1) we fuse its transition function with its driver loop,
obtaining the functional implementation of a big-step abstract machine; (2)
we adjust this big-step abstract machine so that it is in defunctionalized
form, obtaining the functional implementation of a second big-step abstract
machine; (3) we refunctionalize this adjusted abstract machine, obtaining the
functional implementation of a natural semantics in continuation style; and
(4) we closure-unconvert this natural semantics, obtaining a compositional
continuation-passing evaluation function which we identify as the functional
implementation of a denotational semantics in continuation style. We then
compare this valuation function with that of Clinger's original denotational
semantics of Scheme.
An Investigation of Abadi and Cardelli's Untyped Calculus of
Abstract: We study the relationship between the natural
(big-step) semantics and the reduction (small-step) semantics of Abadi and
Cardelli's untyped calculus of objects. By applying Danvy et al.'s functional
correspondence to the natural semantics, we derive an abstract machine for
this calculus, and by applying Danvy et al.'s syntactic correspondence to the
reduction semantics, we also derive an abstract machines for this calculus.
These two abstract machines are identical. The fact that the machines are
identical, and the fact that they have been derived using meaning-preserving
program transformations, entail that the derivation constitutes a proof of
equivalence between natural semantics and the reduction semantics. The
derivational nature of our proof contrasts with Abadi and Cardelli's
soundness proof, which was carried out by pen and paper. We also note that
the abstract machine is new.
To move closer to actual language
implementations, we reformulate the calculus to use explicit substitutions.
The reformulated calculus is new. By applying the functional and syntactic
correspondences to natural and reduction semantics of this new calculus, we
again obtain two abstract machines. These two machines are also identical,
and as such, they establish the equivalence of the natural semantics and the
reduction semantics of the new calculus.
Finally, we prove that the
two abstract machines are strongly bisimilar. Therefore, the two calculi are
Olivier Danvy and Jacob Johannsen.
Inter-Deriving Semantic Artifacts for Object-Oriented
ii+13 pp. Extended version of a paper to appear in WoLLIC 2008.
Abstract: We present a new abstract machine for Abadi and
Cardelli's untyped calculus of objects. What is special about this semantic
artifact (i.e., man-made construct) is that is 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. This abstract machine therefore embodies the
soundness of Abadi and Cardelli's reduction semantics and natural semantics
relative to each other.
To move closer to actual implementations,
which use environments rather than actual substitutions, we then represent
object methods as closures and in the same inter-derivational spirit, we
present three new semantic artifacts: a reduction semantics for a version of
Abadi and Cardelli's untyped calculus of objects with explicit substitutions,
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 furthermore, they are coherent
with the previous ones since as we show, the two abstract machines are
bisimilar. Overall, though, the significance of these artifacts lies in them
not having been designed from scratch and then proved correct: instead, they
were mechanically inter-derived.
Olivier Danvy and Kevin Millikin.
Refunctionalization at Work.
ii+25 pp. To appear in Science of Computer Programming. A
preliminary version is available as the research report BRICS RS-07-7.
Abstract: We present the left inverse of Reynolds's
defunctionalization and we show its relevance to programming and to
programming languages. We propose two methods to transform a program that is
almost in defunctionalized form into one that is actually in defunctionalized
form, and we illustrate them with a recognizer for Dyck words and with
Dijkstra's shunting-yard algorithm.
A Study of Syntactic and Semantic Artifacts and its Application
to Lambda Definability, Strong Normalization, and Weak Normalization in the
Presence of State.
Abstract: Church's lambda-calculus underlies the syntax (i.e.,
the form) and the semantics (i.e., the meaning) of functional programs. This
thesis is dedicated to studying man-made constructs (i.e., artifacts) in the
lambda calculus. For example, one puts the expressive power of the lambda
calculus to the test in the area of lambda definability. In this area, we
present a course-of-value representation bridging Church numerals and Scott
numerals. We then turn to weak and strong normalization using Danvy et al.'s
syntactic and functional correspondences. We give a new account of Felleisen
and Hieb's syntactic theory of state, and of abstract machines for strong
normalization due to Curien, Crégut, Lescanne, and Kluge.
Gudmund Skovbjerg Frandsen and Piotr
Dynamic Normal Forms and Dynamic Characteristic Polynomial.
21 pp. To appear in ICALP '08.
Abstract: We present the first fully dynamic algorithm for
computing the characteristic polynomial of a matrix. In the generic symmetric
case our algorithm supports rank-one updates in randomized
time and queries in constant time, whereas in the general case the algorithm
randomized time, where is the number of
invariant factors of the matrix. The algorithm is based on the first dynamic
algorithm for computing normal forms of a matrix such as the Frobenius normal
form or the tridiagonal symmetric form. The algorithm can be extended to
solve the matrix eigenproblem with relative error in additional
time. Furthermore, it can be used to dynamically maintain
the singular value decomposition (SVD) of a generic matrix. Together with the
algorithm the hardness of the problem is studied. For the symmetric case we
present an lower bound for rank-one updates and an
lower bound for element updates.
Static Analysis for Event-Based XML Processing.
23 pp. Appears in PLAN-X '08.
Abstract: Event-based processing of XML data - as exemplified
by the popular SAX framework - is a powerful alternative to using W3C's DOM
or similar tree-based APIs. The event-based approach is particularly superior
when processing large XML documents in a streaming fashion with minimal
This paper discusses challenges for creating
program analyses for SAX applications. In particular, we consider the problem
of statically guaranteeing that a given SAX program always produces only
well-formed and valid XML output. We propose an analysis technique based on
existing analyses of Servlets, string operations, and XML graphs.