Publications
dblp
On the Learnability of Programming Language Semantics
ICE 2017
10th Interaction and Concurrency Experience
June 21-22, 2017, Neuchâtel, Switzerland.
with Khulood Alyahya.
abstract
pdf
Game semantics is a powerful method of semantic analysis for programming languages.
It gives mathematically accurate models (“fully abstract”) for a wide variety of programming languages.
Game semantic models are combinatorial characterisations of all possible interactions
between a term and its syntactic context. Because such interactions can be concretely
represented as sets of sequences, it is possible to ask whether they can be learned from examples.
Concretely, we are using long short-term memory neural nets (LSTM), a technique which
proved effective in learning natural languages for automatic translation and text synthesis,
to learn game-semantic models of sequential and concurrent versions of Idealised Algol (IA),
which are algorithmically complex yet can be concisely described. We will measure how accurate the
learned models are as a function of the degree of the term and the number of free variables involved.
Finally, we will show how to use the learned model to perform latent semantic
analysis between concurrent and sequential Idealised Algol.
Diagrammatic Semantics for Digital Circuits
CSL 2017
Computer Science Logic 2017, Stockholm, Sweden, August 20-24.
With Achim Jung and Aliaume Lopez.
abstract
pdf
We introduce a general diagrammatic theory of digital circuits, based on connections between
monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling
a foundational gap in reasoning syntactically and symbolically about a large class of digital
circuits (discrete values, discrete delays, feedback). This complements the dominant approach to
circuit modelling, which relies on simulation. The main advantage of our symbolic approach is
the enabling of automated reasoning about parametrised circuits, with a potentially interesting
new application to partial evaluation of digital circuits. Relative to the recent interest and
activity in categorical and diagrammatic methods, our work makes several new contributions.
The most important is establishing that categories of digital circuits are Cartesian and admit,
in the presence of feedback expressive iteration axioms. The second is producing a general yet
simple graph-rewrite framework for reasoning about such categories in which the rewrite rules
are computationally efficient, opening the way for practical applications.
The Dynamic Geometry of Interaction Machine:
A Call-by-Need Graph Rewriter
CSL 2017
Computer Science Logic 2017, Stockholm, Sweden, August 20-24.
With Koko Muroya.
abstract
pdf
Girard's Geometry of Interaction (GoI), a semantics designed for linear logic proofs, has been also
successfully applied to programming languages. One way is to use abstract machines that pass a
token in a fixed graph, along a path indicated by the GoI. These token-passing abstract machines
are space efficient, because they handle duplicated computation by repeating the same moves of
a token on the fixed graph. Although they can be adapted to obtain sound models with regard
to the equational theories of various evaluation strategies for the lambda calculus, it can be at
the expense of significant time costs. In this paper we show a token-passing abstract machine
that can implement evaluation strategies for the lambda calculus, with certified time efficiency.
Our abstract machine, called the Dynamic GoI Machine (DGoIM), rewrites the graph to avoid
replicating computation, using the token to find the redexes. The flexibility of interleaving token
transitions and graph rewriting allows the DGoIM to balance the trade-off of space and time costs.
This paper shows that the DGoIM can implement call-by-need evaluation for the lambda calculus
by using a strategy of interleaving token passing with as much graph rewriting as possible. Our
quantitative analysis confirms that the DGoIM with this strategy of interleaving the two kinds
of possible operations on graphs can be classified as “efficient” following Accattoli’s taxonomy of
abstract machines.
Categorical Semantics of Digital Circuits.
FMCAD 2016,
Formal Methods in Computer-Aided Design
3-6 October, 2016
Mountain View, CA, USA.
With Achim Jung
abstract
pdf
This paper proposes a categorical theory of digital
circuits based on monoidal categories and graph rewriting. The
main goal of this paper is conceptual: to fill a foundational gap
in reasoning about digital circuits, which is currently almost
exclusively semantic (simulations). The level of abstraction we
target is circuits with discrete signal levels, discrete time, and
explicit delays, which is appropriate for modelling a range of
components such as boolean gates or transistors working in
saturation mode.
We start with an algebraic signature consisting of the basic
electronic components of a given class of circuits and extend
it gradually (and in a free way) with further algebraic structure
(representing circuit combinations, delays, and feedback), while
quotienting it with a notion of equivalence corresponding to
input-output observability. Using well-known results about the
correspondence between free monoidal categories and graphlike
structures we can develop, in a principled way, a graph
rewriting system which is shown to be useful in reasoning about
such circuits. We illustrate the power of our system by reasoning
equationally about a challenging class of circuits: combinational
circuits with feedback.
Leaving the Nest: Nominal Techniques for Variables with Interleaving Scopes.
CSL 2015,
Computer Science Logic 2015, Berlin, 7-10 September 2015
Technische Universität Berlin.
With Murdoch James Gabbay, Daniela Petrisan
abstract
doi
We examine the key syntactic
and semantic aspects of a nominal framework allowing scopes of name
bindings to be arbitrarily interleaved. Name binding (e.g. delta x.M) is handled by explicit name-creation and name-destruction brackets (e.g. ) which admit interleaving. We define an appropriate notion of alpha-equivalence for such a language and study the syntactic structure required for alpha-equivalence to be a congruence. We develop denotational and categorical semantics for dynamic binding and provide a generalised nominal inductive reasoning principle. We give several standard synthetic examples of working with dynamic sequences (e.g. substitution) and we sketch out some preliminary applications to game semantics and trace semantics.
Transparent linking of compiled software and synthesized hardware.
DATE 2015,
Design, Automation, and Test in Europe 2015.
With David B. Thomas, Shane T. Fleming, George A. Constantinides
abstract
doi
System-level Linking of Synthesised Hardware and Compiled Software Using a Higher-order Type System.
FPGA 2015,
23rd ACM/SIGDA International Symposium on Field-Programmable Gate Arrays.
With Shane T. Fleming, David B. Thomas, George A. Constantinides
abstract
doi
Devices with tightly coupled CPUs and FPGA logic allow for the implementation of heterogeneous applications which combine multiple components written in hardware and software languages, including first-party source code and third-party IP. Flexibility in component relationships is important, so that the system designer can move components between software and hardware as the application design evolves. This paper presents a system-level type system and linker, which allows functions in software and hardware components to be directly linked at link time, without requiring any modification or recompilation of the components. The type system is designed to be language agnostic, and exhibits higher-order features, to enables design patterns such as notifications and callbacks to software from within hardware functions. We demonstrate the system through a number of case studies which link compiled software against synthesised hardware in the Xilinx Zynq platform.
Compiling Higher Order Functional Programs to Composable Digital Hardware
FCCM 2014,
The 22nd IEEE International Symposium on
Field-Programmable Custom Computing Machines
May 11-13, Boston, Massachusetts.
With Eduardo Aguilar-Pelaez, Samuel Bayliss, Alex I. Smith, Felix Winterstein, David B. Thomas, George A. Constantinides
abstract
doi
This work demonstrates the capabilities of a high-level synthesis tool-chain that allows the compilation of higher order functional programs to gate-level hardware descriptions. Higher order programming allows functions to take functions as parameters. In a hardware context, the latency-insensitive interfaces generated between compiled modules enable late-binding with libraries of pre-existing functions at the place-and-route compilation stage. We demonstrate the completeness and utility of our approach using a case study; a recursive k-means clustering algorithm. The algorithm features complex data-dependent control flow and opportunities to exploit both coarse and fine-grained parallelism.
Towards native higher-order remote procedure calls
IFL 2014,
The 26th Symposium on Implementation and Application of Functional Languages.
With Olle Fredriksson and Bertie Wheen
abstract
pdf
We present a new abstract machine, called DCESH, which models the
execution of higher-order programs running in distributed
architectures. DCESH implements a native general remote higher-order
function call across node boundaries. It is a modernised version of
SECD enriched with specialised communication features required for
implementing the remote procedure call mechanism. The key correctness
result is that the termination behaviour of the remote procedure call
is indistinguishable (bisimilar) to that of a local call. The
correctness proofs and the requisite definitions for DCESH and other
related abstract machines are formalised using Agda. We also formalise
a generic transactional mechanism for transparently handling failure
in DCESHs. We use the DCESH as a target architecture for compiling a
conventional call-by-value functional language ("Floskel") which can
be annotated with node information. Conventional benchmarks show that
the single-node performance of Floskel is comparable to that of OCaml,
a semantically similar language, and that distribution overheads are
not excessive.
Krivine nets: a semantic foundation for distributed execution
ICFP 2014,
The 19th ACM SIGPLAN International Conference on Functional Programming.
With Olle Fredriksson
abstract
pdf
We define a new approach to compilation to distributed
architectures based on networks of abstract machines. Using it we
can implement a generalised and fully transparent form of Remote
Procedure Call that supports calling higher-order functions across
node boundaries, without sending actual code. Our starting point is
the classic Krivine machine, which implements reduction for untyped
call-by-name PCF. We successively add the features that we need for
distributed execution and show the correctness of each addition.
Then we construct a two-level operational semantics, where the high
level is a network of communicating machines, and the low level is
given by local machine transitions. Using these networks, we arrive
at our final system, the \emph{Krivine Net}. We show that Krivine
Nets give a correct distributed implementation of the Krivine
machine, which preserves both termination and non-termination
properties. All the technical results have been formalised and
proved correct in \textsc{Agda}. We also implement a prototype
compiler which we compare with previous distributing compilers based on
Girard's Geometry of Interaction and on Game Semantics.
Bounded Linear Types in a Resource Semiring
ESOP 2014,
23rd European Symposium on Programming, Grenoble, France.
With Alex Smith
abstract
pdf
Bounded linear types have proved to be useful for automated resource analysis and control in functional programming languages. In this paper we introduce a bounded linear typing discipline on a general notion of resource which can be modeled in a semiring. For this type system we provide both a general type-inference procedure, parameterized by the decision procedure of the semiring equational theory, and a (coherent) categorical semantics. This could be a useful type-theoretic and denotational framework for resource-sensitive compilation, and it represents a generalization of several existing type systems. As a nontrivial instance, motivated by hardware compilation, we present a complex new application to calculating and controlling timing of execution in a (recursion-free) higher-order functional programming language with local store.
Abstract machines for game semantics, revisited
LICS
2013, Twenty-Eight Annual IEEE
Symposium on Logic in Computer Science, New Orleans, Louisiana, USA. With Olle Fredriksson.
abstract
pdf
In this paper we define new abstract machines for
game semantics which correspond to networks of conventional
computers, and which can be used as an intermediate representation
for distributed compilation. This is achieved in two
steps. First we introduce the HRAM, a Heap and Register
Abstract Machine, an abstraction of a conventional computer,
which can be structured into HRAM nets, an abstract point-topoint
network model. HRAMs are multi-threaded and subsume
communication by tokens (cf. IAM) or jumps (cf. JAM). Game
Abstract Machines (GAM), are HRAMs with additional structure
at the interface level, but no special operational capabilities. We
show that GAMs cannot be naively composed, but composition
must be mediated using special HRAM combinators. HRAMs are
flexible enough to allow the representation of game models for
languages with state (non-innocent games) or concurrency (non-alternating
games). We illustrate the potential of this technique
by implementing a toy distributed compiler for ICA, a higher-order
programming language with shared state concurrency, thus
significantly extending our previous distributed PCF compiler.
We show that compilation is sound and memory-safe, i.e. no
(distributed or local) garbage collection is necessary.
Diagrammatic Reasoning for Delay-Insensitive Asynchronous
Circuits
Samson Abramsky Festchrift (forthcoming)
abstract
pdf
In this paper we construct a new trace model of delay-insensitive
asynchronous circuits inspired by Ebergen's model in such a way that
it satisfies the compositional properties of a category, with
additional monoidal structure and further algebraic properties. These
properties taken together lay a solid mathematical foundation for a
diagrammatic approach to reasoning about asynchronous circuits, which
represents a formalisation of common intuitions about asynchronous
circuits and their properties.
Seamless distributed computing from the Geometry of Interaction
TGC
2012. 7th International Symposium on Trustworthy Global
Computing Newcastle upon Tyne, UK, 7-8 September 2012 With
O. Fredriksson.
abstract
pdf
In this paper we present a seamless approach to writing and compiling
distributed code. By "seamless" we mean that the syntax and semantics
of the distributed program remain the same as if it was executed on
one node only, except for label annotations indicating on what node
sub-terms of the program are to be executed. There are no restrictions
on how node labels are to be assigned to sub-terms. We show how the
paradigmatic (higher-order functional recursive) programming language
PCF, extended with node annotations, can be used for this purpose. The
compilation technique is directly inspired by game semantics and the
Geometry of Interaction.
Coherent Minimisation: Towards efficient tamper-proof
compilation
ICE
2012. 5th Interaction and Concurrency Experience Workshop.
Stockholm, Sweden June 16, 2012. With Z. Al-Zobaidi.
abstract
pdf
Automata representing game-semantic models of programs are meant to
operate in environments whose input-output behaviour is constrained by
the rules of a game. This can lead to a notion of equivalence between
states which is weaker than the conventional notion of bisimulation,
since not all actions are available to the environment. An environment
which attempts to break the rules of the game is, effectively,
mounting a low-level attack against a system. In this paper we show
how (and why) to enforce game rules in games-based hardware synthesis
and how to use this weaker notion of equivalence, called coherent
equivalence, to aggressively minimise automata.
Game semantics in the nominal model
MFPS
2012. The Twenty-eighth Conference on the Mathematical
Foundations of Programming Semantics, University of Bath, Bath, UK,
June 6-9, 2012. With J. Gabbay.
abstract
pdf
We present a model of games based on nominal sequences, which
generalise sequences with atoms and a new notion
of coabstraction. This gives a new, precise, and compositional
mathematical treatment of justification pointers in game
semantics.
A System-Level Game Semantics
MFPS
2012. The Twenty-eighth Conference on the Mathematical
Foundations of Programming Semantics, University of Bath, Bath, UK,
June 6-9, 2012. With N. Tzevelekos.
abstract
pdf
Game semantics is a trace-like denotational semantics for
programming languages where the notion of legal observable behaviour
of a term is defined combinatorially, by means of rules of a game
between the term (the Proponent) and its context (the Opponent). In
this game the term is conventionally considered the Proponent and
the context the Opponent. In general, the richer the computational
features a language has the less constrained the rules of the
semantic game. In this paper we consider the consequences of taking
this relaxation of rules to the limit, by granting the Opponent
omnipotence, that is, permission to play any move without
combinatorial restrictions. However, we impose an epistemic
restriction by not granting Opponent omniscience, so that Proponent
can have undisclosed secret moves. We introduce a basic C-like
programming language and we define such a semantic model for it. We
argue that the resulting semantics is an appealingly simple
combination of operational and game semantics and we show how
certain traces explain system-level attacks, i.e.~plausible attacks
that are realisable outside of the programming language itself. We
also show how allowing {Proponent} to have secrets ensures that some
desirable equivalences in the programming language are preserved.
Game semantics is a trace-like denotational semantics for
programming languages where the notion of legal observable behaviour
of a term is defined combinatorially, as rules of a game between the
term and its context. In this game the term is conventionally
considered the Proponent and the context the Opponent. In general,
the richer the computational features a language has the less
constrained the rules of the semantic game. In this paper we
consider the consequences of taking this relaxation of rules to the
limit, by granting the Opponent omnipotence. This Opponent is
allowed to play any move, without combinatorial
restrictions. However, we will impose an epistemic restriction by
not granting Opponent omniscience, so that Proponent can have
undisclosed secret moves that Opponent cannot play. This is broadly
inspired by the Dolev-Yao attacker model of security. For the sake
of staying focussed in our presentation we introduce a simple C-like
programming language and we define such a semantic model for it. We
argue that the resulting semantics is an appealingly simple
combination of operational and game semantics and we explain how
certain inequivalences can be interpreted as system-level attacks,
i.e. attacks that are only realizable outside of the programming
language itself. We will also show how allowing Proponent to have
secrets ensures that some desirable equivalences in the programming
language are preserved.
Geometry of Synthesis IV: Compiling affine recursion into static
hardware
ICFP
2011. The 16th ACM SIGPLAN International Conference on
Functional Programming, Tokyo, Japan, September 19-21, 2011. With
S. Singh and A. Smith.
abstract
pdf
doi
Abramsky's Geometry of Interaction interpretation (GoI) is a
logical-directed way to reconcile the process and functional views
of computation, and can lead to a dataflow-style semantics of
programming languages that is both operational (i.e.\ effective) and
denotational (i.e.\ inductive on the language syntax). The key idea
of Ghica's Geometry of Synthesis (GoS) approach is that for certain
programming languages (namely Reynolds's affine Syntactic Control of
Interference--SCI) the GoI processes-like interpretation of the
language can be given a finitary representation, for both internal
state and tokens. A physical realisation of this representation
becomes a semantics-directed compiler for SCI into hardware. In this
paper we examine the issue of compiling affine recursive programs
into hardware using the GoS method. We give syntax and compilation
techniques for unfolding recursive computation in space or in time
and we illustrate it with simple benchmark-style examples. We
examine the performance of the benchmarks against conventional
CPU-based execution models.
Function Interface Models for Hardware Compilation (invited
tutorial paper)
MEMOCODE
2011. ACM/IEEE Ninth International Conference on Formal
Methods and Models for Codesign Cambridge, UK. July 11-13, 2011
abstract
pdf
doi
The problem of synthesis of gate-level descriptions of digital
circuits from behavioural speci?cations written in higher- level
programming languages (hardware compilation) has been studied for a
long time yet a definitive solution has not been forthcoming. The
emphasis of the first part of this tutorial is methodological, arguing
that one of the major obstacles in the way of hardware compilation
becoming a useful and mature technology is the lack of a well defined
function interface model, i.e. a canonical way in which functions
communicate with arguments. In the second part we present a solution
based on the Geometry of Synthesis, a semantics-directed approach to
hardware compilation.
Synchronous game semantics via round abstraction
FoSSaCS
2011. 14th International Conference on Foundations of
Software Science and Computation Structures. With Mohamed Menaa.
abstract
pdf
doi
A synchronous game semantics (one in which several moves may happen
simultaneously) is derived from a conventional (sequential) game
semantics using a round abstraction algorithm. We choose the
programming language Syntactic Control of Interference and
McCusker's fully abstract relational model as a convenient starting
point and derive a synchronous game model first by refining the
relational semantics into a trace semantics, then applying a round
abstraction to it. We show that the resulting model is sound but not
fully abstract. This work is practically motivated by applications
to hardware synthesis via game semantics.
Geometry of Synthesis III: Resource management through type
inference
POPL 2011. 38th
Symposium on Principles of Programming Languages, Austin, Texas. With
Alex Smith.
abstract
pdf
doi
"Geometry of Synthesis" is a technique for compiling higher-level
programming languages into digital circuits via their game semantic
model. Ghica first presented the key idea, then we gave a provably
correct compiler into asynchronous circuits for Syntactic Control of
Interference (SCI), an affine-typed version of Reynolds's Idealized
Algol. Affine typing has the dual benefits of ruling out race
conditions through the type system and having a finite-state
game-semantic model for any term, which leads to a natural circuit
representation and simpler correctness proofs. In this paper we go
beyond SCI to full Idealized Algol, enhanced with shared-memory
concurrency and semaphores. Compiling ICA proceeds in three
stages. First, an intermediate type system called Syntactic Control
of Concurrency (SCC) is used to statically determine "concurrency
bounds" on all identifiers in the program. Then, a program
transformation called "serialization" is applied to the program to
translate it into an equivalent SCC program in which all concurrency
bounds are set to the unit. Finally, the resulting program can be
then compiled into asynchronous circuits using a slightly enhanced
version of the GoS II compiler, which can handle assignable
variables used in non-sequential contexts.
On the compositionality of round abstraction
CONCUR 2010. 21st International Conference on
Concurrency Theory, Paris, France. With Mohamed Nabih Menaa.
abstract
pdf
doi
We revisit Alur and Henzinger's "round abstraction" technique as a
solution to the problem of implementing a low-latency synchronous
process from an asynchronous specification. We use a trace-semantic
setting akin to Interaction Categories [Abramsky et. al.], which is
also a generalisation of pointer-free game semantic models. We define
partial and total correctness for round abstraction relative to
composition and we note that in its most general case round
abstraction can lead to incorrect behaviour. We identify sufficient
properties to guarantee partially correct composition, then we present
a framework for round abstraction that is totally correct when applied
to asynchronous behaviours. We apply this technique to implementing a
hardware compiler from (asynchronous) concurrent programming languages
to low-latency synchronous digital circuits via game semantics.
Geometry of Synthesis II: From Games to Delay-Insensitive
Circuits
MFPS 26.
Mathematical Foundations of Programming Semantics XXVI, Ottawa,
Canada. Electronic Notes in Theoretical Computer Science (ENTCS).
With Alex Smith.
abstract
pdf
doi
In this paper we extend previous work on the compilation of
higher-order imperative languages into digital circuits. We introduce
concurrency, an essential feature in the context of hardware
compilation, and we use an existing game model to simplify proofs of
soundness and adequacy. The synthesised circuits are asynchronous,
more precisely they are the "event logic" circuits introduced by
Sutherland to implement micropipelines, matching more directly the
game model, which is itself asynchronous.
Data-Abstraction Refinement: A Game Semantic Approach
STTT.
International Journal on Software Tools for Technology Transfer.
Volume 12, Number 5, 373-389. With
Adam Bakewell, Aleks Dimovski and Ranko Lazic.
abstract
pdf
doi
This paper presents a semantic framework for data abstraction and
refinement for verifying safety properties of open programs with
integer types. The presentation is focused on an Algol-like
programming language that incorporates data abstraction in its type
system. We use a fully abstract game semantics in the style of
Hyland and Ong and a more intensional version of the model that
tracks nondeterminism introduced by abstraction in order to detect
false counterexamples. These theoretical developments are
incorporated in a new model-checking tool, Mage, which implements
efficiently the data-abstraction refinement procedure using symbolic
and on-the-fly techniques.
Applications of Game Semantics: From Software Analysis to Hardware
Synthesis
LICS
2009 (invited tutorial paper), Twenty-Fourth Annual IEEE
Symposium on Logic in Computer Science, Los Angeles, California, USA.
abstract
pdf
doi
After informally reviewing the main concepts from game semantics and
placing the development of the field in a historical context we
examine its main applications. We focus in particular on finite
state model checking, higher order model checking and more recent
developments in hardware design.
Clipping: A Semantics-directed syntactic
approximation LICS
2009, Twenty-Fourth Annual IEEE Symposium on Logic in Computer
Science, Los Angeles, California, USA. With Adam Bakewell
abstract
pdf
doi
In this paper we introduce clipping, a new method of syntactic
approximation which is motivated by and works in conjunction with a
sound and decidable denotational model for a given programming
language. Like slicing, clipping reduces the size of the source code
in preparation for automatic verification; but unlike slicing it is an
imprecise but computationally inexpensive algorithm which does not
require a whole-program analysis. The technique of clipping can be
framed into an iterated refinement cycle to arbitrarily im prove its
precision. We first present this rather simple idea intuitively with
some examples, then work out the technical details in the case of an
Algol-lik e programming language and a decidable approximation of its
game-semantic model inspired by Hankin and Malacaria's lax functor
approach. We conclude by prese nting an experimental model checking
tool based on these ideas and some toy programs.
Compositional Predicate Abstraction from Game
Semantics TACAS
2009, Fifteenth International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, 2009, York,
UK. With Adam Bakewell
abstract
pdf
doi
We introduce a technique for using conventional predicate abstraction
methods to reduce the state-space of models produced using game
semantics. We focus on an expressive procedural language that has
both local store and local control, a language which enjoys a simple
game-semantic model yet is expressive enough to allow non-trivial
examples. Our compositional approach allows the verification of
incomplete programs (e.g. libraries) and offers the opportunity for
new heuristics for improved efficiency. Game-semantic predicate
abstraction can be embedded in an abstraction-refinement cycle in a
standard way, resulting in an improved version of our experimental
model-checking tool Mage, and we illustrate it with several toy
examples.
On-the-Fly Techniques for Games-Based Software Model
Checking TACAS
2008, Fourteenth International Conference on Tools and
Algorithms for the Construction and Analysis of Systems, 2008,
Budapest, Hungary. With Adam Bakewell
abstract
pdf
doi
We introduce on-the-fly composition, symbolic modelling and lazy
iterated approximation refinement for game-semantic models. We present
Mage, an experimental model checker implementing this new
technology. We discuss several typical examples and compare Mage with
Blast and GameChecker, which are the state-of-the-art tools in
on-the-fly software model checking, and game-based model checking.
Angelic Semantics of Fine-Grained
Concurrency First
Games for Logic and Programming Languages Workshop (Special
Issue), Annals of Pure and Applied Logic, Volume 151, Issues
2-3, February 2008, Pages 89-114. With Andrzej Murawski
abstract
pdf
doi
We introduce a game model for an Algol-like programming language with
primitives for parallel composition and synchronization on
semaphores. The semantics is based on a simplified version of
Hyland-Ong-style games and it emphasizes the intuitive connection
between the concurrent nature of games and that of computation. The
model is fully abstract for may-equivalence.
Geometry of Synthesis: A structured approach to VLSI
design POPL
2007, Symposium on Principles of Programming Languages Nice,
France January, 2007
abstract
pdf
doi
slides
We propose a new technique for hardware synthesis from higher-order
functional languages with imperative features based on Reynolds
Syntactic Control of Interference. The restriction on contraction in
the type system is useful for managing the thorny issue of sharing of
physical circuits. We use a semantic model inspired by game semantics
and the geometry of interaction, and express it directly as a certain
class of digital circuits that form a cartesian, monoidal-closed
category. A soundness result is given, which is also a correctness
result for the compilation technique.
Compositional Model
Extraction for Higher-Order Concurrent
Programs TACAS
2006, 12th International Conference on Tools and Algorithms for
the Construction and Analysis of Systems, Vienna, March 2006. With
A. Murawski
abstract
pdf
doi
The extraction of accurate finite-state models of higher-order or open
programs is a difficult problem. We show how it can be addressed using
newly developed game-semantic techniques and illustrate the solution
with a model-checking tool based on such techniques. The approach has
several important advantages over more traditional ones: precise
account of inter-procedural behaviour, concise procedure summaries and
surprising compactness of the extracted models.
A Counterexample-Guided Refinement Tool
for Open Procedural
Programs SPIN
2006, 13th International SPIN Workshop on Model Checking of
Software, Vienna, March 2006. With A. Dimovski and R. Lazić
abstract
pdf
We present a procedure for game-based model checking of an interesting
fragment of Idealised Algol. The procedure requires only that the user
state the safety property of interest. It than automatically generates
abstractions of open program fragment (i.e. term-in-context) using
iterative refinement. We have built a tool which implements the
procedure. Its effectiveness is evaluated on several examples.
Syntactic Control of
Concurrency Theoretical Computer Science, vol 350 (2-3),
7 February 2006, pp 234-251. With A. Murawski and L. Ong
abstract
ps pdf
doi
We consider a finitary procedural programming language (finite
data-types, no recursion) extended with parallel composition and
binary semaphores. Having first shown that may-equivalence of
second-order open terms is undecidable we set out to find a framework
in which decidability can be regained with minimum loss of
expressivity. To that end we define an annotated type system that
controls the number of concurrent threads created by terms and give a
fully abstract game semantics for the notion of equivalence induced by
typable terms and contexts. Finally, we show that the semantics of all
typable terms, at any order and in the presence of iteration, admits a
regular-language representation and thus the restricted observational
equivalence is decidable.
Data-Abstraction
Refinement: A Game Semantic
Approach SAS
2005, The 12th International Static Analysis Symposium,
London, September 2005. With A. Dimovski and R. Lazić
abstract
pdf
doi
This paper presents a semantic framework for data abstraction and
refinement for verifying safety properties of open programs. The
presentation is focused on an Algol-like programming language that
incorporates data abstraction in its syntax. The fully abstract game
semantics of the language is used for model-checking safety
properties, and an interaction-sequence-based semantics is used for
interpreting potentially spurious counterexamples and computing
refined abstractions for the next iteration. An implementation based
on the FDR model checker demonstrates practicality of the method.
Slot Games: A
quantitative model of
computation POPL
2005, 32nd Annual ACM SIGPLAN - SIGACT Symposium on Principles
of Programming Languages, Long Beach, California, January 2005
abstract
ps pdf
doi
We present a games-based denotational semantics for a quantitative
analysis of programming languages. We define a Hyland-Ong-style games
framework called slot games, which consists of HO games augmented with
a new action called token. We develop a slot-game model for the
language Idealized Concurrent Algol by instrumenting the strategies in
its HO game model with token actions. We show that the slot-game model
is a denotational semantics induced by a notion of observation
formalized in the operational theory of improvement of Sands, and we
give a full abstraction result. A quantitative analysis of programs
has many potential applications, from compiler optimizations to
resource-constrained execution and static performance profiling. We
illustrate several such applications with putative examples that would
be nevertheless difficult, if not impossible, to handle using known
operational techniques.
Syntactic Control of
Concurrency ICALP
2004, 31st International Colloquium on Automata, Languages and
Programming, Turku, Finland, July 2004. With A. Murawski and
L. Ong
abstract
pdf
doi
We consider a finitary procedural programming language (finite
data-types, no recursion) extended with parallel composition and
binary semaphores. Having first shown that may-equivalence of
second-order open terms is undecidable we set out to find a framework
in which decidability can be regained with minimum loss of
expressivity. To that end we define an annotated type system that
controls the number of concurrent threads created by terms and give a
fully abstract game semantics for the notion of equivalence induced by
typable terms and contexts. Finally, we show that the semantics of
all typable terms, at any order and in the presence of iteration,
admits a regular-language representation and thus the restricted
observational equivalence is decidable.
Nominal Games and
Full Abstraction for the
Nu-Calculus LICS
2004, Nineteenth Annual IEEE Symposium on Logic in Computer
Science, Turku, Finland, July 2004. With S. Abramsky,
A. Murawski, L. Ong and I. Stark
abstract
ps
doi
We introduce nominal games for modelling programming languages with
dynamically generated local names, as examplified by Pitts and Stark's
nu-calculus. Inspired by Pitts and Gabbay's recent work on nominal
sets, we construct arenas and strategies in the world (or topos) of
Fraenkel-Mostowski sets. This approach leads to a clean and precise
treatment of fresh names and standard game constructions that are
considered invariant under renaming. The main result is the
construction of the first fully-abstract model of for the nu-calculus
Applying Game
Semantics to Compositional Software Modeling and Verifications
TACAS 2004,
Tenth International Conference on Tools and Algorithms for the
Construction and Analysis of System, Barcelona, March 2004. With
S. Abramsky, A. Murawski and L. Ong
abstract
pdf
doi
We describe a software model checking tool founded on game semantics,
highlight the underpinning theoretical results and discuss several
case studies. The tool is based on an interpretation algorithm
defined compositionally on syntax and thus can also handle open
programs. Moreover, the models it produces are observationally fully
abstract. These features are essential in the modeling and
verification of software components such as modules and turn out to
lead to very compact models of programs.
Semantical Analysis
of Noninterference 3, An Operational
Approach ESOP
2004, The European Symposium on Programming, Barcelona,
March 2004
abstract
ps
doi
We are presenting a semantic analysis of Reynolds's specification
logic of Idealized Algol using the parametric operational techniques
developed by Pitts. We hope that this more elementary account will
make the insights of Tennent and O'Hearn, originally formulated in a
functor-category denotational semantics, more accessible to a wider
audience. The operational model makes clearer the special nature of
term equivalence in the logical setting, identifies some problems in
the previous interpretation of negation and also proves the soundness
of two new axioms of specification logic. Using the model we show
that even a very restricted fragment of specification logic is
undecidable.
Angelic Semantics
of Fine-Grained Concurrency Foundations of Software Science
and Computation
Structures, FOSSACS
2004, Barcelona, March 2004. With A. Murawski
abstract
ps
doi
We introduce a game model for a procedural programming language
extended with primitives for parallel composition and synchronization
on binary semaphores. The model uses an interleaved version of
Hyland-Ong-style games, where most of the original combinatorial
constraints on positions are replaced with a simple principle
naturally related to static process creation. The model is fully
abstract for may-equivalence.
A Games-Based
Foundation for Compositional Software Model Checking PhD Thesis,
Queen's University School of Computing, Kingston, Ontario, Canada,
November 2002
abstract
ps
pdf
doi
We present a program specification language for Idealized Algol that
is compatible both with inferential reasoning and model
checking. Model-checking is made possible by the use of an
algorithmic, regular-language semantics, which is a representation of
the fully-abstract game semantic model of the programming
language. Inferential reasoning is carried out using rules based on
Hoare's logic of imperative programming, extended to handle procedures
and computational side effects. The main logical innovation of this
approach is the use of generalized universal quantifiers to specify
properties of non-local objects. Together, the regular-language
semantics of the programming language and its specification language
on the one hand, and the inferential properties of the specification
language on the other provide a foundation for compositional software
model checking.
The Regular-Language
Semantics of First-order Idealized Algol
Theoretical Computer
ScienceVolume 309, Issues 1-3 , 2 December 2003, Pages
469-502. With Guy McCusker
abstract
ps pdf
doi
We explain how recent developments in game semantics can be applied to
reasoning about equivalence of terms in a non-trivial fragment of
Idealized Algol (IA) by expressing sets of complete plays as regular
languages. Being derived directly from the fully abstract game
semantics for IA, our model inherits its good theoretical properties;
in fact, for first order IA taken as a stand-alone language the
regular language model is fully abstract. The method is algorithmic
and formal, which makes it suitable for automation. We show how
reasoning is carried out using a meta-language of extended regular
expressions, a language for which equivalence is decidable.
A Regular-Language
Model for Hoare-Style Correctness Statements
VCL'2001, Florence, Italy
abstract
ps pdf
Two previous papers of the author show how finitary imperative
procedural languages can be modeled using regular languages only,
which are representation of fully abstract game models. This paper
examines the possibility of using these models as a basis for
model-checking Hoare-style partial correctness statements in such
languages.
Regular Language
Semantics for a Call-by-Value Programming Language
MFPS
17, (preliminary version) Aarhus, Denmark, 2001
abstract
ps
pdf
doi
We give a fully abstract regular language model for a first-order CBV
programming language, which is a representation of its fully abstract
game model.
Reasoning About
Idealized Algol Using Regular Languages
ICALP 2000 ,
Geneva, Switzerland. With Guy McCusker
abstract
ps
pdf
doi
We explain how we can reason about equivalence of terms in a
non-trivial fragment of IA by expressing sets of complete plays from
the game semantic model as regular languages. The model is fully
abstract, concrete and formal , which makes it uniquely suitable for
automation. We show how reasoning can be carried out in a
meta-language of regular expressions, for which equivalence is
decidable.
Abstract Models of
Storage,
Journal of Higher Order and Symbolic
Computation. With Robert D. Tennent
abstract
ps
pdf
A survey of the concept of state in programming languages.
Semantics of Dynamic
Variables in Algol-like Languages,
M.Sc. Thesis, 1997
abstract
ps
A functor-category semantics for pointers.
Copyright notice: This work is Copyrighted, and anybody
caught usin' it without our permission, will be mighty good friends of
ourn, cause we don't give a dern. We wrote it, that's all we wanted to
do. (Woody Guthrie)