Type theory in relation with functional programming, term rewriting, automated proof assistants. Logical foundations of verification: temporal logic, program logics, monadic logic, and their relations to automata and games. The research topics concern in particular the expressiveness of various logical calculi, decidability issues, and efficiency of model checking.