Workshop Program
Department of Computer Science, room 1.42
University of Porto
Porto, Portugal
10:00-10:30
| 10:30-10:35 | Welcome | (I. Cervesato and M. Fernandez) |
| 10:35-12:30 | Proof Theory | (chair: I. Cervesato) |
| 10:35 |
A proof theory for model checking: an overview
|
| 11:30 |
Surface proofs for non-commutative linear logic
|
| 12:00 |
Proof diagrams for multiplicative linear logic
|
12:30-14:00
| 14:00-16:00 | Programming Constructs | (chair: D. Mazza) |
| 14:00 |
Krivine machine and Taylor expansion in a non-uniform setting
|
| 14:30 |
Linear beta-reduction
|
| 15:00 |
Design and Implementation of Concurrent C0
|
| 15:30 |
Non-Blocking Concurrent Imperative Programming with Session Types
|
16:00-16:30
| 16:30-17:55 | Models | (chair: M. Fernandez) |
| 16:30 |
Linear Exponential Comonads without Symmetry
|
| 17:00 |
On Gödel's Second Incompleteness Theorem for Arithmetic without Contraction
|
| 17:30 |
Discussion
|
| 17:55-18:00 | Goodbye | (I. Cervesato and M. Fernandez) |