The next Scottish Programming Languages Seminar will be held on Tuesday 15th March 2011 at the Informatics Forum, University of Edinburgh. The organisers are Brian Campbell and Sam Lindley.
The seminar will be held at the Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB. A map showing the Forum is available. The entrance is opposite that of Appleton Tower.
Lunch will be available from around 1pm, and the talks will start at 2pm. The programme is below. We expect to finish around 5.40pm, after which we will head to a nearby pub.
Our thanks to everyone who let us know that they would be coming. Everyone else is still welcome to attend, hopefully there will be enough food and refreshments for you, too.
Lunch and coffee breaks will be held in "Mini-Forum 2" (room 4.40 in the link below) - take the lift to the fourth floor and turn right; it is the large room at the end of the corridor. Talks will be held in room 4.31/4.33 - from the lifts turn right, then right again into another corridor. The room is the glass-walled meeting room on the inside of the building. You can see it from the lift on the way up.
We will have signs directing you to both rooms on the day.
SPLS receives financial support from the Complex Systems Engineering theme of SICSA, the Scottish Informatics and Computer Science Alliance.
In this talk I will give an overview of the LiquidMetal project at IBM (www.research.ibm.com/liquidmetal/) and present some preliminary results for the GPU backend which I developed in collaboration with IBM. LiquidMetal aims to address the difficulties that programmers face today when developing applications for computers that feature programmable accelerators (GPUs and FPGAs) alongside conventional multi-core processors. It offers a single unified programming language called Lime and a runtime that allows (all) portions of an application to move fluidly between hardware and software, dynamically and adaptively.
We present a brief overview of a framework for defining abstract interpreters for liveness properties, in particular program termination. The framework makes use of the theory of metric spaces to define a concrete semantics, relates this semantics with the usual order-theoretic semantics of abstract interpretation and identifies a set of conditions for determining when an abstract interpreter is sound for analysing liveness properties. Our soundness proof of the framework is based on a novel relationship between unique fixpoints in metric semantics and post-fixpoints computed by abstract interpreters.
This talk is based on the paper Metric Spaces and Termination Analysis from APLAS 2010.
|1500||Tea and coffee break|
A type system extended with units of measure allows static checking of unit consistency, ensuring, for example, that numbers with different units can be multiplied but not added. Kennedy describes an elegant system of units of measure that supports polymorphism, and which has been implemented in the functional programming language F#. This system models units as elements of a free abelian group, for which unification is decidable and has most general solutions, so type inference is possible. However, the system interacts awkwardly with the let-generalisation step of the Damas-Milner algorithm, and the F# implementation fails to infer principal types. I present an approach to unification and type inference based on minimal-commitment problem solving in a structured context, for which generalisation is simple. Type inference for the system of units of measure is then straightforward.
Hypernumbers are a small cash-flow positive Edinburgh startup in the End-User Programming space. End user programming for the desktop is dominated by Microsoft Excel and Microsoft Access and Hypernumbers are trying to extend that market to the web space. The spreadsheet is an expression-based functional programming paradigm and the strategic aim is to make the entire internet an expression-based FP.
|1620||Tea and coffee break|
I'll describe and demonstrate a resource analysis tool for Java bytecode which uses a technique (due to Bob Atkey, and related to work by Steffen Jost and Martin Hofmann) combining separation logic and amortisation.
Parser combinators are a popular method for constructing parsers within functional programming languages. The advantages of parser combinators include the ability to change the language being parsed on-the-fly: either before parsing starts or during parsing, based on previous input. In this talk I will discuss three popular interfaces for parser combinators---monadic, applicative functor and arrow based---and discuss their relative strengths. I will also discuss how to adapt parser combinators to parse grammars that are traditionally difficult for them, including left recursion and high levels of ambiguity, by adapting Earley's algorithm for general context-free grammars.