Jakob von Raumer
About me
- Interests:
- (Homotopy) Type Theory
- Topology
- Category Theory
- Formalisation of Mathematics
- Interactive Theorem Proving
Contact information
- Address: Room 025, Faculty of Informatics (Bldg. 50.34), Am Fasanengarten 5, 76131 Karlsruhe
- E-mail address: [first name]@[hyphenated last name].de
- Matrix: @javra:matrix.org
- GitHub
Publications, Talks, etc.
- A rewriting coherence theorem with applications in homotopy type theory
with Nicolai Kraus
Mathematical Structures in Computer Science 32 (MSCS), 2022
[PDF]
[ArXiv]
- String Diagrams for Strings and Rings
Ninth Symposium on Compositional Structures (SYCO), Como, Italy, 2022
[Slides]
- PhD Thesis: Higher Inductive Types, Inductive Families, and Inductive-Inductive Types
Supervisor: Thorsten Altenkirch
Examiners: Fredrik Nordvall-Forsberg and Venanzio Capretta
[PDF]
- Coherence via Wellfoundedness: Taming set-quotients in homotopy type theory
with Nicolai Kraus
35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Saarbrücken, Germany, 2020
[PDF]
[ArXiv]
[Slides]
[Video]
[Lean]
- A Syntax for Mutual Inductive Families
with Ambrus Kaposi
5th International Conference on Formal Structures for Computation and Deduction (FSCD), Paris, France, 2020
[PDF]
[Slides]
[Agda]
- An Induction Principle for Cycles
with Nicolai Kraus
26th International Conference on Types for Proofs and Programs (TYPES), Turin, Italy, 2020
[Abstract]
- Path Spaces of Higher Inductive Types in Homotopy Type Theory
with Nicolai Kraus
34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vancouver, Canada, 2019
[PDF]
[ArXiv]
[Slides]
[Lean]
- Constructing Inductive-Inductive Types via Type Erasure
with Thorsten Altenkirch, Ambrus Kaposi, and András Kovács
25th International Conference on Types for Proofs and Programs (TYPES), Oslo, Norway, 2019
[Abstract]
[Slides]
- Reducing Inductive-Inductive Types to Indexed Inductive Types
with Thorsten Altenkirch, Ambrus Kaposi, and András Kovács
24th International Conference on Types for Proofs and Programs (TYPES), Braga, Portugal, 2018
[Abstract]
[Slides]
- Homotopy Type Theory in Lean
with Floris van Doorn and Ulrik Buchholtz
International Conference on Interactive Theorem Proving (ITP), Brasília, Brazil, 2017
[PDF]
[ArXiv]
[Lean]
- Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover
5th International Congress on Mathematical Software (ICMS), Berlin, Germany, 2016
[Abstract]
[Slides]
[Lean]
- My Experience with the Lean Theorem Prover
22nd International Conference on Types for Proofs and Programs (TYPES), Novi Sad, Serbia, 2016
[Abstract]
- The Lean Theorem Prover (System Description)
with Leonardo de Moura, Soonho Kong, Jermy Avigad, and Floris van Doorn
25th International Conference on Automated Deduction (CADE), Berlin, Germany, 2015
[PDF]
- Master Thesis: Formalization of Non-Abelian Topology for Homotopy Type Theory
Supervisors: Prof. Jermy Avigad, Prof. Steve Awodey, Prof. Gregor Snelting
[PDF] [GitHub]
[Slides (German)]
- The Jordan-Hölder Theorem
Archive of Formal Proofs
[Proof outline]
[AFP]
- Secondary Sylow Theorems
Archive of Formal Proofs
[Proof outline]
[AFP]
- Bachelor Thesis: Visualization of Hyperbolic Tessellations
Supervisors: Tanja Hartmann, Martin Nöllenburg
[PDF (German)]
[Slides (German)]
[Slides (English)]
If any of the links are dead, send me a message.