print · source · login   

Formalizations and Contributions by EUTYPES Members


The HoTT library is a formalization of homotopy type theory using proof assistant Coq. In it, there are many theorems from the HoTT book and it also has some results using higher inductive types. Link to formalization

The main publication:

  • The HoTT Library: A formalization of homotopy type theory in Coq, Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Mike Shulman, Matthieu Sozeau, Bas Spitters, 2016, arxiv, CPP2017

Publications by EUTYPES members related to parts of the library:

  • Formalising real numbers in homotopy type theory, Gaëtan Gilbert PDF, CPP2017 2017: 112-124
  • Modalities in homotopy type theory, Egbert Rijke, Michael Shulman, Bas Spitters LMCS
  • Synthetic topology in homotopy type theory for probabilistic programming, Florian Faissole, Bas Spitters, PDF

Publications by EUTYPES members building on top of the library (sources elsewhere):

  • Lawvere-Tierney sheafification in Homotopy Type Theory, Kevin Quirin PDF
  • Model structure on the universe in a two level type theory, Simon Boulier, Nicolas Tabareau CPP 2016
  • Finite Sets in Homotopy Type Theory, Dan Frumin, Herman Geuvers, Léon Gondelman, and Niels van der Weide CPP 2018.
  • A HoTT Quantum Equational Theory (Extended Version), J Paykin, S Zdancewic PDF 2019


Unimath is a formalization of mathematics in univalent foundations using the proof assistant Coq. Among others, it contains numerous results on (bi)category theory, K-theory, substitution systems, and induction schemes. Link to formalization

Some contributions by EUTYPES members:

Cubical Agda

Cubical Agda is a formalization of cubical type theory using the proof assistant Agda. it supports higher inductive types and definitional computation rules of the univalence axiom. Link to formalization

Maintainers: Anders Mörtberg (CMU and Stockholm University) and Andrea Vezzosi (IT University Copehagen)


ReLoC is a mechanized logic for interactively proving contextual refinements of programs in a language with higher-order state, fine-grained concurrency, polymorphism and existential and recursive types. It is build on top of the Iris framework in Coq.

Non-deterministic mini-C in Iris

This formalization provides a semantics of a subset of C that takes the C standard's unspecified evaluation order and undefined behavior due to sequence point violations into account. The formalization is build on top of the Iris framework in Coq and comes with a separation logic and verification condition generator (vcgen).


Iron is a higher-order concurrent separation logic that allows for precise reasoning about resources that are transferable among dynamically allocated threads. The formalization is build on top of the Iris framework in Coq.

Coq std++

Std++ is an extended "standard library" for Coq that provides extensive support for common data structures such as lists, finite maps, finite sets, and finite multisets. It is entirely dependency- and axiom-free, and uses type classes for overloading of notations and abstraction.

Translation from ETT to ITT

A translation from Extensional Type Theory to Intensional Type Theory in a constructive way. It comes with a proof-of-concept « plugin » to write extensional proofs in Coq to inhabit Coq types. Link to formalization

Authors: Matthieu Sozeau, Nicolas Tabarau, and Theo Winterhalter (INRIA)


Meta-programming in Coq. It contains in particular a specification of the proof-assistant with work-in-progress proofs of parts of the system and certification of its implementation. It also features a plugin to quote and reify actual Coq terms to and from the reflected syntax. Link to formalization


A formalisation of the Java Virtual Machine that contains the semantics description for all mnemonics of the Java bytecode. Link to web page

A Formalisation of SQL with Nulls

by Wilmer Ricciotti (University of Edinburgh) and James Cheney (University of Edinburgh and The Alan Turing Institute)

A mechanization of the semantics of SQL with set/bag operations, nested subqueries, and nulls, written in Coq. This formalization can be used to reason about the correctness of rewrite rules (widely applied in commercial databases to convert a user query into an equivalent one that can be executed more efficiently).

Link to formalization

Other formalizations by EUTYPES members