Tadeusz’s teaching, activities and research

Contact details

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

My work

  • Here is my CV, if you need it for whatever reason.
  • 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:

  • 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.
  • 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.


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:

My irregular offerings so far:

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.


Here you can find a link to our ESSLLl 2021 lectures with Albert Visser.


Office hours

Just contact me by email.

Coauthors and teachers

And besides…

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: ja2lis2017.jpeg photo_california.jpg perhaps_not_freiling1.jpg P1100667_me.jpg