CSEC: Certified Software Engineering in Coq

The development of tools to construct software systems that respect a given specification is a major challenge of current and future research in computer science. Interactive theorem provers based on type theory, such as Coq, have shown their effectiveness to prove correctness of important pieces of software like the C compiler of the CompCert project. Certified programming with dependent types is attracting a lot of attention recently, and Coq is the de facto standard for such endeavors, with an increasing amount of users, pedagogical material, and large-scale projects. Nevertheless, significant work remains to be done to make Coq more usable from a software engineering point of view.

This collaboration project gathers the expertise of researchers from Chile (Inria Chile, Universidad de Chile, Universidad Católica de Valparaíso), France (Inria Nantes, Inria Paris) and Argentina (Universidad Nacional de Córdoba), in different areas that are crucial to develop the vision of certified software engineering. The focus of this project is both theoretical and practical, covering novel foundations and methods, design of concrete languages and tools, and validation through specific case studies. The end result will be a number of enhancements to the Coq proof assistant (frameworks, tactic language) together with guidelines and demonstrations of their applicability in realistic scenarios.

Kick-off Workshop: March 6-9, 2018 @ DCC

Titles & abstracts of the talks

Slides of the talks are now available! Expand the abstracts to see the link.

Guillaume Munch-Maccagnoni:

  • Why Evaluation Order Matters
  • Curry-Howard for RAII

Federico Olmedo:

  • Language-based Cryptographic Proofs in Coq, or Coq for Probabilistic Programs
  • Improving the Proof Experience in Coq

Pierre-Marie Pédrot:

  • Proof Assistants for Free
  • Weaning and The Exceptional Type Theory

Matthieu Sozeau:

  • An Environment for Programming with Dependent Types, take II
  • Towards Certified Meta-Programming with Typed Template Coq

Nicolas Tabareau:

  • Homotopy Types and Resizing Rules: a fresh look at the impredicate sort of CIC
  • Univalent parametricity

Éric Tanter:

  • Foundations of Dependent Interoperability
  • The Essence of Gradual Typing

Beta Ziliani:

  • Towards typed-tactics in Coq: the what, the why, and the how

Program

Participants

  • Martin Bodin (U Chile)
  • Raimil Cruz (U Chile)
  • Tomas Díaz (U Chile)
  • Hans Fehrmann (U Chile)
  • Ismael Figueroa (PUC Valparaíso)
  • Elizabeth Labrada (U Chile)
  • Fabián Mosso (U Chile)
  • Guillaume Munch-Maccagnoni (Inria Nantes)
  • Federico Olmedo (U Chile)
  • Pierre-Marie Pédrot (MPI)
  • Paula Ríos (U Chile)
  • Matthieu Sozeau (Inria Paris)
  • Nicolas Tabareau (Inria Nantes)
  • Éric Tanter (U Chile)
  • Matías Toro (U Chile)
  • Beta Ziliani (U Córdoba)