| 10:00 - 11:00 | Session 1 |
|---|---|
| 10:00 - 10:30 | Antonio Bucciarelli |
| N-dimensional Booolean Algebras | |
| 10:30 - 11:00 | Alvaro Garcia-Perez |
| No Solvable Lambda-Value Term Left Behind | |
| 11:00 - 11:30 | Coffee break |
| 11:30 - 12:30 | Session 2 |
| 11:30 - 12:00 | Gilles Dowek |
| Linear Lambda-Calculus is Linear | |
| 12:00 - 12:30 | Loïc Peyrot |
| An Operational and Quantitative Study of Curry-Howard Langages | |
| 12:30 - 14:15 | Lunch break |
| 14:15 - 15:45 | Session 3 |
| 14:15 - 14:45 | Claudia Faggian |
| Bayesian Networks and Proof-Nets: a proof-theoretical account of Bayesian Inference | |
| 14:45 - 15:15 | Pablo Barenbaum |
| A Constructive Logic with Classical Proofs and Refutations | |
| 15:15 - 15:45 | Victor Arrial |
| Quantitative Inhabitation through Call-by-Push-Value | |
| 15:45 - 16:15 | Coffee break |
| 16:15 - 17:45 | Session 4 |
| 16:15 - 16:45 | Agustin Borgna |
| Encoding High-Level Quantum Programs as SZX-Diagrams | |
| 16:45 - 17:15 | Andrés Viso |
| Encoding Tight Typing in a Unified Framework | |
| 17:15 - 17:45 | Pierre Vial |
| Sniper: Using Metaprogramming to Improve Coq Automation | |
| 17:45 | Closing |