Lightning talks are your chance to give a quick introduction to your research and your interests. All talk slots are now full! We will have the following schedule for the talks:

	Tuesday 6 August	Thursday 8 August
17.05-17.10	Wadler (slides)	Lukyanov (slides)
17.10-17.15	Urlea (slides)	Friedemann (slides)
17.15-17.20	Goes (slides)	Cowderoy (slides)
17.20-17.22	van Heerdt (slides)	Zetzsche (slides)
17.22-17.27	Yao (slides)	Zalakain (slides)
17.27-17.33	Leijnse (slides)	Westphal (slides)
17.33-17.38	Lambert (slides)	Valliappan (slides)
17.38-17.43	Nagashima (slides)

If you are a speaker, please send the organisers your slides before the coffee break before your talk, so that we can ensure lightning fast handover between talks.

Abstracts

Functional Compiler Engineer (slides)

Philip Wadler, University of Edinburgh

 

Efficient FPGA Cost-Performance Space Exploration Using Type-driven Program Transformations (slides)

Cristian Urlea, University of Glasgow

 

Juvix: Efficient dependently-typed smart contracts (slides)

Christopher Goes, Tendermint/Cosmos- Cryptium Labs

 

Categorical Automata Learning Framework (slides)

Gerco van Heerdt, University College London

 

Towards the Synthesis of Provably Secure Programs (slides)

Xiaomo Yao, KTH Royal Institute of Technology

 

Purely functional distributed programming (slides)

Adriaan Leijnse, Universidade NOVA de Lisboa

Distributed programming without spawning processes and sending messages! Relativistic Functional Reactive Programming replaces the impure notion of explicit communication of information between processes with the pure and composable notion of perception of facts propagating throughout the universe.

Open Games (slides)

Alasdair Lambert, University of Strathclyde

 

Automating Induction in Isabelle/HOL with DSLs (slides)

Yutaka Nagashima, Czech Technical University in Prague

Proof assistants, such as Isabelle/HOL, offer tools to facilitate inductive theorem proving. Isabelle experts know how to use these tools effectively; however they did not have a systematic way to encode their expertise. To address this problem, we present our domain-specific language, LiFtEr. LiFtEr allows experienced Isabelle users to encode their induction heuristics in a style independent of any problem domain. LiFtEr’s interpreter mechanically checks if a given application of induction tool matches the heuristics, thus transferring experienced users’ expertise to new Isabelle users.

Formalising Free Selective Functors in Coq (slides)

Georgy Lukyanov, Newcastle University

This talk will discuss a work-in-progress on encoding Free Selective Functors in Coq as an inductive data type and proving that this datatype is a lawful instance of Functor, Applicative and Selective. The encoding is challenging due to the non-uniformity of its constructors’ type indices, and it is interesting to observe the impact this feature imposes on proofs.

Using Automated Reasoning for Problems in Machine Learning (slides)

Arved Friedemann, Swansea University

Machine learning (ML) provides state-of-the-art performance in many tasks where the rules and representations required for classification cannot be described manually. However, due to the complexities in describing all potential behaviour for an input distribution, their use in safety critical systems is limited. For ML to be applicable for such systems, the robustness against noise, reachability, and similar must be verified. On the other hand, logical formulas, like circuit representations, are verifiable and can be inferred using synthesis techniques. We propose the usage of a Boolean Satisfiability (SAT) solver that uses unit propagation and clause learning to create a logical model that fits given observations and, in addition, can verify given safety criteria. As an outlook, the use of more expressive deductive systems will be discussed.

Information Awareness is Super Effective! (slides)

Philippa Cowderoy

Following what’s happening in a type system is difficult. I’m trying to do better by being more Information Aware, with the aid of Information Effects!

Automated Black-Box Verification of Networking Systems (slides)

Stefan Zetzsche, University College London

 

Type-checking session-typed pi-calculus with Coq (slides)

Uma Zalakain, University of Glasgow

This project formalises session types in Coq using a mix of continuation passing, parametric HOAS, dependent types and ad-hoc linearity checks. Each action that a process takes requires a channel capable of that action. The head of that channel’s type is then stripped off and its continuation is passed to the next action the process takes. Dependent types guarantee this continuation passing is correct by construction. The type of channels is parametrised over, so that users are unable to skip the proper mechanisms to create channels. The HOAS makes the syntax easy to use for both the end user and the designer: all variables are lifted to Coq, all typing judgments happen in Coq, no typing contexts are required. The continuation passing always creates channels that must be used exactly once. Unfortunately Coq has no linearity support, so this check needs to happen ad-hoc, by traversing processes. Ultimately, the claim is this: if the definition of a process typechecks in Coq, and the process uses channels linearly, then type safety and type preservation through reduction hold.

A specification language for automated testing of teletype IO programs (slides)

Oliver Westphal, University of Duisburg-Essen

 

Simple Noninterference by Normalization (slides)

Nachiappan Valliappan, Chalmers University

Information-flow control (IFC) languages ensure programs preserve the confidentiality of sensitive data. Noninterference, a key security property of programs written in such languages, is typically proved using dynamic or denotational semantics. In this talk, I’ll show that noninterference can also be proved by normalizing programs using static semantics. Unlike arbitrary terms, normal forms are well-principled and obey useful syntactic properties towards reasoning about program behavior—hence yielding a simple proof of noninterference.