Jakob von Raumer

About me

• Ph.D. student
• Supervisor: Thorsten Altenkirch
• Interests: Homotopy Type Theory, Topology, Category Theory, Formalization of Mathematics, Interactive Theorem Proving

Contact information

• Address: Office A04, School of Computer Science, Wollaton Rd, Nottingham, NG8 1BB
• E-mail address: [first name]@[hyphenated last name].de
• Jabber: javra@jabber.ccc.de
• GitHub | Bitbucket

Publications, Talks, etc.

• A Syntax for Mutual Inductive Families
  with Ambrus Kaposi
  [PDF]
• Path Spaces of Higher Inductive Types in Homotopy Type Theory
  with Nicolai Kraus
  Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vancouver, Canada, 2019
  [PDF] [ArXiv]
• 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]
• Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover
  The 5th International Congress on Mathematical Software (ICMS), Berlin, Germany, 2016
  [Abstract] [Slides]
• 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
  International Conference on Automated Deduction (CADE-25), 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)]