This directory is dedicated to the file comparison.v
that is mentioned in the paper accepted at LPAR-26
     A Minimalist Approach to Trustworthy Programming with
            Precise Types using Small Inversions
authored by Pierre Corbineau, Basile Gros and Jean-François Monin.

This file contains material for comparing 4 approaches to programming
with dependent types available in Rocq
- the approach at the core of thei paper, called PBSI
  (proxy-based small inversions)
- 3 other approaches (inversion, small inversions presented
  by the 3rd author and Shi at ITP'13, and ethe Equations Package.

Stable contact information:
pierre.corbineau@univ-grenoble-alpes.fr
jean-francois.monin@univ-grenoble-alpes.fr