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 |