Logic

Maria Paola Bonacina
Professore ordinario
Andrea Masini
Professore ordinario
Margherita Zorzi
Ricercatore a tempo determinato
Competenze
Argomento Persone Descrizione
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.
Verifica del software Maria Paola Bonacina
Procedure di decisione per la soddisfacibilità modulo teorie e loro applicazione alla verifica di proprietà di programmi; generazione di invarianti mediante dimostrazione di teoremi; generazione di interpolanti mediante dimostrazione di teoremi; raffinamento di astrazioni per model checking o analisi statica mediante dimostrazione di teoremi

Attività

Strutture

Condividi