Cedric Fournet
Title: Building verified cryptographic components using F*
Abstract: The HTTPS ecosystem includes communications protocols such as TLS and QUIC, the X.509 public key infrastructure, and various supporting cryptographic algorithms and constructions. This ecosystem remains surprisingly brittle, with practical attacks and patches many times a year. To improve their security, we are developing high-performance, standards-compliant, formally verified implementation of these components. We aim for our verified components to be drop-in replacements suitable for use in mainstream web browsers, servers, and other popular tools. In this talk, I will give an overview of our approach and our results so far. I will present our verification toolchain, based on F*: a programming language with dependent types, programmable monadic effects, support for both SMT-based and interactive proofs, and extraction to C and assembly code. I will illustrate its application using security examples, ranging from the functional correctness of optimized implementations of cryptographic algorithms to the security of (fragments of) the new TLS 1.3 Internet Standard.
See https://fstar-lang.org/ for an online tutorial and research papers on F*, and https://project-everest.github.io/ for its security applications to cryptographic libraries, TLS, and QUIC.
Delia Kesner
Title: Multi Types for Higher-Order Languages
Abstract: Quantitative techniques are emerging in different areas of computer
science, such as model checking, logic, and automata theory, to face the
challenge of today’s resource aware computation.
In this talk we discuss multi types, a.k.a. non-idempotent
(intersection) types, which provide a natural tool to reason about
resource consumption. Multi types are applicable to a wide range of
powerful models of computation, such as for example pattern matching,
control operators and infinitary computations.
We provide a clean theoretical understanding of the use of resources,
and survey some recent semantical and operational results in the
domain.
Josef Urban
Title: Machine Learning for Proof Automation and Formalization
Abstract: I will discuss several ways of using machine learning to automate theorem proving and to help with automating formalization. The former includes learning to choose relevant facts for “hammer” systems, guiding the proof search of tableaux and superposition automated provers by learning from large ITP libraries, and guiding the application of tactics in interactive tactical systems. The latter includes learning probabilistic grammars from aligned informal/formal corpora and combining them with semantic pruning, and using recurrent neural networks to learn direct translation from Latex to formal mathematics. Finally, I will discuss systems that interleave learning and deduction in feedback loops, and mention some latest developments in these areas.
Matthieu Sozeau
Title: The Predicative, Polymorphic Calculus of Cumulative Inductive Constructions and its implementation
Abstract: In this presentation, I will give an overview of an extension of the
Predicative Calculus of Inductive Constructions with polymorphic
universes and cumulative inductive types, at the basis of Coq since
version 8.7. Polymorphic universes with cumulativity allow the
definition of constructions that are generic in their universes and
constraints between them, while keeping at the source level the
lightweight syntax of systems based on typical ambiguity.
Cumulative inductive types extend this further to allow for very
liberal (and somewhat surprising) type and term conversions that
subsume the so-called template polymorphism feature of Coq.
We will focus in particular on the set-theoretic model of the calculus
that justifies our treatment of cumulativity, and on the combined
subtleties of universe polymorphism and Coq’s higher-order unification
algorithm. We will showcase the implementation through striking examples
where universe polymorphism and cumulative inductive types are crucial:
to express syntactical models of cumulative type theories and to
faithfully follow informal mathematical practice while formalizing
category theory.
This is joint work with Nicolas Tabareau, Amin Timany and Beta Ziliani.