A Tutorial on Equations
Equations is a plugin for the Coq proof assistant which provides a notation for defining programs by dependent pattern-matching and structural or well-founded recursion. It additionally derives useful high-level proof principles for demonstrating properties about them, abstracting away from the implementation details of the function and its compiled form. The general design and implementation of the plug-in presented in [Sozeau and Mangin 2019] provides a robust and expressive function definition package as a definitional extension to the Coq kernel. At the core of the system is a new simplifier for dependent equalities based on an original handling of the no-confusion property of constructors.
In this tutorial talk, we will present Eqations’ main features from the user point-of-view. This includes Eqations’ grammar for defining programs by dependent pattern-matching and well- founded recursion, highlighting the treatment of Uniqueness of Identity Proofs and the facilities provided for the definition of well- founded or structurally recursive nested or mutually recursive functions. The package also includes supporting tactics for reason- ing a posteriori on Eqations definitions: an elimination principle tailored to the function definition and a set of rewrite rules cor- responding to its clauses; both allow the development of concise and robust proof scripts involving the definitions. Finally, the de- pendent pattern-matching engine at the core of Eqations is also made available in proof mode through a general purpose depen- dent pattern-matching tactic that is more expressive than current destruction tactics and intro-patterns (destruct, inversion or Ssreflect’s elim and vanilla Coq or Ssreflect intro-patterns). The material presented here is part of lecture notes to be integrated in an upcoming volume of Software Foundations centered on the use of advanced tools in Coq.
Sat 25 JanDisplayed time zone: Saskatchewan, Central America change
10:30 - 12:30
|Deriving Instances with Dependent Types|
Arthur Azevedo de Amorim Carnegie Mellon University, USAFile Attached
|The use of Coq for Common Criteria Evaluations|
Yves Bertot INRIA, Maxime Dénès Inria, Vincent Laporte Inria, Arnaud Fontaine ANSSI, Thomas Letan ANSSIFile Attached
|Verifying concurrent Go code in Coq with Goose|
Tej Chajed Massachusetts Institute of Technology, USA, Joseph Tassarotti Boston College, M. Frans Kaashoek Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts Institute of Technology, USALink to publication File Attached
|A Tutorial on Equations|
Matthieu Sozeau InriaMedia Attached File Attached