Foundations of Programming Meetings
School of Computer Science and ITUniversity of Nottingham
The Foundations of Programming group holds regular research meetings. The meetings last around an hour, and are intended to be a friendly forum for discussion and exchange of ideas. Most meetings take the form of a talk by a group member or an invited speaker, but we also have various kinds of discussion sessions. The meetings are open to everyone, not just members of the group. Please contact Graham Hutton if you are interested in visiting the group and giving a talk.
Details of previous years meetings are also available: 1995; 1996; 1997; 1998; 1999; 2000.
Details of recent and upcoming meetings are given below.
Two of Gentzen's innovations, the sequent calculus and natural deduction, have superficial similarities, with their cut-elimination and normalisation theorems respectively ; but the former allows too many proofs and the latter is not well suited for automatic proof search.
We describe in this talk the sequent calculus of Herbelin
(CSL '94), for intuitionistic logic, which may be seen as a calculus
with the advantages of both. It is thus, on the one hand, in the
cut-free case, an abstract foundation for declarative logic
programming with uniform proofs and, on the other hand, when cuts are
allowed, a calculus with explicit substitutions, and thus may be a
clear logical basis for efficient functional language implementation.
In particular, we outline a solution to a problem raised by Herbelin
about the termination of a cut-reduction system that allows enough
permutation of cuts for the simulation of ordinary beta-reduction.
Algorithmic proof-search is a essential enabling technology throughout
informatics. Proof-search is the proof-theoretic realization of the
formulation of logic not as a theory of deduction but rather as a
theory of reduction. Whilst deductive logics typically have a
well-developed semantics of proofs, reductive logics are typically
well-understood only operationally. Each deductive system can,
typically, be read as a corresponding reductive system. We discuss
some of the problems which must be addressed in order or provide a
semantics of proof-searches of comparable value to the corresponding
semantics of proofs. Just as the semantics of proofs is intimately
related to the model theory of the underlying logic, so too should be
the semantics of proof-searches. We discuss how to solve the problem
of providing a semantics for proof-searches which adequately models
both operational and logical aspects of the reductive system.
This is joint work with David Pym.
In this talk I will discuss a number of aspects of
programming languages and motivate the design of a new
language with some novel features. The main aim is to
improve software reliability by providing more secure
features than those in Pascal-like and Java-like languages.
Topics that will be covered include functions and
procedures; access modes for variables and parameters;
pointers, aliasing and swapping; records and
variants; and finally objects.
Computer algebra systems are in widespread practical use, despite the fact
that they are not always reliable. The talk will introduce a novel
scheme for integrating formal reasoning into the Axiom computer algebra
system, thus enabling the system to be both strengthened and made more
sound. The embedding uses dependent types in the Axiom type system, and
the talk will introduce, inter alia, the constructive approach underlying
the work.
In this talk we propose a possible programming language
for quantum computation: the quantum Guarded-Command
Language (qGCL). It is a high-level imperative programming
language derived from the probabilistic Guarded-Command
Language (pGCL). qGCL inherits from its probabilistic
parent pGCL a rigorous semantics and therefore an associated
refinement calculus, which include program refinement, data
refinement and combination of specifications with code.
Furthermore, qGCL incorporates (demonic) nondeterminism and
probability, which are both featured in quantum computation.
We shall start our exposition introducing the necessary
quantum mechanics background. Then we briefly present the main
features of pGCL and from there we introduce the quantum
extensions of qGCL. In order to demonstrate the expressiveness
of our notation we cast in qGCL the most known quantum algorithms,
such as Shor's and Grover's algorithms. The main strentgh of qGCL
is its refinement calculus, which originates from the rigorous
semantics of pGCL. To illustrate this point we shall give an
algebraic derivation of the Deutsch-Jozsa's algorithm and provide
a formal reasoning for some Gedankenexperimente from quantum
physics, such as the famous Einstein-Podolsky-Rosen paradox.
Tradition in the area of formal specification teaches that pure
propositional logic is adequate for the stationary state of finite
bit-level systems, but that in order to capture dynamic behaviour over
time an enrichment by some form of
extra temporal operators (predicate logic, temporal logic, modal
logic) is necessary.
This talk will demonstrate that the opposite strategy is feasible
too, namely that there are fragments of propositional logic in which it
is possible to specify nontrivial classes of finite state
behaviours. This is relevant for applications in Computer Science
where the right trade-off between syntax and semantics is essential.
In the talk we will consider intuitionistic logic as a natural such
fragment, which, though propositional in syntax, offers second-order
expressiveness. We will look at two different ways of exploiting this
semantic richness to accommodate timing behaviour. The first one
generates a fully-abstract semantics for Statecharts, essentially
solving the full-abstraction problem for this widely used engineering
design language. The second fragment is related to Maximovas
intermediate logic LPi (Logic of the Rhombuses), in which properties
of finite bidirectional automata may be expressed.
I will discuss some recent ideas on how to give semantics to
generic programs (i.e. programs which work on all types, but which
are not parametric such as equality or map). The main point is that
generic programs can be viewed as folds or unfolds once one has
chosen the ambient category properly.
A Hoare-calculus for a simple object-oriented (class-based) language is
presented that can be viewed as an extension of America and de Boer's
approach, ie. no explicit representation of the heap is needed in the
assertions. The Hoare-logic is also inspired by OCL (Object Constraint
Language) such that simple Java programs can be shown partially
correct with respect to OCL-specifications. We will discuss limitations
of the presented calculus and compare it with other approaches.
Joint work with Ulrich Schoepp
For many computer science students, the specification and implementation
of a universal function for the lambda-calculus is usually presented in
the context of functional language implementation. The exposition of
the techniques is therefore biased to such domain of closed
expressions.
This report is an attempt to present the subject in systematic and
precise terms, and to provide a critical account of the rationale
behind commonly known techniques that can be used to carry out the
implemention of an (allegedly) efficient interpreter for the pure
lambda-calculus. Its purpose is educational, hence the differences,
criticisms and points in common with other well-known authors also play
an important role.
In this talk I will try to give a brief description of proof planning,
which is an AI based automated proof search technique. I will cover
some of the history of proof planning since several of its key concepts
and motivations have changed a bit over the years. I will then describe
the lambda-clam proof planing system which is a higher-order proof
planner for which I was the main developer when I worked in Edinburgh.
I will discuss what it does, its shortcomings and the shortcomings of
its implementation language and what its future may be.
Some applications are most easily expressed in a programming laguage
that supports concurrency, notably interactive and distributed systems.
Concurrent Haskell is an extension to the purely-functional language Haskell,
allowing it to express explicitly concurrent applications. The
system appears to be both expressive and efficient, and a number of useful
abstractions can be built.
In my talk I shall give an introduction to programming with
Concurrent Haskell.
Or, Why not specify dynamic behaviour in a fragment of propositional
logic?
This is joint work with Martin Wirsing & Rolf Hennicker (LMU Munich).
The modal mu-calculus offers a rich logic for expressing temporal
properties of processes, and much effort has gone into developing
techniques for automatically model-checking such properties of
finite state processes. However, general processes (for example
arbitrary CCS processes) are not finite state, and the
problem of checking whether a process (expressed in a process
algebra) satisfies a formula is undecidable.
In the face of undecidability, one seeks formal systems that are
sound for establishing properties of processes. Although necessarily
incomplete, one would like to find systems that provide perspicuous
reasoning methods which suffice in practice. Much of the talk will be
devoted to presenting a sequent calculus, strongly based on a system
proposed by Mads Dam and Dilian Gurov, that I believe satisfies
these requirements. The crucial idea, due to Dam and Gurov, is to
introduce explicit fixed-point approximants into the proof system.
This allows induction and coinduction arguments to be replaced by
a global combinatorial condition on proofs. In our system, we use
a new syntax for approximants, incorporating "modalities" for
approximant modification.
It is an interesting question to what extent the methods
provided by the proof system do suffice in practice. One way
of addressing this is to obtain restricted completeness results,
showing completeness in special cases where such results are at least
possible in theory. I shall conclude by presenting a new result in
this direction: our proof system is complete for establishing
arbitrary mu-calculus properties of context-free processes.
The proof makes essential use of approximant modifiers.
As far as we know, this is the first completeness result for
a general purpose proof system with respect to a significant
class of infinite state processes.
School of Computer Science and IT
University of Nottingham
Jubilee Campus, Wollaton Road
Nottingham NG8 1BB
United Kingdom