Lab Lunch Talks 1997
Archive: 1994 · 1995 · 1996 · 1997 · 1998 · 1999 · 2000 · 2001 · 2002 · 2003 · 2006 · 2007 · 2008 · 2009
| 7 October | Adriana Compagnoni | Joint work with Maribel Fernandez (ENS Paris) | <abc@dcs.ed.ac.uk> |
An Object Calculus With Algebraic Rewriting |
|||
|
The addition of algebraic data types arises naturally in trying to use Abadi and Cardelli's object calculi as a foundation for a programming language. This work defines such extension, shows a motivating example, and explores the new calculi by establishing properties such as Church-Rosser, Subject Reduction and Uniqueness of Types. Familiarity with the particular object calculi is not essential. |
|||
| 30 September | Andrzek Filinski | <aof@dcs.ed.ac.uk> | |
Denotational Semantics In A Logical Framework |
|||
|
I will give a brief overview of Edinburgh LF and its potential as a tool for machine-assisted reasoning about programming language semantics. In particular, I will outline a calculus of LF signatures and realizations, and show how it captures a natural notion of compositional, type-preserving translations between languages with non-trivial name-binding structure. If time permits, I will also sketch some ideas about representing logical-relations proofs in this setting. |
|||
| 23 September | Samson Abramsky | <samson@dcs.ed.ac.uk> | |
Closure Operators As Concurrent Strategies |
|||
|
Domain theory isn't only for the nasty things in life... |
|||
| 16 September | Adriana Compagnoni | <abc@dcs.ed.ac.uk> | |
Workshop and Conference Reports |
|||
|
I've been to a workshop in Durham, on "Subtyping, Inheritance and Modular Development of Proofs" and to the joint conferences "PLILP/DPLE/ALP/HOA'97" in Southampton. I will give a short talk with some highlights. |
|||
| 9 September | Thomas Kleymann-Schreiber | <tms@dcs.ed.ac.uk> | |
Towards Mechanising Relative Completeness |
|||
|
When considering more interesting language features such as local variables, recursive procedures, parameter passing, exceptions,... it is well known that many proposed verification calculi are unsound or incomplete despite being backing up by "proofs" to the contrary. Why not use computer-aided proof systems? Indeed, it appears that not only is this an option, it is also feasible. All machine-checked results are so far confined to a particular assertion language. It would be more interesting to study relative completeness where one considers an arbitrary expressive assertion language. We sketch how one might set up relative completeness in a logical framework. We conjecture that such an alternative definition of relative completeness is better than the traditional version in that it may prevent certain (all?) incompleteness results. |
|||
| 2 September | Conor McBride | <ctm@dcs.ed.ac.uk> | |
Zeno: A Large Knob With LOGO On |
|||
|
Way back when, Seymour Papert created LOGO, a procedural language with simple `turtle graphics' drawing commands. It has (for better or worse) gained some currency in the Mathematics Education establishment. When the National Curriculum people were looking to force IT into maths lessons, LOGO was one of the few things which came to mind, especially with respect to transformational geometry. Unfortunately, LOGO does not have a convenient notion of transforming a figure by a mapping, so the whole thing was swept under Sir Ron Dearing's National Carpet to howls of Luddite delight. In the early nineties, I and some cronies from the Queen's University of Belfast came up with Zeno, an extension of LOGO which allows coordinate-transforming functions to be applied to figures, enabling students to investigate the properties of such functions in an intuitive visual setting. Naturally, this required us to add to Zeno some operations on functions, ironically, the kind of natty higher-order gizmos Papert expelled from LISP when creating LOGO in the first place. I shall (hopefully) demonstrate the beta-release of Zeno, whilst admitting to
|
|||
| 15 July | Stephen Gilmore | <stg@dcs.ed.ac.uk> | |
| 10 June | LFCS and the proposed IPU reorganisation | <dts@dcs.ed.ac.uk> | |
| 27 May | Jitka Stribrna | <js@dcs.ed.ac.uk> | |
| 13 May | Vivek Gore | <gore@dcs.ed.ac.uk> | |
| 4 March | Rod Burstall | <rb@dcs.ed.ac.uk> | |
Collaboration with Harlequin |
|||
|
Rod will talk about the collaboration with Harlequin on Memory Management, in particular initiating some discussion of the non-disclosure issues raised at last week's Lab Lunch. |
|||
| 25 February | Gordon Duckett | <grd@dcs.ed.ac.uk> | |
Technology Foresight: What's in it for us - if anything? |
|||
| Gordon will be speaking about an example of a Technology Foresight program within the British Aerospace Industry Sector. A brief snapshot of the industry and its research intentions will be given followed by a discussion on "What's in it for us - if anything?" | |||
| 18 February | Alan Smaill | <smaill@dcs.ed.ac.uk> | |
...trying to make sense of Rene Thom's book "Semio Physics"... |
|||
| I have been trying to make sense
of Rene Thom's book "Semio Physics" (Addison Wesley 1990 -- also
"Esquisse d'une semiophysique", InterEditions, 1988).
Thom tries to analyse what sorts of processes or forms are intelligible or significant, and can thereby be used as the basis for a linguistic description. I'll try to explain the ideas, as far as I follow them. |
|||
| 11 February | Alex Simpson | <als@dcs.ed.ac.uk> | |
A constructive proof of Tarski's fixpoint theorem |
|||
| A classic fixpoint theorem of
Tarski says that any monotonic function on a directed-complete
partial order with least element has a least fixpoint. The usual
proof finds the fixpoint as the supremum of a chain of
ordinal-indexed iterates. The argument is not constructively valid.
In the talk I will present a new proof found recently by a mathematician, Dimitri Pataraia, from Georgia. The argument is short, beautiful, very elementary and, despite all this, constructively valid. |
|||
| 4 February | Nigel Topham | Computer Systems Group | <npt@dcs.ed.ac.uk> |
Future High Performance Systems: An Architectural Perspective |
|||
| 28 January | David Pym | Queen Mary & Westfield College | <pym@dcs.qmw.ac.uk> |
Classical Disjunction |
|||
| It has been long-standing problem
in logic to give a non-trivial semantics of the proof theory of
classical logic. A substantial advance, roughly speaking for the
and/implies-fragment, has been provided by Parigot's treatment of
free (cf. natural) deduction via the lambda-mu-calculus. We
consider the two obvious ways to add disjunction to lambda-mu, one
deriving from LJ and one from LK. We see that each gives an
adequate account of classical disjunction but that semantically,
they are quite distinct: indeed, forcing their models to be
isomorphic causes the familiar collapse to a Boolean algebra. We
see that categories of continuations provide models for
lambda-mu-nu, i.e., lambda-mu with LK-derived disjunction.
Considering an application to computing, we also see, for
complexity reasons, that this disjunction is the one we require as
the basis for logic programming. Finally, we see the role of
continuations in the semantics of logic programming based on
lambda-mu-nu's view of classical logic.
I promise to keep this talk down to at most half an hour and to avoid most of the technical details. This is recent/on-going joint work with E. Ritter, University of Birmingham. A draft paper (extended abstract) is available. |
|||
| 21 January | Dave Matthews | LFCS and Prolingua Ltd | <dcjm@dcs.ed.ac.uk> |
LinguaNet |
|||
| LinguaNet is a project about
international communications particularly for police forces. It is
currently supported by the EU's Language Engineering Programme.
Prolingua has set up a network of workstations in police stations
in several different countries around the North Sea which is used
for the daily exchange of messages. Using formatted messages we are
able to achieve a degree of language translation. The initial
version of LinguaNet was written in Standard ML although it was
later translated into C.
I hope to be able to give a live demonstration of the system and I will also be talking about the advantages and disadvantages of using Standard ML as a prototyping language. |
|||
| 14 January | Pekka Orponen. | <pekka@dcs.ed.ac.uk> | |
The effects of noise on discrete-time analog computation. |
|||
| We consider the effects of noise
on the power of discrete-time analog computational models with a
bounded state space, specifically discrete-time analog neural
networks. We show that the presence of arbitrarily small amounts of
noise reduces the power of such models to that of finite automata,
and we also provide a finite upper bound for their VC-dimension in
the presence of analog noise.
(Joint work with Wolfgang Maass.) |
|||
| 7 January | Conor McBride. | <ctm@dcs.ed.ac.uk> | |
Types '96 Aussois. |
|||
| Leaping in at the last minute, Conor gets out his holiday snaps from the Type Theory Workshop held in December 1996 at Aussois in the French Alps. Unfortunately, the developers have sent him the wrong package... | |||
Archive: 1994 · 1995 · 1996 · 1997 · 1998 · 1999 · 2000 · 2001 · 2002 · 2003 · 2006 · 2007 · 2008 · 2009