Certification of high-level and low-level programs

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)
  • Compositional Compiler Verification for a Multi-language World
• Nick Benton & Andrew Kennedy (MSR Cambridge)
  • Generating Certified x86 Code in a Proof Assistant
• Lars Birkedal (Aarhus University)
  • Impredicative Concurent Abstract Predicates
• Arthur Charguéraud (INRIA Saclay - Île-de-France)
  • Interactive verification of stateful higher-order programs using characteristic formulae
• Adam Chlipala (MIT)
  • Bedrock: A Foundational Proof-Carrying Code Platform with Functional Correctness Proofs
• Derek Dreyer (TBC) (Max-Planck Institute for Software Systems)
  • Navigating weak memory with ghosts, protocols, and separation
• Philippa Gardner (Imperial College, London)
  • TBA
• Dan Ghica (University of Birmingham)
  • Compiling functional programs to distributed architectures using abstract machine nets
• 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
• David Pichardie (ENS Rennes)
  • Atomicity Refinement for Verified Compilation
• Peter Sewell (University of Cambridge)
  • Before Certification: Engineering Validatable Models
• Tarmo Uustalu (Tallin University of Technology)
  • Precise qualification of effects with dependently typed monads
• Viktor Vafeiadis (Max-Planck Institute for Software Systems)
  • An Argument for Relaxed Program Logic
• Stephanie 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)
  • Concurrency and compiler correctness
• Steve Zdancewic (University of Pennsylvania)
  • Vellvm: Verifying Transformations of the LLVM IR

• Christine Paulin-Mohring
• Zhong Shao