Scottish Programming Languages Seminar

The importance of reasoning about and refactoring programs is a central tenet of functional programming. Yet our compilers and development toolchains only provide rudimentary support for these tasks. To address this, we have implemented HERMIT, a toolkit enabling informal but systematic transformation of Haskell programs from inside the Glasgow Haskell Compiler's optimization pipeline. With HERMIT, users can experiment with optimizations and equational reasoning, while the tedious heavy lifting of performing the actual transformations is done for them.

HERMIT provides a transformation API that can be used to build higher-level rewrite tools. In this talk I will describe our principal HERMIT application---a read-eval-print shell for performing transformations using HERMIT. I will also demonstrate using this shell to prototype an optimization on a specific example, and discuss our experiences and remaining challenges.

The EU ParaPhrase Project is investigating new approaches to programming parallel computing systems using high-level patterns of parallelism to target heterogeneous parallel platforms. In order to do this effectively, it is necessary to construct good timing models and analyses.

The relaxed-memory concurrency protocols that are enforced by commonly used hardware, such as x86 multicores and some ARM multicores, have complex functional and timing behaviours. Understanding these behaviours is crucial to constructing good timing analyses for these architectures, that can be used to predict parallel performance. This talk takes a principled and rigorous approach to relaxed memory concurrency, building on the functional and behavioural semantics of primitive x86 concurrency primitives including atomic memory exchanges, memory fences and a detailed cache model, to build accurate high-level timing analyses for some key high-level patterns of parallelism. The talk shows that using these analyses, it is possible to accurately predict timing behaviour for real x86 multicores.

Invariance is of paramount importance in programming languages and in physics. In programming languages, John Reynolds’ theory of relational parametricity demonstrates that parametric polymorphic programs are invariant under change of data representation, a property that yields “free” theorems about programs just from their types. In physics, Emmy Noether showed that if the action of a physical system is invariant under change of coordinates, then the physical system has a conserved quantity: a quantity that remains constant for all time. Knowledge of conserved quantities can reveal deep properties of physical systems. For example, the conservation of energy, which by Noether’s theorem is a consequence of a system’s invariance under time-shifting.

In this talk, I'll link Reynolds’ relational parametricity with Noether’s theorem for deriving conserved quantities. I propose an extension of System Fω with new kinds, types and term constants for writing programs that describe classical mechanical systems in terms of their Lagrangians. I'll show, by constructing a relationally parametric model of our extension of Fω, that relational parametricity is enough to satisfy the hypotheses of Noether’s theorem, and so to derive conserved quantities for free, directly from the polymorphic types of Lagrangians expressed in our system.

In this talk I will present a type methodology combining linear types with lightweight dependent types and how to use it in program analysis. Linear types are useful for expressing properties of functions in terms of the usage of their input; lightweight dependent types are useful for describing the behavior of the program in terms of its control flow. These two ideas fit together well when one is interested in analyzing properties of functions depending on the control flow of the program. I will present these ideas in the context of sensitivity analysis for differential privacy.

You put your output in,
You get your input out,
Putc, Getc, shake it all about,
Jack plugs, cables, side effects,
That's what it's all about...

Without I/O, computation is mere mathematical whimsy, yet programming languages tend to treat I/O as an afterthought. In this rambling brain dump, we will survey the peculiar history of programming language I/O, deploying specious taxonomies to try and tease out and critique I/O design choices.