Having FUN in the afternoon

So, high time we had some FUN in the afternoon. More details are available here: http://sneezy.cs.nott.ac.uk/fun/2012-11/ Otherwise, the agenda for the day is posted below!

13:30-14:00 Registration

14:00-14:45 Let's make refactoring tools user extensible!, Simon Thompson

14:45-15:15 Cryptographic protocols verification via supercompilation, Alexei Lisitsa

15:15-16:00 Break

16:00-16:30 Monadic Program Slicing, Yingzhou Zhang

16:30-17:00 Exocute - Unwired Processing Pipelines at Scale, Nigel Warren

17:00-17:30 Frank, a direct style language with typed effects, Conor McBride

Followed by a visit to the pub and the traditional post-Fun curry ... We've tentatively picked the Fountain Head (http://www.drinkinbrighton.co.uk/fountain-head) as the pub venue and have a reservation for up to 20 at Noori's (http://www.noorisbrighton.co.uk/) for 7pm.

Abstracts

Let's make refactoring tools user extensible!, Simon Thompson

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, Alexei Lisitsa

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, Yingzhou Zhang

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, Nigel Warren

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, Conor McBride

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.