9:00-10:00 | Invited talk: Peter Selinger | Number-theoretic Methods in Quantum Computing |

10:00-10:30 | coffee break | |

Special session | Security | |

10:30-11:00 | Stephen Chong | Expressive Information Security Policies |

11:00-11:30 | Aslan Askarov | Security policies in the presence of active adversaries |

11:30-12:00 | Andrew Myers | Integrating authorization with information flow |

12:00-12:30 | Geoffrey Smith | Quantitative Information Leakage Policies |

12:30-14:00 | lunch break | |

Contributed session | ||

14:00-14:25 | Fabio Zanasi | The algebra of partial equivalence relations |

14:25-14:50 | Arthur Azevedo de Amorim | Binding Operators for Nominal Sets |

14:50-15:15 | Jonas Frey | Classical realizability in the CPS target language |

15:15-15:45 | coffee break | |

Contributed session | ||

15:45-16:10 | Richard Statman | On the representation of semigroups and other congruences in the lambda calculus |

16:10-16:35 | Barry Jay | Programs as Data Structures in Lambda-SF -Calculus |

16:35-17:00 | Marc Bagnol, Richard Blute, J.R.B. Cockett and J.S. Lemay | The shuffle quasimonad and modules with differentiation and integration |

17:00-17:25 | Robin Cockett and Jonathan Gallagher | Categorical Models of the Differential λ-Calculus Revisited |

9:00-10:00 | Invited talk: Brigitte Pientka | Programming Coinductive Proofs Using Observations |

10:00-10:30 | coffee break | |

Special session | Verification | |

10:30-11:15 | Andrew Appel | Engineering Operational Semantics: CompCert C as a case study |

11:15-11:40 | Steve Zdancewic | Vellvm, a Formalization of the LLVM Compiler Infrastructure |

11:40-12:05 | Gordon Stewart | Operational Semantics of a Compositional Compiler |

12:05-12:30 | Jan Hofmann | Operational Cost Semantics and Quantitative CompCert |

12:30-14:00 | lunch break | |

Contributed session | ||

14:00-14:25 | Jurriaan Rot | Coalgebraic minimization of automata by initiality and finality |

14:25-14:50 | Sergey Goncharov, Stefan Milius and Christoph Rauch | Complete Elgot Monads and Coalgebraic Resumptions |

14:50-15:15 | Bram Geron and Paul Blain Levy | Iteration and labelled iteration |

15:15-15:45 | coffee break | |

Contributed session | ||

15:45-16:10 | Tomáš Jakl, Achim Jung and Aleš Pultr | Bitopology and four-valued logic |

16:10-16:35 | Richard Statman | How to think of intersection types as Cartesian products |

16:35-17:00 | David Mestel and Bill Roscoe | Reducing complex CSP models to traces via priority |

9:00-10:00 | Invited talk: Nathalie Bertrand | Fault diagnosis in probabilistic models |

10:00-10:30 | coffee break | |

Special session | Probabilistic programming | |

10:30-11:15 | Dan Roy | Probabilistic Programming for Machine Learning and Statistics |

11:15-11:40 | Johannes Borgstrom | A Lambda-Calculus Foundation for Universal Probabilistic Programming |

11:40-12:05 | Sam Staton | Semantics for Probabilistic Programming Languages |

12:05-12:30 | Ken Shan | Operational Semantics for Disintegration |

12:30-14:00 | lunch break | |

Contributed session | ||

14:00-14:25 | Fredrik Dahlqvist, Vincent Danos and Ilias Garnier | Giry and the Machine |

14:25-14:50 | Tetsuya Sato | Approximate Relational Hoare Logic for Continuous Random Samplings |

14:50-15:15 | Tyler Barker | A Monad for Randomized Algorithms |

15:15-15:45 | coffee break | |

Contributed session | ||

15:45-16:10 | Bart Jacobs and Fabio Zanasi | A predicate/state transformer semantics for Bayesian learning |

16:10-16:35 | Bart Jacobs | Effectuses from Monads |

9:00-09:45 | Peter O'Hearn | Concurrent Separation Logic: retrospects and prospects |

9:45-10:10 | Tony Hoare | A Unification of Theories of Concurrent Programming |

10:10-10:40 | coffee break | |

10:40-11:05 | Bill Roscoe | Linking the Malvern Hills: Bridging the Brooksian Peaks |

11:05-11:30 | Viktor Vafeiadis | Explaining Weak Memory Models with Program Transformations |

11:30-12:30 | Invited talk: Steve Brookes | A Denotational Approach to Weak Memory Concurrency |

12:30-14:00 | lunch |