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].
There's no documentation yet, except the one generated by
, here. You can also browse the sources.
Russell Metatheoretic Study in Coq. Matthieu Sozeau, Unpublished, 2006 - Notes.
Valid XHTML 1.1! Valid CSS!