Abstracts will be added as they are recieved. See full program.
More information will follow.
More about the speaker: Nick Benton, Software engineer, Facebook research
Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.
In this work, we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioral types, where the types are model checked for liveness and safety.
More about the speaker: Nobuko Yoshida, Imperial College London
I've been working on extending Haskell with types coming from linear logic. My goal in this talk is to share some of the motivations which led a company to get involved in a subject which may appear quite academic. This involves distributed programming, and optimisation vs control.
More about the speaker: Arnaud Spiwack, Senior Software Architect, tweag I/O
Type theories with equality reflection, such as extensional type theory (ETT), are convenient theories in which to formalise mathematics, as they allow to consider provably equal terms as convertible. Although type-checking is undecidable in this context, variants of ETT have been implemented, for example in NuPRL [3] and more recently in Andromeda [2]. The actual objects that can been checked are not proof-terms, but derivations of proof-terms. This suggest that any derivation of ETT can be translated as a typecheckable proof-term of intentional type theory (ITT). However, this result, investigated categorically by Hofmann [5] in 1995, and 10 years later more syntactically by Oury [6], has never given rise to an effective translation. In this talk, we present the first syntactical translation from ETT to ITT with uniqueness of identity proof and functional extensionality. This translation has been defined and proven correct in Coq [4] and gives rise to an executable plugin that translates a derivation in ETT into an actual Coq typing judgment.
Many constructions and theorems in the type theory literature are given just for some specific type theory, but understood heuristically to hold for all other similar theories. The lack of a language for rigorously stating results in such a general form has become a significant hindrance for some directions of research in the field.
I will present a definition of a reasonably wide class of dependent type theories — general enough to include Martin-Löf’s original intensional type theories, the logical framework, CoC, and book-HoTT, but structured enough for many important theorems and constructions to work off-the-shelf for all such theories. I will also present a formalisation of this definition in Coq, and (if time permits) sketch the proof of an initiality result for such theories.
More about the speaker: Peter Lumsdaine, Assistant professor at Stockholm university
We present the construction of universes in a simplicial type theory modeled in cubical spaces of which simplicial spaces arise as a sub-infinity-topos. These universes classify those types that are simplicial, category-, or groupoid-like. The approach is based on Riehl-Shulman's type theory for synthetic infinity-category theory, and Licata-Orton-Pitts-Spitter's work on internal universes in homotopy type theory. Joint work with Ulrik Buchholtz.
More about the speaker: Jonathan Weinberger, PhD student at Department of Mathematics, Technische Universität Darmstadt
Higher inductive types allow datatypes to be defined by not only regular constructors, but also by constructors for equalities between elements of the type. This enables the definition of a wide variety of interesting types with non-trivial equalities, including:
quotient types, truncations (squash types), and various types inspired from topology (spheres, tori...). Cubical type theories extend dependent type theory with various extensionality principles (functional and propositional extensionality, and more generally Voevodsky's univalence axiom) without losing canonicity so that these notions all have computational content. By extending cubical type theories with higher inductive types we can hence obtain systems that overcome many of the problems related to the intensional equality in traditional type theory without sacrificing the computational nature of type theory. Furthermore, the consistency of these extensions is justified by constructive semantics in various presheaf models generalizing Kan cubical sets. Inspired by these recent developments multiple implementations of proof assistants with native support for all of these features are being actively developed, including cubicaltt, a cubical version of Agda and the redtt system.
More about the speaker: Anders Mörtberg, Postdoc at the School of Computer Science at Carnegie Mellon University
We discuss a formalization of bicategory theory in HoTT. It includes several basic notions (bicategories, lax/pseudo/oplax functors, lax transformations, modifications, biadjunctions) and as an application, we construct a biadjoint biequivalence between 1-types and univalent groupoids. The full formalization can be found on: https://github.com/nmvdw/groupoids
I will present a mode theory (in the framework of Licata-Shulman-Riley) for building a modal type theory for reasoning about simplicial and cubical types, their interaction, and their respective opposite structures. The resulting type theory can be thought of as an improved version of the Riehl-Shulman type theory for synthetic infinity-category theory.
More about the speaker: Ulrik Buchholtz, Department of Mathematics, Technische Universität Darmstadt
In this talk, I will present the Jasmin language. Jasmin is a framework for developing high-speed and high-assurance cryptographic software. The framework is structured around the Jasmin programming language and its compiler. The language is designed for enhancing portability of programs and for simplifying verification tasks. The compiler is designed to achieve predictability and efficiency of the output code (currently limited to x64 platforms), and is formally verified in the Coq proof assistant. A benchmark of the Jasmin compiler on representative cryptographic routines concludes that the code generated by the compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework includes highly automated tools for proving memory safety and constant-time security (for protecting against cache-based timing attacks).
More about the speaker: Pierre-Yves Strub, Maître de conférences at École Polytechnique
The aim of this talk is to present an approach and several examples to the creation of systems relying on the recent advances in the study of type isomorphisms and automorphisms. The power of type isomorphisms and automorphisms is illustrated by the fact that they have a fairly simple computational structure closed under composition behind them (finite hereditary permutations) and the groups of automorphisms of higher order types can represent arbitrary finite groups. The former property allows us to efficiently compute answers to several common problems up to isomorphism, while exploiting the latter property allows us to encode many conventional cryptographic primitives directly in Type Theory. Among other examples we consider automated theorem proving and typed library search up to isomorphism, and an instance of ElGamal cryptosystem based on type automorphisms. One side invertible transformations (retractions) and their possible use are discussed as well.
More about the speaker: Sergei Soloviev, Institut de Recherche en Informatique de Toulouse (IRIT)
mathlib, Lean's mathematical library, is a library focusing on mathematics, including theories on algebra, topology, measure theory, lattice theory, and category theory. Its goal is to provide the mathematical foundations for modern mathematics and computer science. Mathlib's measure and probability theory is currently just starting, with basics like probability mass functions and the Lebesgue measure. In this talk, I will give an overview of its content, current development and future projects. I also want to present some construction principles we employ to generalise the construction of spaces. Download slides.
More about the speaker: Johannes Hölzl, Postdoc at Vrije Universiteit Amsterdam
Inspired by the proof approached used in miTLS[1], a cryptographically verified implementation of TLS, Brzuska, Delignat-Lavaud, Fournet, Kohlweiss and myself introduced a new proof methodology for composed protocols[2]. This methodology relies on "code equivalence" to relate composed security assumptions to a higher-level security notion. We use F*, a powerful, dependently-typed programming language jointly developed by Microsoft Research and INRIA, Paris as a proof assistant and to instantiate the aforementioned proof methodology. As a result, we can conduct security proofs for composed protocols more easily and get a fully verified implementation of the specific protocol (almost) for free.
[1] Implementing and Proving the TLS 1.3 Record Layer Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Jianyang Pan; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin; Jean Karim Zinzindohoué. ePrint: https://eprint.iacr.org/2016/1178
[2] State Separation for Code-Based Game-Playing Proofs Chris Brzuska; Antoine Délignat-Lavaud; Cédric Fournet; Konrad Kohbrok; Markulf Kohlweiss. Preprint: https://eprint.iacr.org/2018/306
More about the speaker: Konrad Kohbrok, Aalto University, Finland
All existing concurrent separation logics for programming languages with dynamically allocated threads (fork-style concurrency) are affine, which means that resources can be leaked during proofs. Hence it is not possible to reason precisely about memory usage. In this talk I will show how to reason about precise resource management in an affine separation logic, with only a modicum of additional bookkeeping. Our approach enables for the first time to reason precisely about resources in a language with fork-style concurrency in a very expressive higher-order concurrent separation logic. As a simple example, we can verify that a program which delegates memory reclamation to a dynamically allocated background thread does not leak memory. Download slides.
More about the speaker: Aleš Bizjak, Postdoc at Department of Computer Science, Aarhus University
In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based on type theory, such as Coq and Agda. Currently, programming and reasoning about coinductive types is difficult for two reasons: The need for recursive definitions to be productive, and the lack of coincidence of the built-in identity types and the important notion of bisimilarity. Guarded recursion in the sense of Nakano has recently been suggested as a possible approach for dealing with the problem of productivity, allowing this to be encoded in types. Indeed, coinductive types can be encoded using a combination of guarded recursion and universal quantification over clocks. This talk studies the notion of bisimilarity for guarded recursive types in Ticked Cubical Type Theory, an extension of Cubical Type Theory with guarded recursion. As a worked example we study a guarded notion of labelled transition systems, and show that path equality coincides with an adaptation of the usual notion of bisimulation for processes. In particular, this implies that guarded recursion can be used to give simple equational reasoning proofs of bisimilarity. If I have time I will also describe a general result stating that, for any functor, an abstract, category theoretic notion of bisimilarity for the final guarded coalgebra is equivalent (in the sense of homotopy type theory) to path equality (the primitive notion of equality in cubical type theory). This work should be seen as a step towards obtaining bisimilarity as path equality for coinductive types using the encodings mentioned above.
More about the speaker: Niccolò Veltri, Postdoc at IT University of Copenhagen
A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making separation-logic proofs look and feel like ordinary Coq proofs.However, IPM is tied to a particular separation logic (namely, Iris), thus limiting its applicability.
In this talk, I will describe MoSeL, a general and extensible Coq framework that brings the benefits of IPM to a much larger class of separation logics. Unlike IPM, MoSeL is applicable to both affine and linear separation logics (and combinations thereof), and provides generic tactics that can be easily extended to account for the bespoke connectives of the logics with which it is instantiated. To demonstrate the effectiveness of MoSeL, we have instantiated it to provide effective tactical support for interactive and semi-automated proofs in six very different separation logics.
MoSeL is joint work with Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer.
More about the speaker: Robbert Krebbers, Assistant professor at Delft University of technology
The go-to use-case to demonstrate the utility of dependent-types is type-safe-by-construction interpreters of simply typed expression languages and lambda calculi. Indeed it is a pearl: it is a definition of a language's semantics that is clean, operational and intrinsically type safe. But can we take the idea of defining language semantics for languages using intrinsically typed definitional interpreters serious and scale to common language features? One such feature is imperative state, for which it was unclear how to interpret it in an intrinsically type-safe manner. We build a state monad with a typed heap and propose to use monadic strength to program with such a monad and the strong invariants that it carries in an existing dependently typed language like Agda. Using this monad to interpret ML-style references, we make the case that typed definitional interpreters should be taken serious as an approach for defining dynamic semantics of *real-world programming languages*.
This talk is mostly about work contained in (Intrinsically-typed definitional interpreters for imperative languages, C. Bach Poulsen et al, POPL'18)[https://doi.org/10.1145/3158104].
More about the speaker: Arjen Rouvoet, PhD student at TU Delft
More information will follow.
More about the speaker: Thorsten Altenkirch, Professor at University of Nottingham
