The Lean theorem prover (system description) L de Moura, S Kong, J Avigad, F Van Doorn, J von Raumer Automated Deduction-CADE-25: 25th International Conference on Automated …, 2015 | 465 | 2015 |

The Lean theorem prover L de Moura, S Kong, J Avigad, F Van Doorn, J von Raumer | 30 | 2015 |

Homotopy type theory in Lean F van Doorn, J von Raumer, U Buchholtz Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017 | 28 | 2017 |

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 | 14 | 2019 |

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 | 4 | 2020 |

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 | 4 | 2015 |

A rewriting coherence theorem with applications in homotopy type theory N Kraus, J von Raumer Mathematical Structures in Computer Science 32 (7), 982-1014, 2022 | 2 | 2022 |

Higher inductive types, inductive families, and inductive-inductive types J von Raumer University of Nottingham, 2020 | 1 | 2020 |

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 | 1 | 2018 |

Formalizing double groupoids and cross modules in the lean theorem prover J von Raumer Mathematical Software–ICMS 2016: 5th International Conference, Berlin …, 2016 | 1 | 2016 |

The Jordan-Hölder Theorem J von Raumer | | 2016 |

An Induction Principle for Cycles N Kraus, J von Raumer EUTYPES-TYPES 2020-Abstracts, 0 | | |