Professor of Computer Science, Yale University
Welcome to my home page! I am interested in doing research on programming languages, formal methods, operating systems, and computer security. I am an advocate of certified software. I believe that certified programming with mechanized proofs is the most promising approach toward building truly dependable software and taking control of the rapidly growing complexity in future computer systems.
I lead the FLINT group at Yale. Together with my OS colleagues, we are interested in building novel certified system software. Our work spans many fields, ranging from programming language design, compiler development, formal semantics and logics, proof engineering and automation, realistic OS kernel hacking, to solving difficult problems related to all aspects of concurrency and distributed computing.
I am looking for new postdocs and phd students. Feel free to contact me if you have interests in or around my research areas, are creative and highly motivated, and have strong technical skills.
I will be teaching CS430 Formal Semantics in Fall 2013. In the past I taught CS112 Introduction to Programming, CS421 Compilers and Interpreters, CS422 Operating Systems, CS428 Language-Based Security, and CS210 A Second Course in Programming. I also attend the systems seminars on APLAR and SPAM.
Please submit to ESOP 2014.