Dr. Jakob von Raumer

	Kontakt Tel.: +49 721 608-47401 Email: Loading...	IPD Prof. Snelting Raum 022, Gebäude 50.34 Am Fasanengarten 5 76131 Karlsruhe Deutschland
	Sprechzeiten: Montag & Dienstag

Arbeitsgebiete

Interaktive Theorembeweiser, Typentheorie, Kategorientheorie, Homotopietypentheorie

Lehre

• Vorlesung: Programmierparadigmen , Wintersemester 2023/2024
• Übung: Programmierparadigmen - Übungen , Wintersemester 2023/2024
• Vorlesung: Programmierparadigmen , Wintersemester 2022/2023
• Übung: Programmierparadigmen - Übungen , Wintersemester 2022/2023, Beste Übung
• Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2022
• Vorlesung: Programmierparadigmen , Wintersemester 2021/2022
• Übung: Programmierparadigmen - Übungen , Wintersemester 2021/2022, Beste Übung
• Praktikum: Theorembeweiserpraktikum: Anwendungen in der Sprachtechnologie , Sommersemester 2021
• Praktikum: PSE: Visualisierung von Typinferenz , Wintersemester 2020/2021

Veröffentlichungen

2020

• Higher Inductive Types, Inductive Families, and Inductive-Inductive Types
  February 2020 : J. v. Raumer
• A Syntax for Mutual Inductive Families
  5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference) 2020, pp. 23:1--23:21 : A. Kaposi, J. v. Raumer
• Coherence via Well-Foundedness: Taming Set-Quotients in Homotopy Type Theory
  LICS '20: 35th Annual {ACM/IEEE} Symposium on Logic in Computer Science, Saarbr{\"U}cken, Germany, July 8-11, 2020 2020, pp. 662--675 : N. Kraus, J. v. Raumer

2019

• Path Spaces of Higher Inductive Types in Homotopy Type Theory
  34th Annual {ACM/IEEE} Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019 2019, pp. 1--13 : N. Kraus, J. v. Raumer

2017

• Homotopy Type Theory in Lean
  Interactive Theorem Proving - 8th International Conference, ITP 2017, Bras{\'{\i}}lia, Brazil, September 26-29, 2017, Proceedings 2017, pp. 479--495 : F. v. Doorn, J. v. Raumer, U. Buchholtz

2016

• Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover
  Mathematical Software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings 2016, pp. 28--33 : J. v. Raumer

2015

• The Lean Theorem Prover (System Description)
  Automated Deduction - {CADE-25} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 2015, pp. 378--388 : L. M. d. Moura, S. Kong, J. Avigad, F. v. Doorn, J. v. Raumer

Betreute Studien- und Abschlussarbeiten

offen

• String Diagrams für Lean 4, Masterarbeit

laufend

• Hammer für Lean 4 unter Benutzung von SMT-Solvern für HOL, Praxis der Forschung
• Interaktives Term-Rewriting für Lean 4, Bachelor-/Masterarbeit