Name: Ralph Matthes
Type: User
Company: IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3
Bio: until 2005 at LMU München (Germany) first as mathematician then as computer scientist, since then researcher in computer science at CNRS (France)
Location: Toulouse, France
Blog: https://www.irit.fr/~Ralph.Matthes/
Ralph Matthes's Projects
Breadth-first traversal following a proposal of Martin Hofmann (1993-1995)
Coinductive Representation of Graphs - Code for Celia Picard's PhD thesis
Homotopy type theory
Large category of modules over monads on top of UniMaths and Display category
Archive for all Coq related OPAM packages organized in various repositories
Multi platform setup for Coq, Coq libraries and tools
Skew monoidal categories in UniMath with structural strengths
The mathematical study of type theories, in univalent foundations
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Various websites