|← Fun in Oxford, February 2012||404, who knows where →|
We haven't had much Fun lately, so it's high time we had some more. Miles Sabin (milessabin.com) has kindly agreed to host us in Brighton, on 14th November. More local details will follow, but I wanted to get the date in your diaries, and also to solicit speakers. Please let me know if you'd like to give a talk! Conor, Graham, and I are all in Copenhagen at ICFP this week, so if you're there too, feel free to grab one of us.
|14:00–14:45||Simon Thompson: Let's make refactoring tools user extensible! Let's make refactoring tools user extensible!|
|14:45–15:15||Alexei Lisitsa: Cryptographic protocols verification via supercompilation Cryptographic protocols verification via supercompilation|
|16:00–16:30||Yingzhou Zhang: Monadic Program Slicing Monadic Program Slicing|
|16:30–17:00||Nigel Warren: Exocute - Unwired Processing Pipelines at Scale Exocute - Unwired Processing Pipelines at Scale|
|17:00–17:30||Conor McBride: Frank, a direct style language with typed effects Frank, a direct style language with typed effects|
Let's make refactoring tools user extensible!
I will present a framework for making a refactoring tool extensible, allowing users to define refactorings from scratch using the concrete syntax of the language, as well as to describe complex refactorings in a domain-specific lan- guage for scripting. I will demonstrate the approach in practice through a series of examples.
The extension framework is built into Wrangler, a tool for refactoring Erlang programs, but would argue that the approach is equally applicable to tools for other languages.
Cryptographic protocols verification via supercompilation
V. Turchin around 1980 has proposed the following scheme for proving properties of the functional programs using program transformation: "...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 non-deterministic protocols (e.g. cache coherence protocols) using a particular scheme of "parameterized testing + supercompilation."
This work has been presented in a talk on Fun Meeting in March 2009, Leeds. In this talk we will present the basics of the approach and its further developments towards the verification of cryptographic protocols. The protocols are specified/modeled by functional programs at different levels of abstraction, and verification is done using Turchin's supercompilation method.
Monadic Program Slicing
Program slicing is a well-known program analysis technique that extracts the elements of a program related to a particular sub-computation. Current slicing methods, however, are specialised to program dependence graphs (PDG), and lack good composability and parallelizability. Therefore, we present a novel formalism for program slicing—monadic program slicing—which abstracts the computation of program slicing as a slice monad transformer, and applies it to semantic descriptions of the program in a modular way.
Monadic slicing algorithms allow program slices to be computed directly on abstract syntax, with no need to explicitly construct intermediate structures such as dependence graphs or to record any execution history. The monadic abstraction mechanism ensures that our monadic slicing methods have excellent flexibility, composability and parallelizability.
Exocute - Unwired Processing Pipelines at Scale
In this talk we present work undertaken at Brunel University on the Exocute project. This project imagines a design space in which processing elements are manifold and network bandwidth is bountiful. At this change in scale we propose that distributed systems begin to look more like biological systems and less like traditional computing platforms. Among other factors considered in the design are:
- Dynamic construction of virtual processing pipelines expressed as Type transition graphs - passing immutable state between systems components
- The overlapping lifetimes of processes, data structures and hardware components
- Cellular Analogy
- Intercellular signalling
- Apoptosis (PCD)
- Dynamic load balancing by consensus
- Dynamic discovery and identification
- The use of Object Spaces (Fly) as a generic communication medium.
We will also present some examples of writing worker cells to the Exocute model in Scala.
Frank, a direct style language with typed effects
Frank is an experimental typed functional programming language I've been quietly working on since 2007. It resembles Bauer and Pretnar's Eff, in that it supports direct style programming with side effects. However, it has a type system which makes clear which effects are available at any point and ensures that programs perform only available effects. Code thus resembles ML but types resemble those of Haskell, except that it is always clear which parts of types describe values and which describe effect permissions, reducing the need for plumbing operators like >>= and <*>.
As in Eff, effects are specified via interfaces of operations, and the permitted effects are locally renegotiable by specifying how new operations are to be handled. Frank types are effect-polymorphic in that they express requirements on and amendments to an arbitrary and nameless ambient set of permitted operations. This polymorphism is so neatly invisible that convincing anonymous referees it exists is sometimes difficult: it boils down to writing the type for map and the code for map, then discovering it's actually the monadic mapM. I implemented a version of Frank earlier this year, so I'll finish with a demonstration.