Archived Research Projects

They can be revived at any time!

Compiler Correctness

Nick Benton, Robert Harper and I managed to prove the correctness of compiling polymorphism of System F to dynamic typing through a modified cross-language logical relation.