Theoretische Informatik


Tadeusz's teaching, activities and news page

Contact details

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

Besides, here is my CV (never quite up-to-date), if you need it for whatever reason. And here is my publication list, most of the time up-to-date.

Recent projects and publications

At any given moment, I'm pursuing several projects. Those few ongoing or recently completed ones which can be advertised right now include:

  • Lewis meets Brouwer: constructive strict implication with Albert Visser. Our invited contribution to appear in the special issue of Indagationes Mathematicae “L.E.J. Brouwer, 50 years later”. An executive summary by Albert: More or less everything the authors know about the Lewis Arrow (but not quite: there will hopefully be a sequel). We illustrate the rich life of the arrow in the constructive context. More specifically, we argue that in the constructive setting it is not enough to do modal logic with an unary box and an unary diamond, even when the modal relation in Kripke semantics is binary. The box, in particular, needs to be replaced by the original “strict implication” of C. I. Lewis. We present its various appearances, ranging from logics of provability in HA to functional programming.
  • Our most recent paper with Wesley H. Holliday, One modal logic to rule them all?, got accepted at AiML 2018. Also with Wes, I managed to solve a decade-old open problem from my PhD Thesis (restated in §6 of the Algebras and Coalgebras chapter in the Handbook of Modal Logic). The issue of “sub-Kripkean” algebraic completeness is quite relevant for the development of modal possibility semantics in Wesley's group. And now, we have a massive paper accepted by The Review of Symbolic Logic and available in the UC eScholarship system. Previously presented this at Logic Colloquium of UC Berkeley (April 2015), Trends in Logic 2015, and ToLo V in 2016.
  • Our paper on Negative Translations and Normal Modality (with Miriam Polzer and Ulrich Rabenstein) has been accepted to FSCD 2017 (here's a local copy). A Coq formalization can be found here. The title is, hopefully, self-explanatory. Again, we believe this fills a rather large gap in the literature. Here are the slides of FSCD presentation.
  • This is a rather unusual subject for me, but my paper on Infinite Populations, Choice and Determinacy has been invited and accepted to a forthcoming special issue of Studia Logica on Logics for Social Behaviour. Like other references, this paper is also about being careful with non-constructive assumptions… but in a rather unexpected setting and involving somewhat uncommon tools.
  • The ultimate paper on Coalgebraic Predicate Logic (CPL) with Lutz Schröder, Dirk Pattinson and Katsuhiko Sano. Our invited (and accepted) contribution to a special festschrift issue of Logical Methods in Computer Science in honor of Jiří Adámek. Apart from details of all proofs, revamped examples and presentation, we are presenting new theorems (e.g., omitting types) and a redesigned Gentzen calculus. Our earlier papers are JLC 2017 (on a suitable variant of van Benthem/Rosen theorem for CPL, invited to a special issue on Special issue on Canonicity and Correspondence for Nonclassical Logics), and much prior to that, some conference (ICALP 2012, TbiLLC 2011) material.
  • Guard your daggers and traces with Stefan Milius has (finally!) appeared in a special issue of Fundamenta Informaticae with selected papers from FiCS'13 (yes, it's vol. 150 from 2017…). Yes, this is also proof theory of a constructive modal logic… in a heavily categorical disguise. We are working now on a follow-up paper, focusing on guarded traces in non-cartesian setting.
  • Relational Lattices: From Databases to Universal Algebra, a massively improved and extended journal version of a previous conference paper with Szabolcs Mikulas and Jan Hidders was invited to and published in a special issue of JLAMP (Volume 85 from June 2016, full versions of selected papers from 14th RAMiCS). Here is a local copy. Another (non-boolean) perspective on foundations of relational model in database theory. Luigi Santocanale has obtained some interesting results playing with pure lattice signature (CMCS 2016) and has answered some of our challenges regarding undecidability (RAMiCS 2017), demonstrating a connection with modal logic in the process. And with Jan, we are now obtaining more positive results adapting more standard database techniques. This, too, will be published in due course.

  • An Algebraic Glimpse at Bunched Implications and Separation Logic (here's a local copy) with Peter Jipsen. A draft of our invited contribution to the collection “Hiroakira Ono on Residuated Lattices and Substructural Logics”. We believe this fills a rather large gap in the literature and that it is going to be a useful reference for anybody interested in (generalized) logic of Bunched Implications, intuitionistic generalizations of arrow logic, or simply substructural logic in computer science.
  • My tribute to the memory of Leo Esakia and Dito Pataraia (an invited chapter in a dedicated volume of Outstanding Contributions to Logic series, but I'd rather suggest you read Author's Cut available on arXiv or its local copy). Again, constructive modalities with provability (and computer science) smack. An overview which triggered my interest in the subject.

These are the things I have been working on since I arrived at FAU in late 2012. At the moment, according to Google Scholar, my most quoted publications still come from the earlier, pre-2012 period, but this is likely to change. All my publications, including earlier ones, can be found here.


I have been a PC member of RAMiCS 2018, AIRIM'18, WoC 2015, RAMiCS 2014, AiML 2012 and TACL 2011.

(Speaking of TA(N)CL, here is a photo from the first edition (Tbilisi 2003) from its old webpage. If you happen to work in the area, have fun identifying participants!)

I have been 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 forthcoming sixth edition.


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.

In the forthcoming semester (SoSe 2017/2018), I am going to be responsible for:

Other courses I have taught at FAU:

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.

Leiden 2014 workshop

… see dedicated webpage for that. Or, for that matter, the Infinite Populations, Choice and Determinacy paper.

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