Logic

Maria Paola Bonacina
Full Professor
Andrea Masini
Full Professor
Margherita Zorzi
Temporary Assistant Professor
Research interests
Topic People Description
Lambda Calculus Andrea Masini
Margherita Zorzi
Quantum and Probabilistic lambda calculi. Lambda calculus for Continuation Passing Style. Computational interpretation of modal proofs.
modal and temporal logics Andrea Masini
Margherita Zorzi
Proof theoretical analysis of modal and temporal logics. Modal and temporal logics for security. Distribute logics. Branching a linear temporal logics.
proof theory, Linear logic, Type theory Andrea Masini
Margherita Zorzi
Sequent calculi for modal, linear and temporal logics. Natural deduction systems for modal, linear and temporal logics. Labelled deductive systems. Type systems for CPS. Proof nets for linear and classical logics. Deductive systems for quantum computability.
Software Verification Maria Paola Bonacina
Decision procedures for satisfiability modulo theories and their application to check program properties; invariant generation by theorem proving; interpolating theorem proving; abstraction refinement for either model checking or static analysis by theorem proving

Activities

Research facilities