|← Fun in Cambridge, May 2007||Fun at Credit Suisse, February 2008 →|
FUN in the AFTERNOON at YORK
Thursday, 22 November 2007
Venue and Transport
We'll be meeting in the Haycox Lecture Room of the Department of Computer Science on the Heslington Campus of the University of York, YO10 5DD.
York has good rail links. From the station, it takes about 20 minutes to get to the campus by bus (number 4, every 10 minutes) or by taxi.
If you plan to come by car I *cannot* reserve a parking space for you, but I can at least provide a visitors' permit so that you don't have to pay the usual fee. Please ask in advance.
See http://www.york.ac.uk/np/maps/ for more information about where we are and how to get here.
Alan Mycroft points out that people coming by train on a GNER route may be able to get very cheap tickets:
Food and Drink
The CS department is not a suitable venue for meals. So if you arrive wanting to have lunch before the talks, please find somewhere to eat on campus or in nearby Heslington village. For example:
- if you are short of time or energy, one option is right next to the CS building at the side of the library -- the Freshers snack-bar serves things like soup & baguettes;
- still within the university, but a short walk round the lake to Wentworth Graduate College, the Edge cafeteria is my own preference when eating on campus -- a modest selection but good quality:cost ratio;
- if you fancy a pub lunch, a ten-minute walk will take you just off campus and into Heslington where The Charles XII will oblige;
- also in Heslington is the ever-popular Browns bakery and grocery, with an excellent selection of baked goods, along with a hot-food counter, fruit, drinks etc.
After the afternoon's programme of talks, as FitA tradition demands, we'll go for a Curry at a restaurant.
Schedule of Talks
|14.00 - 14.45||R* is the new [a]|
|Conor McBride, University of Nottingham|
|14.45 - 15.00||1st break|
|15.00 - 15.25||Static contract checking for Haskell|
|Dana Xu, University of Cambridge|
|Dana's slides in .ppt and .pdf|
|15.25 - 15.50||Program specialization by graph reduction|
|Mike Thyer, Cyan Technology|
|Mike's animated applet|
|15.50 - 16.10||2nd break|
|16.10 - 16.35||Typechecking XML updates|
|James Cheney, University of Edinburgh|
|16.35 - 17.00|| Lazy SmallCheck:
exhaustive, demand-driven testing in Haskell
|Matthew Naylor, University of York|
|Matthew's slides and a relevant link|
R* is the new [a]
Conor McBride, University of Nottingham
Lists are ubiquitous in functional programming, often receiving privileged notation and a great deal of attention in standard libraries. Lists have both container-like structure and monadic structure. However, this flexibility can sometimes be a source of trouble: list types are often used brutally to represent sequential data with other crucial structure (size, order, signature, etc) unaccounted for. Generic list-based operations are thus applicable, but not necessarily in a meaningful way.
As dependently-typed programming has emerged, we have seen the notion of list fragmented into many distinct sequential structures, each enforcing its own peculiar invariant. This leads to neat solutions for small examples but a clear and dangerous code re-use problem. In this talk, I investigate the possibility of abstracting over the invariants, restoring a uniform presentation of sequential data. In particular, I propose reflexive-transitive closure, R*, as the dependent analogue of the general notion of list, and show how a variety of dependent list-like structures from the literature can be so encoded. I examine what sort of general library support we can expect for *, in the light of its structural properties. This is joint work with Ulf Norell and Patrik Jansson.
Static contract checking for Haskell
Dana Xu, University of Cambridge
Program errors are hard to detect and are costly both to programmers who spend significant efforts in debugging, and to systems that are guarded by runtime checks. Static verification techniques have been applied to imperative and object-oriented languages, like Java and C#, but few have been applied to a higher-order lazy functional language, like Haskell. In this paper, we describe a sound and automatic static verification tool for Haskell, that is based on contracts and symbolic execution. Our approach gives precise blame assignments at compile-time in the presence of higher-order functions and laziness.
Program specialization by graph reduction
Mike Thyer, Cyan Technology
This talk will demonstrate novel graph reduction techniques which use reduction beneath lambdas to achieve program specialization. Unlike other partial-evaluation and meta-programming systems, functions rather than annotations are used to control the specialization. This enables a more dynamic form of specialization where the specializing effect is inherited by interpreted languages. This inherited specializing effect will be graphically demonstrated.
Typechecking XML updates
James Cheney, University of Edinburgh
A wide variety of languages have been developed for transforming or querying XML, many with strong static type systems based on regular expressions. However, updates are also important for XML databases. Update languages for relational databases are specialized towards expressing transformations that are "mostly the identity" and can be executed efficiently "in-place", and so existing statically typed XML transformation and query languages are not directly useful for writing updates. Recent proposals for XML update languages to complement XQuery take an imperative approach which, to me at least, sacrifices many of the benefits of XQuery's purely functional design - including static typing and optimization based on equational laws. Worse, some designs propose allowing updates within queries - so these benefits of XQuery's design also disappear in the presence of updates.
In this talk I will describe what I think is wrong with the imperative approach and present the semantics and type system of Flux, a "functional" XML update language with static typechecking.
Lazy SmallCheck: exhaustive, demand-driven testing in Haskell
Matthew Naylor, University of York
If there is any case in which a program fails, there is almost always a simple one, and the simplest cases are the easiest to investigate. Such observations motivate the development of SmallCheck, a library that tests program properties for all fully-defined values up to some size. This talk presents a variant called Lazy SmallCheck, which generates partially-defined inputs that are progressively refined as demanded by the property under test. The key observation is that if a property evaluates to True or False for a partially-defined input then it would also do so for all refinements of that input. By not generating such refinements, Lazy SmallCheck may test the same input-space as SmallCheck using significantly fewer tests, allowing larger input spaces to be checked in a given amount of time.
This talk presents examples and comparisons that motivate the use of Lazy SmallCheck, and discusses the relationship between Lazy SmallCheck and recent testing tools based on lazy narrowing and similar techniques. The talk represents joint work with Fredrik Lindblad and Colin Runciman.