An Ssreflect Tutorial

Georges Gonthier (1) , Roux Stéphane Le (2)

1 Microsoft - Microsoft Research [Cambridge]
2 MSR - INRIA - Microsoft Research - Inria Joint Centre

This document is a tutorial for ssreflect which is a proof language based on Coq. This tutorial is mostly dedicated to people who already know the basics of logic.

Mots clés: proof assistants; formal proofs; Coq; small scale reflection; tactics

Domaines: Logique en informatique [cs.LO]

Georges Gonthier, Roux Stéphane Le. An Ssreflect Tutorial. [Technical Report] RT-0367, INRIA. 2009, pp.33. ⟨inria-00407778⟩