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
Dale Miller
A proof theory for model checking: an overview
11:30
Lawrence Dunn and Jamie Vicary
Surface proofs for non-commutative linear logic
12:00
Matteo Acclavio
Proof diagrams for multiplicative linear logic
12:30-14:00
14:00-16:00 Programming Constructs (chair: D. Mazza)
14:00
Antoine Allioux
Krivine machine and Taylor expansion in a non-uniform setting
14:30
Stefano Guerrini
Linear beta-reduction
15:00
Max Willsey, Rokhini Prabhu and Frank Pfenning
Design and Implementation of Concurrent C0
15:30
Miguel Silva, Mário Florido and Frank Pfenning
Non-Blocking Concurrent Imperative Programming with Session Types
16:00-16:30
16:30-17:55 Models (chair: M. Fernandez)
16:30
Masahito Hasegawa
Linear Exponential Comonads without Symmetry
17:00
Daniyar Shamkanov
On Gödel's Second Incompleteness Theorem for Arithmetic without Contraction
17:30
All participants
Discussion
17:55-18:00 Goodbye (I. Cervesato and M. Fernandez)