Foundations of Programming Meetings 1997
School of Computer Science and ITUniversity of Nottingham
The semantics of qualified types has previously been defined in terms of a translation into the second order polymorphic lambda-calculus, supported by a coherence result stating that although there may be many translations for a given term, they are in some sense equivalent. Though a reasonable solution, it depends on the fact that a suitable model is constructed for the polymorphic lambda-calculus.
A model for the polymorphic lambda-calculus requires structures suitable
for modelling impredicative polymorphism, which, in light of the fact that
qualified types supports only predicative polymorphism, seems a strong
requirement. In this talk, we present an alternative semantics for qualified
types. Extending previous results of Ohori, we present a simple semantics for
qualified types in terms of the simply typed lambda-calculus. Exploiting
well-known results for logical relations and the simply typed
lambda-calculus, we develop a parametricity theorem for qualified types
with respect to our original semantics.
RBMH is a language for creating interactive animations on PCs. It is
implemented in Haskell, and uses Haskell as a host language so that
animations are actually Haskell programs. The declarative style of
programming appears to be well suited to animation. I will give some
indications as to why this is so. I will also describe in detail some
simple examples in RBMH and then demonstrate them. This will help to
show that the approach makes the construction of animations very easy
and concise. The main concepts will be introduced, and some
implementation considerations discussed.
RBMH is an interesting application in itself, but also has relevance to
functional programming in general by addressing questions in semantics,
interaction, interfacing with other technologies, modularity, type
systems and compile-time optimization.
The RBMH system is being developed by Conal Elliott at Microsoft Research,
and in collaboration with Nottingham, Yale and Glasgow Universities.
In recent years state transformers have been used to provide a structured and
efficient implementation of state within pure functional programs. However,
programs written using this method can only exploit "single-threaded" state,
that is, there is one mutable state value of a fixed type that is threaded
through the program. In practice this means that all variables are global.
I approach the problem of state within the context of describing simple
data-flow networks. This raises problems as individual components within
the network might require their own _local_ state, but must still be able
to be combined to form larger components. I describe combinators for
constructing these networks that allow the programmer the clarity, safety
and modularity of local variables, with the resulting programs being
automatically transformed to a single state-thread.
The pi-calculus is a model of concurrent computation whose central
concept is that of the channel name. In the earlier calculus CCS,
values and channels are different entities. This distinction is not
made in the pi-calculus, and results in extra expressive power. In
this tutorial talk I will give examples to illustrate the polyadic
version of the pi-calculus, and describe the monomorphic type system
for this calculus developed by Turner. I will also present Ostheimer and
Davie's encoding of the call-by-value lambda-calculus, thus illustrating
how the pi-calculus can be considered a superset of the lambda-calculus.
The Girard/Reynolds calculus of polymorphic functions, also known as
system F, provides a general framework for the representation of
inductive types, for example the natural numbers. In this talk we
highlight the correspondence between the inductive types of system F
and the propositions of second-order logic, in particular that well
known inductive proof principles arise as a natural consequence of
inductive types.
One of the attractions of building functional parsers using combinators
is that the structure of parsers closely follows the structure of the
underlying grammars. Unfortunately, this is not true for left-recursive
grammars, which must either be transformed to eliminate the left-recursion,
or re-expressed using special combinators. In this talk I will show
that left-recursion does not in fact present a problem, provided
that the correct fixpoint operator for parsers is used. Some prior
exposure to the theory of fixpoints will be assumed, but all the
necessary definitions and results will be summarised.
This talk is based upon an idea by Philip Wadler.
Conceptually, stream processors are concurrent processes with a number
of input and output streams. Networks of such processors have
applications in a variety of areas, including simulation of systems,
mechanisms for I/O in functional languages, and the high-level
construction of graphical interfaces.
Developing equational theories for stream processors based on
implementations in deterministic functional languages can give
misleading results. In this talk we develop a simple
language of stream processors, whose semantics is specified by
translation into the pi-calculus. We avoid misleading results in the
equational theory by using bisimulation as a notion of semantic
equivalence.
Milner, Walker, and Parrow's pi-calculus has been proposed as a
fundamental calculus of processes in the same way that the lambda
calculus is considered a fundamental calculus of functions. A lot of
programming languages have been based upon the lambda calculus, and so,
dually, it is interesting to ask what a programming language based upon
the pi-calculus would look like. Pierce and Turner have developed such
a language, called Pict. In this talk I will give an introduction to
Pict, and concentrate on the derived constructs in the language that
allow Pict programs to be written at a high level, as opposed to the
low level nature of the pure pi-calculus. Examples of Pict programs
will be used extensively to explain the language's features.
Category theory is a very natural setting for thinking about functions and
functional programming, but some extra work is required to extend functions
to the more general notion of relations. I will describe one approach to
modelling the relational calculus in a categorical setting, and show the
importance and problems of calculating 'pullbacks' in the evaluation of
relational expressions using this approach.
Real-valued functions and ordinary differential equations (ODEs) are useful
for describing behaviors in (continuous) animation but they are also used
in many other domains. Our work on functional animation has introduced
some interesting ideas in this area which may be worth exploring independently,
in a more general setting. In this talk I will describe the problem of
representing real-valed functions, how numerical methods for solving ODEs
work, and a neat representation for ODEs.
Paul: Genetic programming for countdown;
Game semantics is an approach to specifying the semantics of
programming languages through the ideas of game theory. In this talk I
will give an introduction to the basic concepts in this field. The
semantics of programming language constructs such as constants,
functions, state, and control operators will be illustrated using
games. Constraints can be placed on the strategies used to play the
games and these correspond closely to certain programming disciplines.
These constraints will be explained and used to describe a "semantic
cube".
Monads are a concept from category theory that have applications in
many areas of computing. In this talk I will explain how the concept
of a monad can be viewed in terms of the simpler set-theoretic concept
of a monoid. More technically, I will explain how a monad in a category
C can be defined to be a monoid in the functor category C^C.
This is the first meeting of the Autumn term. Each member of the
group will present a 5-minute overview of their recent and current
work, addressed to a general audience.
Bisimulation is a standard technique for defining equivalences for
concurrent languages. We can reason equationally about programs if such
bisimulations are congruences. The proof of these congruences for
bisimulations on higher-order calculi, and weak bisimulations tend to be
significantly complex. In this talk I will discuss a technique that
simplifies these proofs and was first proposed by Howe. Using a simple
arithmetical language I will illustrate the basic concepts involved in
his method.
The principles of abstraction, correspondence, and data type
completeness have been proposed to guide and evaluate the design of
general purpose languages in the late 1970s. I argue that these
semantic principles for language design can be particularly useful
for the design of extensions to purely functional languages. After
evaluating a simple functional core language with respect to the
design principles, I focus on language extensions, using module
systems and i/o-facilities as examples. Following the principles,
we are led to a simple, yet expressive extended language. It turns
out that the final language design demands support for orthogonal
persistence.
Comments: The core of this talk has been given at IFL'97. It addresses a
fairly general audience and presents some afterthoughts on my Ph.D.
work. I will try to extend the parts describing my work and the
context in which I have been working.
Several proof tools have been developed to aid coinductive proofs but
nearly all require user interaction. Crucially they require the user to
supply an appropriate relation which the system can then prove to be a
bisimulation (a relation of observationally equivalent objects).
Proof planning is an approach to automated theorem proving that aims
to extend the current tactic based systems with proof methods, which
may involve heuristics, to guide tactic application. Proof planning
has been successfully applied to the area of inductive theorem
proving. This talk aims to outline the basic ideas behind proof
planning with reference to the planning of coinductive proofs.
In this talk we describe a technique called type directed specialisation,
which has recently been proposed as a new paradigm for partial evaluation.
We show that an interpreter for the simply typed lambda calculus,
which operates on a universal type, can be specialised such that all type
tags are removed (e.g. run-time type checking is avoided).
This talk is based upon a recent paper by John Hughes.
Fudgets is a toolkit for developing graphical applications in the functional
language Haskell. In this talk I will describe the basics of a formal theory
of Fudgets based upon ideas from concurrency theory. The theory is useful for
reasoning about programs written in Fudgets, and also for verification of
Fudget implementations. Some simple examples of using the theory for reasoning
will be illustrated.
The interpretation of natural language utterances
typically depends on the context of utterance, and also has
effect of updating that context. This talk looks at using
a fragment of linear logic as a tool for formally modelling
context update in natural language.
The work, which is the result of collaboration with Josef van
Genabith, extends the glue language approach of Mary Dalrymple
and colleagues. This uses a fragment of linear logic as a
meta-level glue language, determining how the object-level
meanings of individual words and constituents may be stuck
together. Dalrymple's work does not address context dependent
aspects of meaning, but the resource sensitivity of linear
makes it well suited for modelling various forms of update.
Corecursion is a definition principle that is commonly described as
the dual of recursion. This talk will review various discussions of
corecursion and various attempts at providing a formal definition of
what corecursion is. I shall also discuss the need for corecursive
definitions in coinductive proof and the connection between
non--termination and corecursion. This talk will raise several
questions about corecursion which it won't answer, hopefully at the
end there will be time for some discussion of those questions.
Ben: Type inference for cyclic types;
Graham: Non-structural induction over trees;
Colin: Structural congruences in the pi-calculus;
Tony: Modelling behaviours functionally;
Mark: Reasoning about an abstract machine.