| 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 |
© 2024 | Verona University
******** CSS e script comuni siti DOL - frase 9957 ********p>
