PTSF27jul13.zip

• readme.txt

• f_term.v: source html
• f_env.v: source html
• f_typ.v: source html
• f_typ2.v: source html
• f_equivalence.v: source html

original formalisation by Vincent Siles that this is based on:

• base.v: source html
• ut_term.v: source html
• ut_env.v: source html
• ut_red.v: source html
• ut_typ.v: source html
• ut_sr.v: source html
• ut_typ_eq.v: source html
• term.v: source html
• env.v: source html
• red.v: source html
• typ_annot.v: source html
• strip.v: source html
• glue.v: source html
• final_result.v: source html

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