The Parsifal team, in the Laboratory of Informatics of the École polytechnique, works on foundational aspects of proof theory as well as on the design and implementation of systems that exploit that foundational work. Recently prototyped systems support logic programming, model checking, and automated reasoning. These systems are used to study a wide range of computational logic issues, including program correctness, security, concurrency, and operational semantic specifications and their formalized meta-theory.

University of Luxembourg is specifically collaborating with prof. Tomer Libal, a visiting researcher in the University of Luxembourg. Prof. Libal is an expert in higher-order automated theorem proving and is the developer of several tools in computational logic.