Program and Slides

You can find the program on the website of Floc2018.

  • Zachary Tatlock, Verifying Distributed Systems (slides)
  • Véronique Benzaken and Évelyne Contejean, A Coq mechanised formal semantics for real life SQL queries : Formally reconciling SQL and (extended) relational algebra (slides)
  • Armaël Guéneau, Procrastination, A proof engineering technique (slides) (demo)
  • Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling and Pierre-Yves Strub, Classical Analysis with Coq (slides)
  • Sylvain Boulmé, What is the Foreign Function Interface of the Coq Programming Language? (slides)
  • Olivier Laurent, Preliminary Report on the Yalla Library (slides)
  • Mirai Ikebuchi and Keisuke Nakano, ComplCoq: Rewrite Hint Construction with Completion Procedures (slides)
  • Cyprien Mangin and Matthieu Sozeau, Towards a formalization of the guard condition (slides)
  • Jason Gross, Teaching Your Rooster to Crow in C
  • Lasse Blaauwbroek, Proof Construction by Tactic Learning
  • Coq Development Team session (slides)

Comments are closed.