Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.

This is an old revision of the document!

Certification of high-level and low-level programs

Dates and location

From July 7 to July 11, at Institut Henri Poincaré.


This workshop is organised around invited talks and plenty of time for discussions. Topics of interest include :

  • separation logic and concurrency (CSL, rely-guarantee, ramified separation logic, high-order concurrency, …)
  • semantics of low-level languages (C, SSA, weak-memory models, effects and monads, linear logic, games semantics…)
  • compositional verification and program refinement (library abstractions, simulation, logical relations, …)
  • compositional verified compilers (CompCert, LLVM, translation validation, …)
  • certified system software (runtime environment, GC, OS kernels, web servers & other applications, network controllers, …)
  • advanced proof techniques for formalizing syntax and semantics (binding, co-induction, dependent types…)


  • Andreas Abel (Chalmers University)
  • Amal Ahmed (Northeastern University)
  • Nick Benton (MSR Cambridge)
  • Lars Birkedal (Aarhus University)
  • Arthur Charguéraud (INRIA Saclay - Île-de-France)
  • Adam Chlipala (MIT)
  • Derek Dreyer (TBC) (Max-Planck Institute for Software Systems)
  • Philippa Gardner (TBC) (Imperial College, London)
  • Dan Ghica (University of Birmingham)
  • Alexey Gotsman (TBC) (IMDEA, Madrid)
  • Robert Harper (TBC) (Carnegie Mellon University)
  • Martin Hofmann (Ludwig-Maximilians-Universität München)
  • Andrew Kennedy (MSR Cambridge)
  • Xavier Leroy (INRIA Paris-Rocquencourt)
  • Greg Morrisett (Harvard University)
  • Magnus Myreen (University of Cambridge)
  • Aleksandar Nanevski (IMDEA, Madrid)
  • Peter O'Hearn (TBC) (University College London)
  • Matthew Parkinson (MSR Cambridge)
  • David Pichardie (ENS Rennes)
  • Peter Sewell (University of Cambridge)
  • Aaron Turon (Max-Planck Institute for Software Systems)
  • Tarmo Uustalu (Tallin University of Technology)
  • Viktor Vafeiadis (Max-Planck Institute for Software Systems)
  • Stéphanie Weirich (University of Pennsylvania)
  • Hongseok Yang (University of Oxford)
  • Nobuko Yoshida (Imperial College, London)
  • Francesco Zappa-Nardelli (INRIA Paris-Rocquencourt)
  • Steve Zdancewic (University of Pennsylvania)


workshop_5.1392373852.txt.gz · Last modified: 2014/02/14 11:30 by paulin
Dieses Dokuwiki verwendet ein von Anymorphic Webdesign erstelltes Thema.
www.chimeric.de Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0