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
• XMPP: javra@jabber.ccc.de
• GitHub | Bitbucket

Publications, Talks, etc.

• 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
  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)]