Nicolas Pouillard

In this presentation I will present the experimental language Ling. We shall get an intuitive understanding of the language through familiar concepts from imperative programming. We shall cover how Ling enables a modular and precise control on memory allocation, through a general optimization called fusion. This optimization, fusion is a cost-free abstraction mechanism which brings high level programming to system programming.

The design of Ling is the result of my researches in collaboration with Daniel Gustafsson and Nicolas Guenot at the IT-University of Copenhagen and also from the language Limestone by Jean-Philippe Bernardy and Víctor López Juan at the University of Chalmers. These two lines of research stand upon the longstanding research topics of process calculi (such as the π-calculus), term calculi (such as λ-calculus), Linear Logic, and dependent Type Theory (such as used in Coq and Agda to write proofs and programs). The research on the λ-calculus and Type Theory gave rise to a powerful family of languages including but not limited to: Haskell, OCaml, Coq, Idris, and Agda. The research on the π-calculus gave rise to a vast family of calculi for concurrency. However type systems for these languages took much longer to emerge and progress. For instance the main concurrent programming language in use today is still dynamically typed. This is changing as we understand better how to the use the formulae of Linear Logic as behavior types (or session types) for concurrent processes. Still the aim of this experimental language is to program systems precisely and modularly. The need for precision comes from the resource constraints such as memory, file handles and the need for modularity comes the desire to reduce programming mistakes by solving problems at the right abstraction level. Functional programming offers a pretty good framework for modularity. This modularity comes at a cost which is rather difficult to predict. One the one hand optimizing compilers can fuse function composition to eliminate the need for intermediate data-structures. One the other hand when such an optimization fails to trigger the resulting program might poorly perform. The system of Ling controls when fusion can happen. Therefore one knows statically when fusion occurs and when intermediate buffers are needed. Today concurrent systems are built out of shared memory. However, the shared memory model is a nightmare for programmers. Here the approach is reversed we start from a concurrent programming language and apply it also for shared memory. At first the goal is not necessarily to target a parallel architecture but to program at level of abstraction where the programmer knows precisely the resources needed and the compiler still has plenty of opportunity to re-order and parallelize safely some instructions. This talk is intended at an audience familiar with imperative programming. Using the language should not require to understand anything about Linear Logic even though it is used fundamentally. Finally this presentation is an open call for comments and contributions to the open development of the language and infrastructure.

Software engineering is in a unsustainable state: software is mainly developed in a trial and error fashion, which always leads to vulnerable systems. Several decades ago the correspondence between logics and programming (Curry-Howard) was found. This correspondence is now being used in modern programming languages using dependent types, such as Agda, Coq, and Idris. In this talk I show our development of attacks and security notions within Agda, using the recent BREACH exploit as an example. Our development is a constructive step towards verified software and bridges a gap between theory and practice. I will explain the details about the Curry-Howard correspondence. The target audience are interested people with some programming experience.

Using the recent BREACH exploit as an example, I will present how to represent attacks and security notions within the Type Theory of Agda.

Using security notions such as semantic security (IND-CPA, IND-CCA), it is intuitive to show how the use of compression leads to a not semantically secure encryption, and thus potential issues. Indeed the length of the ciphertext can now be controlled by the adversary who can control the plaintext. I will show how this intuitive result can be formalized using Agda.

A note on Agda: It is both a programming language and a proof system. The programming language features pure, exhaustive, and terminating functions over rich user defined data types (inductive and co-inductive). This powerful λ-calculus is equipped with a rich type-system featuring dependent-types. Through the Curry-Howard correspondence this programming language can also be used as a proof system. With such a combined system it becomes possible to write programs and proofs about these programs in a unified way. Additionally using this approach, one can start proving properties starting only with programming skills and gradually learn more proof techniques by exploring the type system.

I claim that functional programming and dependent types can be of a great help to formalize cryptography and thus privacy enhancing tools. I will present how functions are convenient at describing these games and adversaries. I will also give an overview of the crypto-agda project: how type-isomorphisms can ease probabilistic reasoning; how circuits can help capturing the requirements on the complexity bounds; and how all of these aspects can fit together thanks to polymorphism!