2017 competition
Winner
Algebraic Subtyping
Stephen Dolan, University of Cambridge
Type inference gives programmers the benefit of static, compile-time type checking without the cost of manually specifying types, and has long been a standard feature of functional programming languages. However, it has proven difficult to integrate type inference with subtyping, since the unification engine at the core of classical type inference accepts only equations, not subtyping constraints.
This thesis presents a type system combining ML-style parametric polymorphism and subtyping, with type inference, principal types, and decidable type subsumption. Type inference is based on biunification, an analogue of unification that works with subtyping constraints.
Making this possible are several contributions, beginning with the notion of an "extensible" type system, in which an open world of types is assumed, so that no typeable program becomes untypeable by the addition of new types to the language.
While previous formulations of subtyping fail to be extensible, this thesis shows that adopting a more algebraic approach can remedy this. Using such an approach, this thesis develops the theory of biunification, shows how it is used to infer types, and shows how it can be efficiently implemented, exploiting deep connections between the algebra of regular languages and polymorphic subtyping.
View Stephen Dolan's dissertation
Highly commended
Security in Next Generation Air Traffic Communication Networks
Martin Strohmeier, University of Oxford
A multitude of wireless technologies are used by air traffic communication systems during different flight phases. From a conceptual perspective, all of them are insecure as security was never part of their design and the evolution of wireless security in aviation did not keep up with the state of the art.
Recent work has exploited this inherent vulnerability and revealed a discrepancy between the perspectives of security researchers and the aviation community. This thesis bridges this gap and combines wireless security knowledge with the perspective of aviation professionals to improve the safety of air traffic communication networks.
It develops a new threat model and examines the awareness of the aviation community concerning the security of their wireless systems. We analyse all potential vulnerabilities and collect expert opinions on the impact of concrete attack scenarios using insecure technologies.
Based on our analysis, we propose, implement, and evaluate novel cyber-physical means to secure air traffic communication, which work transparently alongside existing technologies and can immediately improve their security under existing real-world constraints.
