Valery Trifonov

Associate Research Scientist of Computer Science

M.S., Sofia University, Sofia, Bulgaria, 1985
Ph.D., Johns Hopkins University, 1997
Joined Yale Faculty 1997
Personal Homepage

Office Location: AKW 304
Telephone: 203.432.7606

Valery Trifonov's interests are in the semantics and implementations of programming languages, including type systems and compilation techniques for object-oriented languages, and higher-order typed intermediate languages. Currently he is working with Zhong Shao on the FLINT project, designing intermediate calculi for compiling higher-order typed languages–ML, Haskell, Java–to proof-carrying machine code. The reflexive properties of the developed languages are so expressive that they allow constructing machine-verifiable safety proofs for services typically included in the trusted computing base (the runtime or the operating system), such as storage reclamation and dynamic loading. His current research is focused on extending this design to the level of safe mobile machine code.

Representative Publications:
	"A type system for certified binaries, with Zhong Shao, Bratin Saha, and Nikolaos Papaspyrou. In Proceedings of POPL 2002: The 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 217-232.
	"Fully reflexive intensional type analysis, with Bratin Saha and Zhong Shao. In Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming, pp. 82-93.
	"Representing Java classes in a typed intermediate language, with Christopher League and Zhong Shao. In Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming, pp. 183-196. Subtyping Constrained Types, with Scott F. Smith. In Proceedings of the 3rd International Symposium on Static Analysis, Lecture Notes in Computer Science 1145, Springer-Verlag, 1996, pp. 349-365.