hermesmarc Goto Github PK

I'm a mathematician by training, but arguably more of a logician by practice. As you can see below, I have done some work on the intersection of computer-verified mathematics, first-order arithmetic and computability theory, in particular making use of an approach coined synthetic computability.

I am currently looking for a PhD position in the area of mathematical logic, interested in continuing research on mechanized mathematics, topics like paraconsistent logics, the boundaries of the incompleteness theorems, or combinations of these themes.

If you are interested or have any pointers for me in this regard, please feel free to contact me!

• An Analysis of Tennenbaum’s Theorem in Constructive Type Theory
  • 👥 Marc Hermes, Dominik Kirst
  • 🏆 Won the Award for Best Paper by Junior Researchers (FSCD 2022)
  • 📘 Included in the Journal Logical Methods in Computer Science (Volume 20 Issue 1).
• Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
  • 👥 Dominik Kirst, Marc Hermes
  • 🔖 First published at ITP 2021
  • 📘 Extended version in the Journal of Automated Reasoning (Volume 67)
• My Master Thesis: Modeling Peano Arithmetic in Constructive Type Theory