|← Fun in Nottingham, May 2009||Fun at Standard Chartered Bank, February 2010 →|
Simon M says
A date for your diaries: the next “Fun in the Afternoon” will be held at Microsoft Research, Cambridge, on Thursday 26 November.
Fun in Cambridge is taking shape; we have a preliminary program (below). I'll announce the final program and local arrangements shortly.
If you would like to come, please email firstname.lastname@example.org with your name and affiliation, by Friday 20 November (late registrations will probably be accommodated, but it will help if we can get an idea of the numbers a few days in advance).
|12.00 - 13.00||Lunch: various local options|
|13.00 - 13.30||F-ing modules|
|Andreas Rossberg, Max Planck Institute for Software Systems|
|13.30 - 14.00||Distributive Laws in Programming Structures|
|Ondrej Rypacek, University of Nottingham|
|14.00 - 14.30||Break|
|14.30 - 15.00||ΠΣ: Dependent Types Without the Sugar|
|Thorsten Altenkirch, University of Nottingham|
|15.00 - 15.30||Canonical Logical Frameworks|
|Robin Adams, Royal Holloway, University of London|
|15.30 - 16.00||Break|
|16.00 - 16.30||Dynamic analysis in the Reduceron|
|Matthew Naylor, University of York|
|16.30 - 17.00||Slicing It|
|Thomas Schilling, University of Kent|
|17.30 - 18.30||Pub|
Abstracts Alphabetically by Author
Canonical Logical Frameworks
Robin Adams, Royal Holloway, University of London
A canonical logical framework, or lambda-free logical framework, is a logical framework that deals only with objects in beta-normal, eta-long form. The concept has been invented independently three times over the last 15 years or so: by Aczel, with the Type Framework TF; by Watkins et al, with the Canonical Logical Framework, and by Plotkin, with DMBEL.
I shall show how all these frameworks can be fitted into a hierarchy such that they extend one another conservatively. I shall also demonstrate the main selling point of canonical LFs: certain results can be proven more easily in a canonical LF, then 'lifted' - that is, the same result proven for a traditional LF as an immediate corollary.
ΠΣ: Dependent Types Without the Sugar
Thorsten Altenkirch, University of Nottingham
(Based on joint work with Nils Anders Danielsson, Andres Löh and Nicolas Oury)
The recent success of languages like Agda and Coq demonstrates the potential of using dependent types for programming. These systems rely on many high level features like datatype definitions, pattern matching and implicit arguments to facilitate the use of the language. However, these features complicate the metatheoretical study and are a potential source of bugs.
To address these issues we introduce ΠΣ, a dependently typed core language. It is small enough for metatheoretical study and the typechecker is small enough to be formally verified. In this language there is only one mechanism for recursion---used for types, functions and infinite objects---and an explicit mechanism to control unfolding, based on lifted types. Furthermore structural equality is used consistently for values and types; this is achieved by a new notion of α-equality for recursive definitions.
We show, by translating several high-level constructions, that ΠΣ is suitable as a core language for dependently typed programming. We also provide a formal description of the language and its typing rules.
See also: our recent paper (with the same title) or/and download pisigma from hackage.
Dynamic analysis in the Reduceron
Matthew Naylor, University of York
The Reduceron is a graph-reduction machine implemented on a field-programmable gate array (FPGA). Last year, we reviewed the machine and set out to improve its runtime performance by a factor of six. If achieved, the performance of leading PC and FPGA implementations of graph-reduction would be on a par for a common class of programs --- an unusual and intriguing state of affairs for such a general-purpose processor.
In this talk, I will present our progress towards this goal, beginning with an overview, and then focusing on two recently added features: update avoidance and speculative evaluation of primitive redexes. Both enjoy the accuracy and simplicity of dynamic analysis without incurring the runtime overhead that often makes static analysis perferable in a conventional setting.
This talk represents joint work-in-progress with Colin Runciman.
Andreas Rossberg, Max Planck Institute for Software Systems (with Claudio Russo and Derek Dreyer)
ML modules are a powerful language mechanism for decomposing programs into reusable components. They also have a reputation for being complex, and dependent on fancy type theory that is mostly opaque to non-experts. While this reputation is certainly understandable, we aim here to demonstrate that it is undeserved. To do so, we give a very simple elaboration semantics for a full-featured, higher-order ML-like module language. Our elaboration defines the meaning of module expressions by a straightforward, compositional translation into vanilla System F (the polymorphic lambda-calculus), under plain F typing contexts. We thereby show that modules are merely a particular mode of use of System F.
Our module language supports the usual second-class modules, with SML- style generative functors and local modules. To demonstrate the versatility of our approach, we further extend the language with the ability to package modules as first-class values -- an almost trivial extension, as it turns out. (Our approach also scales to handle OCaml- style applicative functor semantics, but the details are significantly more subtle, so we will not present them here.)
Lastly, we report on our experience using the "locally nameless" approach in order to mechanize the soundness of our elaboration semantics in Coq.
Distributive Laws in Programming Structures
Ondrej Rypacek, University of Nottingham
Distributive laws in Computer Science are in general rules governing the transformation of one programming structure into another. In functional programming, they are parametrically polymorphic functions with a characteristic type "swapping the order of two parameterized-type constructors". Their importance has been noted but to date documented only in several isolated cases and by diverse formal approaches such as Backouhse & Hoogendijk's zips, Meertens' functor pullers or McBride's idiomatic functors.
In this talk, a formal approach to distributive laws in programming structures will be presented, which discloses their simple nature, a uniform approach to elementary constructions on them and their precise relationship to similar notions elsewhere in Category Theory. Although the approach rests formally on deep results from 2-Category Theory, the presentation will be geometrical as much as possible, making use of the wonderful three dimensional nature of 2-categories.
Thomas Schilling, University of Kent
Haskell's type error messages are often not as helpful as they could be. One fundamental problem is that they blame a single location while several other locations may fix the error as well. A type error slice does not blame a single location, but a fragment of the failing program.
Previous work on type error slices requires reformulating type checking as a constraint solving problem. This makes it very difficult to integrate support for type error slices into existing compilers. In this talk I present how we can overcome this limitation by requiring only a very basic interface to the type checker.