[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
POSTDOC POSITION IN MACHINE-VERIFIED SEMANTICS AT PRINCETON|
The Programming Languages group at Princeton University's Department of Computer Science is soliciting applications for a post-doctoral research position in the Concurrent C Minor project, led by Andrew Appel. This is a one-year position, renewable, starting mid-August 2009.
The research is on the application of semantics to provide a machine-verified foundation for usable-scale languages, compilers, and program analysis tools. We use axiomatic semantics (e.g., Concurrent Separation Logic), operational semantics, modal logics; we relate these to each other by machine-checked proofs in Coq. We prove things about languages at the level of C, and (eventually) upward to functional languages and downward to machine language. We work closely with the CompCert project led by Xavier Leroy at INRIA and with the SAnToS laboratory led by John Hatcliff at Kansas State University.
The ideal candidate will have completed a PhD in Computer Science, and will have expertise and experience with several of the following: Operational Semantics; Use of proof assistants (such as Coq, Isabelle/HOL, Twelf, or others); Axiomatic Semantics (such as Hoare Logic, Separation Logic); Logic, Modal Logic; Compiler implementation; Formal verification; Program analysis algorithms and tools.
Submit applications (or inquiries) by e-mail to Andrew Appel <ap...@princeton.edu> with "2009 postdoc" in the Subject line. Include a CV in PDF, names of three references, and a brief statement of your research interests and accomplishments.
Princeton University is an equal opportunity employer and complies with applicable EEO and affirmative action regulations. For information about applying to Princeton and how to self-identify please see http://www.princeton.edu/dof/about_us/dof_job_openings/