John-Baptiste Tristan, Paul Govereau and Greg Morrisett.
In PLDI'11: Proceedings of the ACM SIGPLAN Conference on Programming Design and Implementation, 2011. ACM Press.
See Also: Harvard University Technical Report TR-01-11, January 2011. Type-theoretic semantics for transactional concurrency
Aleksandar Nanevski, Paul Govereau and Greg Morrisett.
In TLDI'09: Proceedings of the 4th ACM SIGPLAN Workshop on Types in Language Design and Implementation, 2009. ACM Press.
See Also: Harvard University Technical Report TR-09-07, July 2007. Ynot: dependent types for imperative programs
Aleksandar Nanevski and Greg Morrisett and Avraham Shinnar and Paul Govereau and Lars Birkedal
In ICFP'08: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, 2008. ACM Press.
An Expressive Language of Signatures.
Norman Ramsey, Kathleen Fisher and Paul Govereau.
In ICFP'05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, 2005. ACM Press. Type Generativity in Higher-Order Module Systems
Paul Govereau.
Harvard University Technical Report TR-05-05, 2005.
 |
The LLVM M.D. (Mis-optimization Detector) Project. A denotational translation validator designed to detect compiler optimizations that change the meaning of the input program. |
 |
The Ynot Project: A next generation functional programming language that provides clean support for dependent and refinement types within a modern functional language. The focus of this work is on the integration of dependent types with effectful computations so that we can reason as easily about programs with effects as without. |
 |
I a former member of the C-- project. In the past, I have worked on the C-- runtime system, and the Power PC code generator. I also developed a Tiger front-end and garbage collector for testing and documentation purposes. |