| Fun in Nottingham, February 2007 → |
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.
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.)
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).
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.
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.