Teoria typów w odniesieniu do programowania funkcyjnego, przepisywanie termów, automatyczne wspomaganie dowodzenia. Logiczne podstawy weryfikacji: logika temporalna, logika programów, logika monadyczna i jej związek z automatami i grami. Tematy badawcze dotyczą między innymi siły wyrazu rozmaitych rachunków logicznych, rozstrzygalności, oraz efektywności weryfikacji modelowej.