Fun in Nottingham, February 2007 →

Well, that was Fun

Our inaugural meeting was held in Oxford University Computer Laboratory on Thursday 16 November 2006, and... Wow! We filled a big room, we had some great talks, we went down the pub. On and off stage, the meeting more than fulfilled our hopes for its function. Well done, Jeremy! Many thanks to everyone who came and made this new seminar such a success.


As promised, here's the receipt for dinner. Curry, as it happens, in the function room of Bagicha, North Parade, Oxford.

Jeremy Said

It turns out that we are too numerous for the room I've booked. Happily, we have a new building nearing completion, as you'll note, and the lecture theatre of that is amply big enough and (nearly!) ready for use. You'll have to excuse the builders, the dust, and the lack of air conditioning, but I hope at this time of year it won't matter too much. It will be a good way to christen the place.

We'll have lunch beforehand and coffee in the middle in the social area in the basement of what used to be our new building, but will henceforth be called our middle-aged building. Local guides will show you around and let you through carded doors.

We'll retire afterwards to a local pub for further discussion. After that, some of us may want to stay for dinner. Can you let me know if you think you probably will? Also let me know if you have any dietary constraints. Then I'll try to book an appropriately-sized room somewhere. (I'll take a final headcount on the day, but an early estimate will help.)


  • 1200-1400 BYO sandwiches etc in the social area
  • 1400-1500 Phil Wadler (University of Edinburgh)
                        Links: web programming without tiers
    Phil's slides.
  • 1500-1530 coffee in the social area
  • 1530-1600 James Cheney (University of Edinburgh)
                        Mechanized Metatheory Model-Checking
    James's slides.
  • 1600-1630 Wouter Swierstra (University of Nottingham)
                        A Principled Approach to Version Control
    Wouter's slides.
  • 1630-1700 Andrew Kennedy (Microsoft Research, Cambridge)
                        C# is a functional programming language
    Andrew's slides in pdf and powerpoint.
  • 1700-1900 pub
  • 1900+        dinner


  • Mechanized Metatheory Model-Checking
    James Cheney (University of Edinburgh)

    Syntactic techniques based on operational semantics and type systems are extremely useful for studying the metatheory of logics and programming languages. However, proving properties of such systems is often an onerous task, because there are often a large number of "standard" or straightforward cases. It is tempting to cut corners and do careful proofs only for cases that seem interesting, but this can easily lead to a counterexample being missed. It therefore seems attractive to try to formalize such proofs in order to ensure their validity. However, this cure is often worse than the disease, since theorem proving tools tend to have a high learning curve. Moreover, theorem proving generally addresses the uncommon case of formalizing an informal proof of a well-understood system which has stood the test of time, rather than the common case of finding a bug in a poorly-understood system that may still be under development.

    Based on envious observations of the success of formal methods for verifying industrial hardware designs using model-checking, I will argue that "partial" techniques which provide full automation and search for counterexamples, but which do not try to verify correctness, are likely to be more useful on a day-to-day basis activities than full verification. I will describe an unsophisticated, yet useful, implementation of such a "model-checking" approach to mechanized metatheory implemented using nominal logic programming (although the basic idea could be employed in many other settings).

  • A Principled Approach to Version Control
    Wouter Swierstra (University of Nottingham)

    Version control systems are essential for managing the distributed development of large software pro jects. We present a formal model for reasoning about version control. In particular, we give a general definition of patch. Patches abstract over the data on which they operate, making our framework equally suited for version control of everything from highly-structured XML files to blobs of bits. We model repositories as a multiset of patches. The mathematical definitions of patches and repositories enable us to reason about complicated issues such as conflicts and conflict resolution.

  • C# is a functional programming language
    Andrew Kennedy (Microsoft Research, Cambridge)

    Polymorphic functions, parameterized types, lambda expressions, type inference, streams, GADTs, and combinator libraries: these are features usually associated with functional languages such as Haskell and ML. In this talk I will show how the design of C# 3.0, launching next year, was strongly influenced by ideas from functional programming, and supports all these features. I will use classic examples from the functional programming literature to illustrate the talk.