Russell Metatheoretic Study in Coq. Matthieu Sozeau, Unpublished, 2006 - Notes.
Russell metatheoretic study
We seek to prove the correctness of Russell's type system and the
generation of proof obligations in Coq.
At present we've been able to prove the Subject Reduction property
of the declarative system, using the technique developped in .
I've written a draft walkthrough for the proof [1].