Abstract
A lens is an optical device which refracts light. Properly adjusted, it can be used to project sharp images of objects onto a screen— a principle underlying photography as well as human vision. Striving for clarity, we shift our focus to lenses as abstractions for bidirectional programming. By means of standard mathematical terminology as well as intuitive properties of bidirectional programs, we observe different ways to characterize lenses and show exactly how their laws interact. Like proper adjustment of optical lenses is essential for taking clear pictures, proper organization of lens laws is essential for forming a clear picture of different lens classes. Incidentally, the process of understanding bidirectional lenses clearly is quite similar to the process of taking a good picture. By showing that it is exactly the backward computation which defines lenses of a certain standard class, we provide an unusual perspective, as contemporary research tends to focus on the forward computation. © Springer International Publishing Switzerland 2015

Abstract
Our department has long been an advocate of the functional-first school of programming and has been teaching Haskell as a first language in introductory programming course units for 20 years. Although the functional style is largely beneficial, it needs to be taught in an enthusiastic and captivating way to fight the unusually high computer science drop-out rates and appeal to a heterogeneous population of students. This paper reports our experience of restructuring, over the last 5 years, an introductory laboratory course unit that trains hands-on functional programming concepts and good software development practices. We have been using game programming to keep students motivated, and following a methodology that hinges on test-driven development and continuous bidirectional feedback. We summarise successes and missteps, and how we have learned from our experience to arrive at a model for comprehensive and interactive functional game programming assignments and a general functionally-powered automated assessment platform, that together provide a more engaging learning experience for students. In our experience, we have been able to teach increasingly more advanced functional programming concepts while improving student engagement.

Abstract
A bidirectional transformation consists of pairs of transformations-a forward transformation get produces a target view from a source, while a putback transformation put puts back modifications on the view to the source-satisfying sensible roundtrip properties. Existing bidirectional approaches are get-based in that one writes (an artifact resembling) a forward transformation and a corresponding backward transformation can be automatically derived. However, the unavoidable ambiguity that stems from the underspecification of put often leads to unpredictable bidirectional behavior, making it hard to solve nontrivial practical synchronization problems with existing bidirectional transformation approaches. Theoretically, this ambiguity problem could be solved by writing put directly and deriving get, but differently from programming with get it is easy to write invalid put functions. An open challenge is how to check whether the definition of a putback transformation is valid, while guaranteeing that the corresponding unique get exists. In this paper, we propose, as far as we are aware, the first safe language for supporting putback-based bidirectional programming. The key to our approach is a simple but powerful language for describing primitive putback transformations. We show that validity of putback transformations in this language is decidable and can be automatically checked. A particularly elegant and strong aspect of our design is that we can simply reuse and apply standard results for treeless functions and tree transducers in the specification of our checking algorithms. © 2014 Springer International Publishing Switzerland.

Abstract
Different XML formats are widely used for data exchange and processing, being often necessary to mutually convert between them. Standard XML transformation languages, like XSLT or XQuery, are unsatisfactory for this purpose since they require writing a separate transformation for each direction. Existing bidirec- tional transformation languages mean to cover this gap, by allowing programmers to write a single program that denotes both transformations. However, they often 1) induce a more cumbersome programming style than their traditionally unidirectional relatives, to establish the link between source and target formats, and 2) offer limited configurability, by making implicit assumptions about how modifications to both formats should be translated that may not be easy to predict. This paper proposes a bidirectional XML update language called BiFluX (BIdirectional FunctionaL Updates for XML), inspired by the Flux XML update language. Our language adopts a novel bidirectional programming by update paradigm, where a program succinctly and precisely describes how to update a source document with a target document in an intuitive way, such that there is a unique "inverse" source query for each update program. BiFluX extends Flux with bidirectional actions that describe the con- nection between source and target formats. We introduce a core BiFluX language, and translate it into a formally verified bidirectional update language BiGUL to guarantee a BiFluX program is well-behaved.

Abstract
MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protocols, and secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified executable implementations. The first uses a fully automated extraction from EasyCrypt to OCaml. The second reduces the trusted computing base (TCB) and provides better performance by combining code extraction with formally verified manual low-level components implemented in the Jasmin language. We conclude with a discussion of the trade-off between the formal verification effort and the performance of resulting executables, and how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH.

Abstract
Secure multiparty computation (SMC) allows for complex computations over encrypted data. Privacy concerns for cloud applications makes this a highly desired technology and recent performance improvements show that it is practical. To make SMC accessible to non-experts and empower its use in varied applications, many domain-specific compilers are being proposed.We review the role of these compilers and provide a formal treatment of the core steps that they perform to bridge the abstraction gap between high-level ideal specifications and efficient SMC protocols. Our abstract framework bridges this secure compilation problem across two dimensions: 1) language-based source- to target-level semantic and efficiency gaps, and 2) cryptographic ideal- to real-world security gaps. We link the former to the setting of certified compilation, paving the way to leverage long-run efforts such as CompCert in future SMC compilers. Security is framed in the standard cryptographic sense. Our results are supported by a machine-checked formalisation carried out in EasyCrypt.