Lab Lunch Talks 2003
Archive: 1994 · 1995 · 1996 · 1997 · 1998 · 1999 · 2000 · 2001 · 2002 · 2003 · 2006 · 2007 · 2008 · 2009
24th June 2003 Michal Konecny mkonecny@inf.ed.ac.uk
Type-Safe Web Session Programming Peter Thiemann's WASH is a Web authoring system embedded in Haskell. I would like to make a gentle advertisement for it based on a small example. WASH is session-centric, abstracting away many low-level features of web programming and it uses Haskell98 types to guarantee type-safety of all data flow as well as a quasi-validity of all XHTML pages that it might produce. For more information, see http://www.informatik.uni-freiburg.de/~thiemann/haskell/WASH/.
17th June 2003 David Aspinall David.Aspinall@ed.ac.uk
A Logic for Grail GRAIL (acronym too painful to write down) is the intermediate language used in the Mobile Resource Guarantees (MRG) project. It is a functional view of a fragment of the Java Virtual Machine Language. Don Sannella introduced MRG at a lab lunch earlier this year (quick reminder of the tagline: "proof-carrying code for resource bounds"). I'll talk about the low-level logic that we are designing for expressing resource usage of Grail programs, and explain how it is being prototyped within the Isabelle theorem prover.
10th June 2003 Peter Buneman opb@inf.ed.ac.uk
The Fast Fourier Transform as a Database Query What do database queries, scientific programming and monads have to do with each other? The speaker will display his ignorance of all three topics.
3rd June 2003 Robert Atkey R.A.Atkey@sms.ed.ac.uk
Common Lisp I'll talk a bit about the language Common Lisp and some of the more interesting features it has such as dynamic binding, macros, multimethods etc. This will be a very superficial overview of the language and will mainly concentrate on the features I find interesting.
27th May 2003 Julian Bradfield jcb@inf.ed.ac.uk
Second-order logic and foundations of mathematics is the title of a recent (Bull.Symb.Logic vol 7 no 4, Dec 2001) paper by Jouko Väänänen, discussing the differences between first-order set theory and second-order logic as a foundation for mathematics. As a side effect, he obtains a depressing result on the complexity of validity for Hintikka's independence-friendly logic. I found this paper very nice (and also pleasantly short); in this talk I shall try to present it in overview.
20th May 2003 Allan Clark A.D.Clark@sms.ed.ac.uk
The Mono Project Most people have heard about the .NET platform as an alternative to the Java development platform. The Mono project is an open source project aimed at developing a free version of the .NET platform for unix based environments. In this talk I hope to give an overview of the technology present within the mono project, provide a feel for the current status of the project and try to place mono within the context of other projects such as the Gnome Desktop and DotGnu.
13th May 2003 John Longley jrl@inf.ed.ac.uk
Vague thoughts in the direction of a new programming language I will outline some rather fragmentary thoughts which I intend to make the basis of a grant proposal in the near future. The idea is to draw inspiration from some recent work in game semantics and come up with a stunningly beautiful new programming language that brings together the best of Java and the best of Standard ML. I can't tell you exactly what's in the language yet, but I hope to give some feel for how the ideas of denotational semantics are supposed to help.
6th May 2003 Sibylle Froeschle sib@inf.ed.ac.uk
The undecidability of hereditary history preserving bisimilarity,
- or the power of concurrent systemsI will try to explain the main ideas behind the undecidability proof of hereditary history preserving bisimilarity (Jurdzinski, Nielsen 2000) with as little technicalities as possible.
28th April 2003 Alex Simpson Alex.Simpson@ed.ac.uk
Zen Gardens and Polymorphic Effects I have recently returned from six months in Kyoto, Japan where I was visiting Masahito "Hassei" Hasegawa at the Research Institute for Mathematical Sciences, Kyoto University. I will talk a little about my impressions of Japan, and a little about some joint work (still in progress) with Hassei on relating varieties of polymorphism and computational effects.
22nd April 2003 Don Sannella dts@inf.ed.ac.uk
Mobile Resource Guarantees The MRG project, which is an EC-funded collaboration between LFCS the LMU Munich, is building infrastructure for endowing mobile bytecode programs with independently verifiable certificates describing their resource consumption. These certificates will be condensed and formalised mathematical proofs of a resource-related property which are by their very nature self-evident and unforgable. Arbitrarily complex methods may be used to construct such a certificate, but once constructed its verification will always be a simple computation. This makes it feasible for the recipient to check that the proof is valid, and so the claimed property holds, before running the code. This work falls within the area known as "proof carrying code". Our focus in MRG on quantitative resource guarantees is different from the traditional PCC focus which is security. Another novelty is the method to be used to generate proofs, which is to use a linear type system that classifies programs according to their resource usage as well as according to the kinds of values they consume and produce. The intention is to generate proofs of resource usage from typing derivations.
15th April 2003 Jennifer Tenzer J.N.Tenzer@sms.ed.ac.uk
ETAPS'03 8th April 2003 Ulrich Schoepp Ulrich.Schoepp@ed.ac.uk
Joyal's Species of Structures Joyal's Species of Structures, and some of its applications to combinatorics, programming languages and semantics.
1st April 2003 Ian Stark Ian.Stark@ed.ac.uk
FreshML The FreshML system of Pitts and Shinwell is "a new language derived from Standard ML which provides superior facilities for writing software systems which manipulate syntax involving binding operations". Compiler available at www.freshml.org. I'll talk about the language, and a small amount of the non-standard set theory it is based on.
25th March 2003 Martin Hofmann mhofmann@informatik.uni-muenchen.de
A new deductive system for the mu-calculus February 18th, 2003 Kousha Etessami <kousha@inf.ed.ac.uk >
How would you gzip a file if you didn't care about the ordering between some pairs of symbols in the alphabet?
--or--
Compression of concurrent traces.February 11th, 2003 Sam Lindley and Jon Cook
Report on POPL 2003 February 4th, 2003 Martin Grohe <grohe@inf.ed.ac.uk >
The Strong Perfect Graph Theorem I will talk about a recent result of Chudnovsky, Robertson, Seymour, and Thomas solving one of the most important open problems in graph theory by proving Berge's strong perfect graph conjecture (1960).
The relevance of this result for computer science is due to a curious connection between perfect graphs and integer programming.
January 28th, 2003 Patrick Goldsack, senior researcher at the Hewlett-Packard Corporate Research Laboaratories based in Bristol, UK
SmartFrog - A System for Grid Configuration SmartFrog is a framework targeted at describing and instancing applications and resources for Grid infrastructures. The talk will only cover one aspect of the framework in detail, namely the data definition language that is used to define the configuration requirements to the underlying SmartFrog engine. The talk will briefly examine the requirements for such a language, how these requirements have been met, and show an example of the language in use. Although aimed at a similar space to XML, namely data definition, the SmartFrog language differs in that it is designed to provide data descriptions which are parameterisable, checkable and reusable. Furthermore, it is based on a prototyping model rather than the more common schema/instance model of languages such as XML. Note that this is work in progress, so the detailed design of the language is still in some flux.
Archive: 1994 · 1995 · 1996 · 1997 · 1998 · 1999 · 2000 · 2001 · 2002 · 2003 · 2006 · 2007 · 2008 · 2009