PTSF27jul13.zip

original formalisation by Vincent Siles that this is based on:

master thesis by Floris van Doorn, of which these are the Coq files: thesis.pdf