See my original webpage/online business card for these. Go there if you find the picture on the right confusing.

• Here is my CV, if you need it for whatever reason.

• Essential information about my work can be found in my research statement. You can also consult this overview (mostly for years 2014-2018).

• All my publications, including earlier ones, can be found here. Moreover, Google Scholar is also quite good at being up-to-date, whatever one thinks of Google. Other aggregators, scientific networks, DBLP etc. are suboptimal. After a long break, I started again recently to experiment with researchgate.

I will be/have been a PC member of RAMiCS 2020, RAMiCS 2018, AIRIM’18, WoC 2015, RAMiCS 2014, AiML 2012 and TACL 2011.

I will be/have been an invited speaker at workshop on proof theory and logic (Utrecht U, 2019), algebra and duality in non-classical logic at Chapman U. (2018) and ILLC, UvA (201) , a keynote speaker at ALCOP 2015 (and a speaker at several other editions), an invited speaker at OAL2.0 (2011) and a guest lecturer at several graduate and summer schools (see below for the last item). Besides, I have been a semi-regular invitee of the International Workshop on Topological Methods in Logic, including the second, the third, the fifth and the sixth edition. The fifth edition in 2016 included my tutorial on Dialogues, Proofs and Programs. Finally, I gave something of a tutorial at the Logics for Social Behaviour workshop, Lorentz Center 2014.

Coq formalizations and occasionally educational software developed by myself and/or my students:

• A Coq formalization of our (almost) entire AiML 2018 paper with Wesley H. Holliday developed by my student Michael Sammler.

• A Coq formalization of our FSCD 2017 paper Negative Translations and Normal Modality with Miriam Polzer and Ulrich Rabenstein. Here are the slides of the Oxford 2017 presentation and those of the Amsterdam 2018 presentation and those of the Prague 2019 presentation.

• Miriam’s earlier formalization of a fundamental result in relational algebra/calculus in database theory by Sagiv and Yannakakis. Depends on a formalization of the relational calculus by Benzaken et al. (ESOP 2014) whose code has never been made publicly available.

• The code of our fork (SemProg) of Software Foundations by Pierce et al. Here is the actual GitHub repository: email me for access (for researchers only).

• A Coq formalization of a most peculiar result about the intuitionistic propositional calculus, proved by Wim Ruitenburg in 1984. Here are the slides of TACL 2017 presentation on the subject and here is its abstract. See also my Prague ICS AML presentation (Oct 2019) for more on the background.

• An almost entirely verified formalization of correspondence for inductive formulas (SQEMA) by Merlin Göttlinger. One “unfold” proof obligation broke all machines and OS‘s Merlin tested.

• Paul Wild’s development of Aarhus ModuRes library. I guess mostly rendered obsolete by newer versions of Iris and follow-up projects.

• Here’s the webpage for Michael Gebhard’s implementation of LOOP/WHILE language used in several standard references (and in our ThInfWiL course). You can compare it with an earlier BSc project by Alexander Dietsch on the same subject. Compare it also with Michael Banken’s BSc work on simulating counter machines.

At any moment, I am open towards supervision of FAU students, be it Bachelor or Master level. Please see our project webpage for some proposals and do talk to me also if you have other ideas.

I am regularly responsible for:

• Practical Semantics of Programming Languages (SemProg) since the first edition in 2013 (in 2017 jointly with Christoph Rauch and in 2013 jointly with Daniel Gorín). A course I introduced into the Chair curriculum. Seems a fixture each spring/summer term as long as I am at FAU, and most likely beyond that.
• Formal Methods for Software Development (FMSoft) (tutorials by Christoph Rauch) since WS 2015/16. In WS 2014/2015, I did tutorials for the same lecture (and the experience led me to drastically change the choice of software on offer after I took over).
• Supervision of tutors for Übungen zu Theoretische Informatik für Wirtschaftsinformatik und Lehramt (ÜThInfWI-A) since SS 2014 (with the exception of 2016).

My irregular offerings so far:

• I designed the lecture Logical Foundations of Database Theory (LGruDat). In WS 2016/17 with tutorials by Christoph Rauch, entirely solo in WS 2013/14 .
• In WS 2015/16, I was teaching a course on Nonclassical Logics in Computer Science (NoCL) (jointly with Lutz Schröder).
• In SS 2017, I was responsible for Seminar on Homotopy Type Theory (jointly with Sergey Goncharov).
• In SS 2014, I was responsible for Seminar Categories in Programming (CaP) (jointly with Sergey Goncharov).
• In WS 2013/14, I was responsible for Seminar Curry-Howard Correspondence (SemCurry) (jointly with Daniel Gorín).
• Finally, during the first year of my stay at FAU, I was assisting as tutor with the last edition of Komplexität von Algorithmen (SS 2013) and one of earlier editions of GLoLoP (WS 2012/13),

My previous teaching activities elsewhere include:

• Teaching the course Generative Development at the CS Department, University of Leicester in 2012. This was a one-off to help the department in an emergency situation. My help for the department included also individual BSc and MSc supervision and moderation (supervision) of a number of projects in their Personal and Group skills module. Some were fun.

• Occasional self-designed courses at summer schools or PhD schools. Examples so far include Provability, fixed points and clock ticks (4 hrs) at the Midlands Graduate School (MGS 2012), Birmingham or Queries, Modalities, Relations, Trees, XPath (15 hrs) at the Summer School Leicester-JXNU 2010, Jangxi Normal University, Nanchang, China.

ESSLLI 2021

Office hours

Just contact me by email.

• As for my coauthors so far, you have already seen above some of the most recent ones in the hot projects section above: Albert Visser, Wesley Holliday, Lutz Schröder, Daniel Hausmann, Christoph Rauch, Michael Sammler, Deepak Garg, Derek Dreyer, Peter Jipsen, Dirk Pattinson, Katsuhiko Sano, Stefan Milius, Jan Hidders, Szabolcs Mikulas, Miriam Polzer, Matthias Zinner and Ulrich Rabenstein. The earlier ones were: Frank Wolter, Balder ten Cate, Gaëlle Fontaine, Maarten Marx, Tomasz Kowalski, Sven Helmer, Daniela Petrișan and Murdoch Gabbay. I also don’t mind writing papers on my own. Recall that the full list can be found here.
• My PhD supervisor was sensei Hiroakira Ono (JAIST) and my Master of Philosophy supervisor was professor Andrzej Wroński (UJ). Here is an event back in 2011 celebrating both researchers.

Do read these remarks on “the threat from within” to academia by John Etchemendy, an accomplished logician and Stanford’s longest-serving provost (2000-2017).

Please also read this advice from professors of Princeton, Harvard and Yale.

Finally, here’s how I look like, in reverse chronological order: