Index of /PEOPLE/monin/SmallInversions

	Name	Last modified	Size	Description
	Parent Directory		-
	Coq_Workshop_2010/	2026-09-10 17:30	-
	LPAR_2026/	2026-09-11 09:45	-
	Years/	2026-09-11 10:01	-
	README.md	2026-09-11 10:02	791
	README.html	2026-09-11 10:02	1.3K

This place is dedicated to small inversions for Coq and Rocq.

PBSI

The more recent development is called PBSI (proxy-based small inversions). It is largely automated in a tool mainly developed by Basile Gros, during its PhD under the supervision of Pierre Corbineau and Jean-François Monin. This tool is available here:

https://github.com/BasileGros/proxy-based-small-inversions

History (sketch)

• 2010: first version published at the Coq Workshop
• 2013: second version published at ITP, based on continuations
• 2015-now: unpublished version used in teaching, based on auxiliary algebraic types. Became basic PBSI.
• 2026: PBSI published at LPAR, including dependent PBSI that facilitate the development of Rocq programs with dependent types and of proofs over them.

Coucou