ETAPS report (finally)

I've been putting this off for ages and I've finally lost motivation to write a new report. Instead I will reprint the report I produced as part of my funding requirements. Sorry it's not as good as some of the other conference reports. Lesson learned: write the blog as you go, don't leave it until later.


The YOGI Project: Software Property Checking via Static Analysis and Testing

This project sought to combine static analysis with testing to verify programs written in C. The main application has been to verify drivers; at which it has, apparently, been successful. The system is of course undecidable --- it is possible that their algorithm does not terminate. If the algorithm does terminate, then it either finds an error in the code or produces a proof that the program satisfies its specification.

Well-Typed Programs can't be Blamed

This paper (presented brilliantly by Phil Wadler) is another step towards combining dynamic and static typing. The main contribution is that defiing the `can't be blamed' property: ``in a program with both dynamic and statically typed parts, if a type error occurs, then it must be the fault of the dynamically typed part''. This is essentially a formulation of type soundness for hybrid/gradually typed systems.

I found the four variations of subtyping, and how these relate with co- and contravariance, very interesting.


Exploring the Design Space of Higher-order Casts

Similar to the previous talk , this work addresses the problem of type safety in hybrid/gradually typed systems. The contribution here is the use of higher-order casts, that is, casts over function types (which cannot be statically checked). By labelling each cast (with blame labels) and propagating these labels during execution, the source of runtime errors can be accurately reported.

The system is formalised using a calculus with coercions to model casts; coercions are normalised, and blame labels propagated through normalisation. Several approaches for assigning blame are presented.

I particularly like this work as inaccurate error messages are a very real problem when programming, and this paper presents a solution to some of these problems.


Is Structural Subtyping Useful? An Empirical Study

This work presents an empirical study of Java programs and shows that certain benefits of structural subtyping may be beneficial in a Java-like language. The motivation is that dynamic languages with structural typing are growing in popularity, and so it is sensible to ask if elements of these systems could be useful in more static languages.

The study was undertaken by inferring structural types in the programs and checking when the nominal types were too precise in comparison to the (minimal) structural types. These results were further broken down into cases where there is no possible nominal supertype and where there is; the implication being that in the former case, structural types would be of benefit.

The study found that most types were over-specified (which is unsurprising --- one wouldn't expect all fields and methods of a class to be used in every method), but furthermore that suitable nominal types did not usually exist, that the required structural types were usually small, and that these structural types were not used often --- which implies that they are not worth making into named interfaces.

My criticism of the work is that just because some of the benefits of structural types are beneficial does not mean that structural types are the best solution, and this aspect is not addressed in the paper. That said, the analysis itself is important and, without the link to motivating structural types, ranks as one of the most interesting papers in the conference.


An Interval-based Inference of Variant Parametric Types

This talk presented an interesting and useful way to infer inference annotations. However, the talk was let down by some misunderstandings of variant parametric types and Java wildcards, for example, assuming they have the same semantics, which is wrong. It was also unclear what role annotations on receivers played in the inference algorithm, versus being present in the source language.


The Financial Crisis, a Lack of Contract Specification Tools: What can Finance Learn from Programming Language Design


This was an interesting, mostly non-technical, invited talk which described a mechanism for sepcifying financial contracts using types. The author spoke about some details of their system and his business which runs it. The motivation is that financial trades are not well-understood, in particular, the contracts which specify them are informal and imprecise. The solution is essentially modelling trades like a programming language entity.


Global Principal Typing in Partially Commutative Asynchronous Sessions

The contribution of this work is a session based type system for the Pi Calculus and some interesting meta-theoretic results. Subtyping is sound and complete, and inference is shown to find a principal typing.


Automatic Parallelisation with Separation Logic

This work uses separation logic to perform an independence analysis of expressions. A trace semantics with sophisticated labelling facilitates this. The result is an analysis of a program's footprint which can be used to parallelise expressions.


Deny-Guarantee Reasoning

This work extends rely-guarantee reasoning to handle fork/join concurrency. The crucial concept is interference: some action which affects the state of the program; rely-guarantee creates interferences, but interference must be constant to support forking. Deny-guarantee uses separation logic techniques to split interference, this is used to ensure consistency of interference across forked threads. This technique is similar to fractional permissions. Another crucial concept is the thread predicate, which is a predicate in separation logic which gives a postcondition when and if a thread is joined.


A Basis for Verifying Multi-threaded Programs

Based on fractional permissions, this idea supports complex concurrency primitives (including fork/join, as in the previous talk). Permissions are extended with more complex operations, such as sharing and unsharing. Complex specifications can be written and verified by the system, which also prevents deadlock.