Boris Masiar Djalal's picture
Randi Heggernes Eilertsen

Boris Masiar Djalal

Researcher, Forsker
  • E-mailboris.djalal@uib.no
  • Visitor Address
    HIB - Thormøhlens gate 55
    5006 Bergen
  • Postal Address
    Postboks 7803
    5020 Bergen

Formalisation with the Coq proof assistant, SSReflect, Mathematical Components library

From now on you can follow the following link only:

We use the Coq proof assistant and follow (a modified version of) the
Volume 1: Logical Foundations of the electronic textbook Software Foundations.
The authors of Volume 1 are: Benjamin C. Pierce and Arthur Azevedo de Amorim and Chris Casinghino and Marco Gaboardiand and Michael Greenberg and Cătălin Hriţcu and Vilhelm Sjöbergand and Brent Yorge.
The modifications are mainly aimed at using the SSReflect set of tactics, which allows us to achieve the same things with fewer tactics to know.

Link to the modified volume 1 (modifiied chapters currently include Preface up to More Basic Tactics):

Link to try Coq code in your browser:
You may also want to try another editor, CoqIDE. You can install it with the Coq Platform (link: https://github.com/coq/platform).