• People
• Events
• Research

Lab Lunch Talks 2006

Archive: 1994 · 1995 · 1996 · 1997 · 1998 · 1999 · 2000 · 2001 · 2002 · 2003 · 2006 · 2007 · 2008 · 2009

• 5th December Dominik Wojtczak

  NWERC 2006

  I would like to talk about a recent, and first time ever, participation of a student team (Michael Smith, Ali Eslami, Edward Leiper) from the University of Edinburgh in the Northwestern European Programming Contest that took place on the 18th of November 2006 in Stockholm.

  I will explain how the contest looks like, what is it all about, and most importantly what kind of problems students have to solve, illustrated by an example problem, with its solution, from this year's competition.

• 21st November Matija Pretnar

  Handling computational effects

  In the last five years, Gordon Plotkin and John Power have developed a unified algebraic approach to computational effects such as exceptions, nondeterminism, input/output, state... I will give a simple overview of the results and unveil important recent work.

• 14th November Shriram Krishnamurthi

  Flapjax: a Programming System for the Web

  Contemporary Web applications face numerous challenges: They must be responsive to user inputs and to server communications. They must maintain persistent data on servers. They must enable sharing of data with other users, while placing restrictions on this sharing. They need to interface well with third-party Web services.

  Flapjax is a programming system that supports all these operations. Flapjax shares the syntax of JavaScript, making it instantly familiar to many programmers, but transparently endows its semantics with reactive, dataflow evaluation. Because Flapjax compiles to JavaScript, it can immediately be deployed on most browsers. Flapjax is also designed to be used as a library in existing applications.

  See http://flapjax-lang.org/ for the goods.

• 24th October Bartek Klin

  Bialgebras and modal logic

  I will tell you about some recent ideas about what happens when one combines structural operational semantics (modelled with bialgebras) with modal logics (interpreted on coalgebras). Some category theory is involved, but I will try to be as informal as necessary to make the message clear also to those who do not care about categories.

• 3rd October DeLesley Hutchins

  Eliminating Distinctions of Class -- Using Prototypes to Model Virtual Classes.

  This is a test run of a talk that I'll be giving at OOPSLA in October.

  In mainstream OO languages, inheritance can be used to add new methods, or to override existing methods. Virtual classes and feature oriented programming are techniques which extend the mechanism of inheritance so that it is possible to refine nested classes as well. These techniques are attractive for programming in the large, because inheritance becomes a tool for manipulating whole class hierarchies rather than individual classes. Nevertheless, it has proved difficult to design static type systems for virtual classes, because virtual classes introduce dependent types.

  I present a formal object calculus which implements virtual classes in a type-safe manner. My type system uses a novel technique based on prototypes, which blur the distinction between compile-time and run-time. At run-time, prototypes act as objects, and they can be used in ordinary computations. At compile-time, they act as types. Prototypes are similar in power to dependent types, and subtyping is shown to be a form of partial evaluation. I prove that prototypes are type-safe but undecidable, and briefly outline a decidable semi-algorithm for dealing with them.

• 19th September Patrick Maier

  Why I am interested in intuitionistic temporal logics

  Reactive behaviour of systems is frequently specified in temporal logics (such as LTL) whose semantics is defined in terms of infinite traces. In compositional verification using so-called assume-guarantee rules, however, the finite prefixes of infinite traces play a key role. This calls for logics whose semantics are defined in terms of prefix-closed sets of finite and infinite traces. In this talk, I will present such a semantics for LTL, giving rise to a superintuitionistic temporal logic. I will demonstrate how this logic (and in general, a whole family of superintuitionistic temporal logics) admits a logical characterization of safety and liveness properties and a rather intriguing (well, to me) logical formulation of sound composition rules for (apparently) circular assume-guarantee reasoning.

• 12th September 2006 William Stirton

  Let "theory of type assignment" mean a set of rules for assigning types to terms of the untyped lambda calculus. Every such theory gives rise to the well-known "typability" and "type-checking" problems. In relation to all of the best-known theories -- with the exception of the very simplest as well as those which assign a type to every lambda term whatsoever -- these two problems are known to be unsolvable. How should we respond to this fact (discussion point)? Some researchers have been busy proving that the two problems are indeed solvable in relation to certain fragments of the well-known theories, eg the polymorphic and intersection theories, but are the results satisfactory (another discussion point)? The same researchers sometimes lament the lack of "power" of the known decidable fragments, but what can they mean by this (another discussion point)? I myself would suggest that one way to make precise the concept of the "power" of a theory would be to identify that with the particular sub-class of recursive functions representable in the theory, and would like to hear what people think of this proposal. I have devised a theory of type-assignment with respect to which the two problems are solvable and which I think has some nice properties. These will be summarized.

• 5th September 2006 Kyriakos Kalorkoti

  Bokut' Normal Forms in Group Theory

  HNN extensions are a standard construction in group theory and have played a key role in establishing undecidabilty results for finitely presented groups. This talk will outline the construction and application of certain normal forms due to L.A. Bokut' that have proved very useful in establishing r.e. Turing degree versions of the results. The talk is aimed at a general audience, technical details will be kept to a minimum and no expert knowledge of the subject will be assumed.

• 29th October 2006 Thierry Martinez

  Automata with bindings and their application to regular type inference and polymorphism

  Regular expressions are often used to extract parts of a matched word as well as to decide whether the word belongs to the associated regular language. The first part of the talk presents slightly extended automata that can be used to extract these parts. First, we will define regular expressions with bindings and non-deterministic automata with bindings, and show a Kleene theorem to go from one representation to the other. We will then introduce a notion of deterministic automata with bindings, and show how to transform a non-deterministic automata into an equivalent deterministic one. Deterministic automata have some extensions of the classical construction of the product automata: building the intersection and union between two automata with bindings, and the set-difference between an automaton with bindings and a classical automaton. Moreover, deterministic automata can be minimized to improve performance of these constructions as well as the performance of matching against a word.

  In the second part of the talk, we will introduce a language where all values are strings whose types are regular expressions. We will show that regular expressions with bindings can express polymorphic types and will illustrate the particular role of non-deterministic bindings when they are used in types. Finally, we will sketch how types can be inferred.

• 25th July 2006 Sam Lindley

  Sieves: adding declarative concurrency to C++

  Concurrency is becoming increasingly important to mainstream software developers. Unfortunately the predominant thread-based approach to concurrent programming is highly bug-prone, difficult to reason about, and does not scale well to large numbers of processors.

  Codeplay, a small Edinburgh-based computer games technology company, has devised a declarative concurrency extension to C++ which has a straightforward semantics, is intended to be no more difficult to reason about than sequential C++, and should scale to large numbers of processors. I shall give a short talk on the fundamentals of this system.

• 18th July 2006 Laura Korte

  The Turtle in Search of the Grail (how game-building can improve the theoretical computer science curriculum)

  We present `constructive game-based learning' as a new approach to theoretical computer science education in the undergraduate curriculum. Game-based learning generally refers to different forms of learning-by- game-PLAYING. Constructive game-based learning on the other hand, refers to learning-by-game-BUILDING. We will argue that theoretical computer science is a particularly suitable niche for this technique. Furthermore, we will present results of the first of two studies into the effects of constructive game-based learning on student motivation/affect and student performance.

• 30th May 2006 Kenneth MacKenzie

  More about knots

  Having prepared far too much material for my Lab Lunch talk of a few weeks ago, I'll try to finish it off this week. I'll talk about the discovery of new knot invariants in the 1980s (the Jones polynomial among others), and then go back to the late 19th century to say something about knot theory's Scottish origins.

  This talk will be largely independent of the previous one, and should also be a lot more relaxed.

Archive: 1994 · 1995 · 1996 · 1997 · 1998 · 1999 · 2000 · 2001 · 2002 · 2003 · 2006 · 2007 · 2008 · 2009