Abstract: The goal of computer-aided cryptography is to develop tools that help the rigorous design and analysis of cryptographic constructions. Over the years, the focus of computer-aided cryptography has expanded from analysis of cryptographic protocols in the symbolic model to include new goals. Most notably, these goals include analyzing cryptographic primitives and protocols in the computational model, and reasoning about implementations. In this talk, I will illustrate how existing techniques from program verification and program synthesis can be used for achieving a number of goals in computer-aided cryptography.
Abstract: The equality reflection rule states that propositionally equal terms are judgmentally equal. It is generally frowned upon, as it makes type checking undecidable. Nevertheless, it would be useful to have a workable implementation of a type theory with equality reflection, for instance to tackle Voevodsky's Homotopy Type System. The difficulties created by equality reflection are numerous. It destroys the structural rules of exchange and strengthening, η-reductions cannot be performed without explicit typing annotations in the terms, and injectivity of type constructors becomes an unreasonable expectation. In the talk I shall discuss the design and implementation of a type theory with reflection which works around these complications, while still being a useful tool.
Abstract: Static type systems are meant to guarantee the absence of certain run-time errors. Quantum computing comes with new kinds of run-time errors, for example attempted violations of the no-cloning property of quantum mechanics. Therefore, quantum computing is potentially interesting from a type-theoretic point of view. In this talk, I will talk about the quantum lambda calculus, a strongly typed functional quantum programming language that has been around for about a decade, and Quipper, a more practical language that is currently implemented as a Haskell EDSL. I will outline some of the challenges involved in creating a type-safe version of Quipper.
Abstract: The starting point for this tutorial will be the Seely correspondence between (extensional) dependent type theory and locally cartesian closed categories, such as the category of sets. Under this correspondence, polynomial functors provide semantics for generic data types, and their initial algebras provide semantics for W-types (wellfounded trees). While trees in this approach are defined inductively, it is also possible to define trees combinatorially, directly as certain multivariate polynomial endofunctors. This leads to an alternative characterisation of initial algebras, namely as operations for the free monad on a polynomial endofunctor. The monad itself has important structure not seen at the level of initial algebras, namely the monad multiplication, which always encodes a notion of substitution. I will finish with some outlook regarding the role of polynomial monads (which are essentially operads) to encode and manipulate combinatorial and algebraic structures, and the need for groupoids and higher groupoids to really unleash the power of this formalism -- also in intensional type theory.
Abstract: HITs were introduced in 2011, following the Oberwolfach mini-workshop on HoTT, as a rather speculative array of new type-constructors, essentially generalising inductive definitions to give (homotopically) higher-dimensional types in the most simple-minded way possible.
Four years later, where do we stand on them? I will survey what we now know about them (or at least, as much of that as I know).
Well-understood: logical consequences. One aspect has worked out as well as anyone could have hoped: their logical consequences within the theory. As mostly developed during the IAS special year, the conjunction of HITs and uxnivalence allows the "synthetic" redevelopment of much of classical abstract homotopy theory within type theory.
Moderately understood: semantics. The semantics has taken longer to get to grips with, but a reasonable understanding is now emerging. The rough ideas are clear, but technicalities related to stability and coherence remain more troublesome than one might expect.
Mike Shulman and I have given models of a restricted range of HITs in a reasonable range of homotopy-theoretic settings (including simplicial sets), using local universes (Lumsdaine, Warren 2015) to obtain stability. On the other hand, Thierry Coquand and collaborators (Bezem, Cohen, Huber, Norsberg) have given models of a wider range of HITs in the cubical set model; and these models are strictly stable by construction, so that the added overhead of local universes is not required.
Little-understood: proof theory. The proof-theoretic aspects of HITs, however, are quite unsatisfactorily understood. Most obviously, we still have no fully general scheme of higher inductive definitions (in the sense of, say, the general inductive definitions of the Calculus of Inductive Constructions). Moreover, even for simple higher inductive types, when taken with judgemental computation rules, we do not understand the effects on proof-theoretic properties such as normalisation, confluence, decidability of typing.
Interesting progress on these issues has appeared recently in the cubical type theories of Altenkirch, Brunerie, Coquand, Licata, and others.