|← Fun in Kent, November 2008||Fun in Nottingham, May 2009 →|
It's Fun up North! Come for a grand afternoon in Leeds, on the afternoon of Tuesday, 3 March 2009.
Do please drop me an email if you're thinking of attending. IMPORTANT: For planning, please state whether you'll be here for lunch and/or joining us for dinner. For those coming by car, parking can be reserved, but you will need to send your registration number, too. If you want to come to the dinner, or need a car parking reservation, please email me by NO LATER than 12:00 on Friday 27th.
We'll meet up from 12 noon for lunch, with talks starting at 2pm. Dinner is planned for 6.00pm, details will be forthcoming (probably at Brio's, an Italian restaurant) - we will need numbers to make a booking.
We're currently seeking offers of talks. So if you have something you'd like to share, please send a title and abstract to David Duke (djd at comp . leeds . ac . uk), by Wednesday 4th February.
The meeting will be held in the Common Room of the School of Computing (SoC) at the University of Leeds. SoC is situated in the EC Stoner building, Number 78 on the campus map, between staircases 1 and 2 (marked on the map in small red circles - it's a loooong building!). If any requires access by lift, there is one available in staircase 2. The Common Room is room 9.21, which is actually only two floors up from the main entrance, as level numbers are absolute, starting from some way down the hill!
For those hunting for lunch, there are a number of "sandwich" bars across campus, or numerous outlets between the train station and University - further details will be provided closer to the date. David adds: Lunch: if you're coming by train, there are numerous outlets at the station (including for example an M&S food place in one corner), and on the walk from station to the University. For those coming by car, or wanting to explore the campus, there is a cafe offering sandwiches, pastries, soup etc on level 10 of the EC Stoner building (2 min walk from 9.21), or for a larger range of options, there is the student union shop and refectory, building 32 on the campus map, 5-10mins walk.
Please do contact David if you have any general questions, or need any further arrangements.
How To Get Here
Leeds is well connected by road and rail, with services on major routes including those to London, Edinburgh, Manchester, and Birmingham. The University is close to Leeds city centre, a 15 minute walk from the Railway Station or 5 minutes in a taxi. General information on travelling to the University can be found at http://www.leeds.ac.uk/visitors/getting_here.htm. Typing "EC Stoner Building, University of Leeds" into maps.google.co.uk shows exactly where we are as the first search result, and you can also use the map to augment the written directions. For anyone coming from further afield, Leeds-Bradford airport is around 20-30 minutes by taxi, depending on traffic.
For people wanting to stay overnight, a list of suggestions can be provided; at this point please contact David directly.
|12.00 - 13.45||Lunch: BYO sandwiches, tea/coffee/fruit juice provided|
|13.45 - 14.30||Back to BASICs|
|Lennart Augustsson, Standard Chartered|
|14.30 - 15.00||Coffee|
|15.00 - 15.30||Resource-Aware Domain Specific Languages|
|Edwin Brady, University of St. Andrews|
|15.30 - 16.00||How to Keep Your Streams Flowing|
|Venanzio Capretta, University of Nottingham|
|16.00 - 16.30||Coffee|
|16.30 - 17.00||Verification via Supercompilation|
|Alexei Lisitsa, University of Liverpool|
|17.00 - 17.30||Supercompilation for Haskell|
|Neil Mitchell, Standard Chartered|
|17.30 - 18.30||Pub|
|18.30 -||Dinner (Brio's)|
Abstracts Alphabetically by Author
Back to BASICs
Lennart Augustsson, Standard Chartered
I will show how to embed a simple imperative language in Haskell. This part is mostly of hack value, but has a useful tidbit or two. I will also show how this embedded language can be translated to LLVM code with the Haskell to LLVM bindings.
Resource-Aware Domain Specific Languages
Edwin Brady, University of St. Andrews
The well-typed interpreter has almost become the “hello world” of new dependently typed functional programming languages. However, the type sytems implemented in these examples are typically very simple and translate directly to the host language. The technique becomes much more valuable when used to express other static properties, such as safe resource usage. The challenge is to keep the notational overhead low while retaining compositionality and correctness. In this talk, I will describe the embedding of a resource aware domain specific language for safe memory management in Idris, an experimental functional language with dependent types, and explore the techniques and notations which will be required to make such languages realistic in practice.
How to Keep Your Streams Flowing
Venanzio Capretta, University of Nottingham
Consider the following two functional programs:
g : Nat → Stream(Nat)
g 0 = [0..]
g 1 = [1..]
g n = map (+) (g (n-1)) (g (n-2))
f : Nat → Stream(Nat)
f n = n :: merge (f (2n)) (f (2n+1))
(where merge interleaves the elements of two streams)
They have the same type and a similar structure: fg = β . (fg x fg) . α where α : Nat -> Nat² and β : Stream(Nat)² → Stream(Nat). They both define total functions but the reason is different. For g, it is α that guarantees totality (i.e. termination); it is a “recursive coalgebra”. For f, it is β that guarantees totality (i.e. productivity); it is a “corecursive algebra”. Programming with and reasoning about recursive algebras is well-known. I will introduce the computational and logic principles related to corecursive algebras.
One surprising fact is that there is a disconnection between the natural programming method (that of corecursion) and the natural logic principle (that of bisimulation). I will show you that it is possible to have productive programs that do not satisfy the principle of bisimulation and vice versa, there are algebras that satisfy bisimulation but fail to give good corecursion. This is in contrast with the dual case, where recursion corresponds very well with induction.
I will also introduce you to a line of research that tries to identify when a set of corecursive equations can be solved by a unique total function; that is, when a functional program on coinductive types is productive.
Verification via Supercompilation
Alexei Lisitsa, University of Liverpool
V. Turchin has proposed around 1980 the following scheme using program transformation for proving properties of the functional programs: “...if we want to check that the output of a function F(x) has the property P(x) we can try to transform the function P(F(x)) into an identical True.” In the work joint with Andrei Nemytykh we extended Turchin's proposal to the verification of parameterized nondeterministic protocols using a particular scheme of “parameterized testing + supercompilation”. In the talk I will overview this verification via supercompilation technique and illustrate it by the case studies.
Supercompilation for Haskell
Neil Mitchell, Standard Chartered
Haskell supports features such as higher order functions and lazy evaluation, which allow succinct programs, but can be difficult to compile efficiently. This talk describes how supercompilation can be used to optimise Haskell programs. Combining supercompilation with GHC can lead to performance improvements over GHC alone.