Author of the publication

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Unsolvability of the Quintic Formalized in Dependent Type Theory., , , and . ITP, volume 193 of LIPIcs, page 8:1-8:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2021)Gardening with the Pythia A Model of Continuity in a Dependent Setting., , and . CSL, volume 216 of LIPIcs, page 5:1-5:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2022)A First Order Theory of Diagram Chasing., and . CSL, volume 288 of LIPIcs, page 38:1-38:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2024)A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)., , , and . ITP, volume 8558 of Lecture Notes in Computer Science, page 160-176. Springer, (2014)A Formal Proof of the Irrationality of ζ(3)., and . CoRR, (2019)Machine-Checked Computational Mathematics (Invited Talk).. CALCO, volume 270 of LIPIcs, page 5:1-5:1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2023)Compositional Pre-processing for Automated Reasoning in Dependent Type Theory., , , , , , and . CPP, page 63-77. ACM, (2023)Trocq: Proof Transfer for Free, With or Without Univalence., , and . ESOP (1), volume 14576 of Lecture Notes in Computer Science, page 239-268. Springer, (2024)Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence., , and . ESOP (1), volume 14576 of Lecture Notes in Computer Science, page 269-274. Springer, (2024)Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341)., , , and . Dagstuhl Reports, 8 (8): 130-155 (2018)