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)
    • Coinduction in Agda using Copatterns and Sized Types
  • Amal Ahmed (Northeastern University)
  • Nick Benton & Andrew Kennedy (MSR Cambridge)
    • Generating Certified x86 Code in a Proof Assistant
  • Lars Birkedal (Aarhus University)
  • Arthur Charguéraud (INRIA Saclay - Île-de-France)
  • Adam Chlipala (MIT)
    • Bedrock: A Foundational Proof-Carrying Code Platform with Functional Correctness Proofs
  • 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)
    • TBA
  • Robert Harper (TBC) (Carnegie Mellon University)
  • Martin Hofmann (Ludwig-Maximilians-Universität München)
    • Abstract effects and proof-relevant logical relations
  • Xavier Leroy (INRIA Paris-Rocquencourt)
    • Verified static analyses
  • Greg Morrisett (Harvard University)
    • Engineering Challenges for Modeling Languages
  • Magnus Myreen (University of Cambridge)
    • CakeML: a verified implementation of ML
  • Aleksandar Nanevski (IMDEA, Madrid)
    • TBA
  • David Pichardie (ENS Rennes)
    • Atomicity Refinement for Verified Compilation
  • Peter Sewell (University of Cambridge)
    • TBA
  • Aaron Turon (Max-Planck Institute for Software Systems)
    • Navigating weak memory with ghosts, protocols, and separation
  • Tarmo Uustalu (Tallin University of Technology)
  • Viktor Vafeiadis (Max-Planck Institute for Software Systems)
    • An Argument for Relaxed Program Logic
  • Stéphanie Weirich (University of Pennsylvania)
    • Combining Proofs and Programs in a Dependently Typed Language
  • Hongseok Yang (University of Oxford)
    • Replicated Data Types: Specification, Verification, Optimality
  • Nobuko Yoshida (Imperial College, London)
    • Idioms for Interaction and their applications in large distributed systems
  • Francesco Zappa-Nardelli (INRIA Paris-Rocquencourt)
  • Steve Zdancewic (University of Pennsylvania)
    • Vellvm: Verifying Transformations of the LLVM IR


workshop_5.1393688702.txt.gz · Last modified: 2014/03/01 16:45 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