Follow
Jakob von Raumer
Jakob von Raumer
Karlsruhe Institute of Technology
Verified email at von-raumer.de - Homepage
Title
Cited by
Cited by
Year
The Lean theorem prover (system description)
L Moura, S Kong, J Avigad, F Doorn, J Raumer
International Conference on Automated Deduction, 378-388, 2015
4152015
Homotopy type theory in Lean
F Doorn, J Raumer, U Buchholtz
International Conference on Interactive Theorem Proving, 479-495, 2017
282017
Path spaces of higher inductive types in homotopy type theory
N Kraus, J von Raumer
2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2019
132019
Coherence via well-foundedness: Taming set-quotients in homotopy type theory
N Kraus, J von Raumer
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020
9*2020
A syntax for mutual inductive families
A Kaposi, J von Raumer
Schloss Dagstuhl--Leibniz-Zentrum für Informatik 167, 23, 2020
42020
Formalization of non-abelian topology for homotopy type theory
J von Raumer, S Awodey, F Herrlich
MA thesis. Karlsruhe Institute of Technology, 2015. url: http://vonraumer …, 2015
42015
A Rewriting Coherence Theorem with Applications in Homotopy Type Theory
N Kraus, J von Raumer
arXiv preprint arXiv:2107.01594, 2021
12021
Reducing inductive-inductive types to indexed inductive types
T Altenkirch, A Kaposi, A Kovács, J von Raumer
24th International Conference on Types for Proofs and Programs, TYPES, 2018
12018
Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover.
J von Raumer
ICMS, 28-33, 2016
12016
Higher inductive types, inductive families, and inductive-inductive types.
J von Raumer
University of Nottingham, 2020
2020
Formalizing Double Groupoids and Cross Modules in the Lean Theorem Prover
J Raumer
International Congress on Mathematical Software, 28-33, 2016
2016
The Jordan-Hölder Theorem
J Von Raumer
Arch. Formal Proofs 2014, 2014
2014
An Induction Principle for Cycles
N Kraus, J von Raumer
EUTYPES-TYPES 2020-Abstracts, 0
The system can't perform the operation now. Try again later.
Articles 1–13