Homotopy Type Theory and Computing – Classical and Quantum

Speakers and Abstracts

• Thorsten Altenkirch | University of Nottingham

  Title: Univalence Without an Interval
  

  Abstract: We are developing a new formulation of univalent type theory (known as HoTT) which doesn't use an interval type. The first step is to formulate a type theory with internal parametricity which can be modelled using BCH cubes - see our POPL paper [1]. As a next step we identify a fibrant universe using a higher coinductive type.

  This is joint work with Yorgo Chamoun, Ambrus Kaposi and Mike Shulmann

  [1] Altenkirch, T., Chamoun, Y., Kaposi, A., & Shulman, M. (2024). Internal parametricity, without an interval. Proceedings of the ACM on Programming Languages, 8(POPL), 2340-2369.

• Carlo Angiuli | Indiana University *

  Title: Normalization: Running Open Terms
  

  Abstract: This talk will survey the normalization problem for type theory, in anticipation of upcoming talks at this conference by Shulman and Kovács. I will attempt to define normalization in general, before focusing on the simply-typed lambda calculus, its (beta-eta) normal forms, and normalization by evaluation. I will also discuss dependent types, the relationship between computation and normalization, and a forthcoming expository resource.

  
  * Note: This talk will be presented virtually.

• Ulrik Buchholtz | University of Nottingham

  Title: Primitive Recursive (Homotopy) Type Theory
  

  Abstract: I'll present a subsystem of Martin-Löf type theory where all functions from Nat to Nat are primitive recursive. The soundness proof involves a gluing construction for a sheaf topos model constructed from a site of primitive recursive functions. Then I'll use this as a starting point for some speculations about geometric type theory and its computational aspects. This is based on joint work with Johannes Schipp von Branitz.

• Eric Finster | University of Birmingham

  Title: A Tour of Parameterized Spectra
  

  Abstract: This talk will be a survey of some of the defining characteristics of the infinity-topos of parameterized spectra. I will try to describe both "external" properties, such as what this topos classifies as a higher geometric theory, as well as "internal" properties, that is, the various additional axioms satisfied by its internal logic. Where possible, I will try to explain how to express well-known constructions from homotopy in the internal language of this topos.

• Daniel Gratzer | Aarhus University

  Title: Towards a Category of Spaces in Simplicial Type Theory
  

  Abstract: Simplicial type theory as introduced by Riehl and Shulman and developed by Buchholtz, Martı́nez, Weinberger, and others enables a type-theoretic synthetic study of ∞-categories. A major absence from the existing results in simplicial type theory is the absence of basic "generating" ∞-categories e.g., the ∞-categories of groupoids. We present a work-in-progress construction of a type satisfying the properties expected of the ∞-category of ∞-groupoids or, equivalently, the universal left fibration. We draw on existing work by Weaver and Licata to construct a universe of ∞-groupoids within an extension of multimodal HoTT/homotopy MTT tooled for synthetic cubical spaces and argue that it lies within the subcategory of (synthetic) simplicial spaces and satisfies the expected properties (Segalness, Rezkness, directed univalence) and is closed under the expected connectives.

• András Kovács | Gothenburg University

  Title: Optimizing Evaluation for Cubical Type Theories
  

  Abstract: There are numerous interesting computations in cubical type theory, mostly in relation to synthetic homotopy theory, which are too expensive to perform in existing systems. One way to try to address this is to optimize the involved definitions. Another way, that I focus on in this talk, is to improve evaluation for the theory itself. I present a recent implementation of a CTT with major performance improvements. Broadly speaking, the benefits stem from a) systematically omitting unnecessary computation b) exploiting the canonicity property of the CTT when computation depends on interval variables but not free variables with fibrant types.

• Thomas Lamiaux | ENS Paris-Saclay

  Title: Computing Cohomology Rings in Cubical Agda
  

  Abstract: In this talk, we will discuss the formalization of Cohomology Rings in Cubical Agda, and how we computed a few basic examples. We will particularly focus on : 1. How the choice of a data type representation influence formalisation, in our case for representing polynomials and cohomology rings 2. How suitable representations can be used to compute cohomology rings 3. Where computation would be helpful, how it is limited in practice, and how we can still recover some computation to help us with our proof

• Dongho Lee | Dalhousie University

  Title: A Concrete Categorical Semantics for Proto-Quipper Language and Dynamic Lifting
  

  Abstract: In this talk, we discuss a concrete categorical semantics of Proto-Quipper-L, a quantum circuit description language with dynamic lifting. The language is an extension of linear lambda-calculus with quantum channel constants (which represent tree structure of gates) and circuit operations (which are box and unbox) where terms can have tree shapes. The type system roughly comes from the multiplicative intuitionistic linear logic where the term represents the proof. The categorical semantics of the language is built upon the linear and non-linear model for linear logic by Benton and coproduct completion as the categorical semantics of Proto-Quipper-M by Rios and Selinger while we give a concrete categorical model for diagrams based on graphical calculus. For the computational effect of dynamic lifting we introduce branching monad and give an interpretation of terms in the Kleisli category.

• Axel Ljungström | Stockholm University

  Title: More cellular (co)homology in HoTT
  

  Abstract: In this talk, I'll present some ongoing work with Anders Mörtberg and Loïc Pujet on the development and computer formalisation of cellular homology and cohomology. Cellular cohomology was first studied in HoTT by Buchholtz and Favonia who constructed cellular cohomology groups and showed that these define a cohomology theory. This was done by proving their construction equivalent to the usual construction of cohomology groups via Eilenberg-MacLane spaces. I will present an alternative approach to cellular (co)homology (à la Buchholtz & Favonia) using a more traditional framework building on the theory of cellular approximations. One benefit of this approach is that it works uniformly for homology and cohomology. In particular, I will show you some versions of cellular approximation theorems we can prove constructively in HoTT and discuss how these can be used to get functorial cohomology and homology theories. Another benefit of the approach by cellular approximation is that it makes the definition of the cup product on cellular cohomology rather direct. If time permits, I will discuss also this construction and whether it can aid in cohomology computations, both in the mathematical sense and in the sense of normalisation in constructive proof assistants like Cubical Agda.

• David Jaz Myers | NYU AD

  Title: Topological Quantum Gates in Homotopy Type Theory
  

  Abstract: Despite the evident necessity of topological protection for realizing scalable quantum computers, the conceptual underpinnings of topological quantum logic gates had arguably remained shaky. Building on recent results on defect branes in string/M-theory and on their holographically dual anyonic defects in condensed matter theory, here we explain how the specification of realistic topological quantum gates, operating by anyon defect braiding in topologically ordered quantum materials, has a surprisingly slick formulation in parameterized point-set topology, which is so fundamental that it lends itself to certification in modern homotopically typed programming languages such as cubical Agda. We propose that this remarkable confluence of concepts may jointly kickstart the development of topological quantum programming proper by providing a powerful paradigm for simulating and verifying topological quantum computing architectures with high-level certification languages aware of the actual physical principles of realistic topological quantum hardware.

   In this talk, we will present the description of these topological quantum gates in homotopy type theory and describe the use of cubical type theory as a certification language for topological quantum computing. We will focus on the definition of the configuration spaces in cubical type theory, which play a crucial role in the construction of the space of conformal blocks as a twisted cohomology group.

• Anders Mörtberg | Stockholm University

  Title: Computational Proofs in Synthetic Homotopy Theory
  

  Abstract: Cubical type theories provide computational meaning to HoTT, making it possible to simplify proofs in synthetic homotopy theory and sometimes even reducing whole arguments purely to computer computations. A classic example is the Brunerie number which we recently managed to simplify so that it becomes computable in just a few seconds in Cubical Agda. I will discuss this and other similar proofs by computation that we have done. I will also discuss various examples of things that we have not managed to compute and work in progress into making Cubical Agda able to compute more things for us.

• Jennifer Paykin | Intel Corporation

  Title: Symplectic Types for a Clifford Lambda Calculus
  

  Abstract: Can quantum programming languages move beyond gate-based programming? In this talk I will present work in progress where quantum algorithms (specifically, Clifford unitaries over qudits) are expressed as functions on compact Pauli encodings. Inspired by the fact that projective Cliffords correspond to center-fixing automorphisms on the Pauli group, we develop a type system where well-typed expressions correspond to symplectic morphisms---that is, linear transformations that respect the symplectic form. This language is backed up by a robust categorical and operational semantics, and well-typed functions can be efficiently simulated and synthesized into circuits. The resulting linear type system and semantics is a promising candidate for synthetic mathematical reasoning using linear HoTT.

• Robert Rand | University of Chicago *
  Title: Verifying the ZX-calculus and its Friends
  

   

  Abstract: We seek to verify the ZX-calculus, a powerful tool for representing and reasoning about quantum computation. ZX-diagrams are typically represented as adjacency-based graphs, reflecting the guiding principle that “only connectivity matters”. In the context of formal theorem provers like Coq, however, such graphs are difficult to reason about, especially when we seek to give them semantics. To address this gap, we introduce VyZX, a verified library for reasoning about the ZX-calculus, using inductive constructs that arise naturally from category theoretic definitions. We extend VyZX to reason about a variety of monoidal categories, provided they satisfy an appropriate set of coherence conditions.
  
  * Note: This talk will be presented virtually.

• Mitchell Riley | NYU AD

  First Talk
  
  Title: Tiny Objects in Type Theory
  

  Abstract: I will present an extension of Martin-Löf Type Theory that contains a
  tiny object; a type for which there is a right adjoint to the
  formation of function types as well as the expected left adjoint. I
  will suggest a couple of potential applications and sketch a
  normalisation algorithm.
  
  
  Second Talk
  
  Title: Linear HoTT and Quipper
  

  Abstract: HoTT is an extension of HoTT with linear type formers. Like the
  Proto-Quipper family of languages, Linear HoTT can be used to specify
  (linear) quantum circuits parameterised by (non-linear) classical
  data. Because we have all of ordinary Martin-Löf Type Theory at our
  disposal, there is the prospect of formally verifying properties of
  our quantum programs in the same language that they are specified. In
  this talk I will give a new, simpler set of rules for Linear HoTT and
  sketch a translation of Quipper into this system.

• Urs Schreiber | NYU AD

  Title: Towards Quantum Programming via Linear Homotopy Types
  

  Abstract: Remarkably, among the infinity-toposes into which HoTT interprets are “tangent infinity-toposes” of parameterized module spectra, which behave like semantics for an enhancement of HoTT by dependent *linear* homotopy types, neatly combining the linear aspect of typed quantum programming languages (like Proto-Quipper) with homotopy-theoretic aspects needed for future *topological quantum* languages. I will survey this LHoTT-perspective on quantum systems, developed jointly with Hisham Sati (“Topological Quantum Gates in HoTT” arXiv:2303.02382, “Entanglement of Sections” arXiv:2309.07245, “The Quantum Monadology” arXiv:2310.15735, “Quantum and Reality” arXiv:2311.11035).

• Michael Shulman | University of San Diego *

  Title: Towards an Implementation of Higher Observational Type Theory
  

  Abstract: Higher Observational Type Theory is a third style of Homotopy Type Theory, contrasting with Book HoTT and Cubical Type Theory. It is characterized by a definition of identity types by recursion on the base type: the identity type of a product type is defined to be a product of identity types, and so on. Extensionality principles like funext, univalence, and bisimulation then hold essentially by definition, rather than only up to equivalence. Like Cubical Type Theory, Higher Observational Type Theory can be built by defining a fibrancy predicate in a non-univalent substrate theory, which in this case is a form of internally parametric type theory. Altenkirch's talk describes a canonicity proof for this substrate; I will sketch a normalization algorithm for it (sans proof), and then demonstrate a prototype implementation of this algorithm. This is joint work in progress with Altenkirch, Kaposi, and Uskuplu.
  
  * Note: This talk will be presented virtually.

• Jonathan Sterling | University of Cambridge

  Title: Baby steps in higher domain theory
  

  Abstract: I present some preliminary results obtained with Leoni Pugh concerning partial map classifiers in higher domain theory, realised in a version of Riehl and Shulman’s simplicial type theory extended by Phoa’s principle for the simplicial interval.

• David Wärn | University of Gothenburg

  Title: The zigzag construction
  

  Abstract: The zigzag construction gives a more or less explicit sequential colimit description for certain pullbacks of pushouts of spaces. It generalises the fact that the free groupoid on a bipartite graph can be understood in terms of zigzags of edges modulo backtracking. It remains to be understood to what extent this description can be used for computations. This requires understanding what happens in each step of the construction. In this talk, I will present the construction with a view toward generalisations and applications.