The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

Join Penn as a postdoc on the DeepSpec project!

Outstanding postdocs with interests in programming languages, formal verification, and systems software are invited to join the programming languages group at Penn!  We are currently seeking researchers as part of “The Science of Deep Specification,” an NSF-funded Expedition in Computing.  

The goal of DeepSpec is to catalyze the adoption of deep specification techniques, through a tightly integrated combination of focused research, course development, and community building.  At Penn, Steve Zdancewic leads the Vellvm project, which provides a Coq specification of the LLVM intermediate representation. In this Expedition, Vellvm will serve as a testbed for experimenting with proof-engineering techniques and as a component of a larger system involving many deep specifications. Handling deep specifications at such a large scale (and that evolve over time, as LLVM’s must) will require significant technical advances. Stephanie Weirich leads the CoreSpec project, which seeks to develop a Coq specification of the core language of the Glasgow Haskell Compiler (GHC).  This part of the DeepSpec project will extend the breadth of the connected network of specifications to include a industrial-strength high-level programming language.  Benjamin Pierce leads the QuickChick project, focused on property-based testing of deep specifications.  The goal of this part of the DeepSpec research is to accelerate the development of deeply specified software by supporting a smooth transition between automated random testing and full formal verification.  Another strong focus of work at Penn will be on the role of deep specifications in modernizing undergraduate curricula in traditional core subjects such as operating systems and compilers.

These threads are closely connected to the other components of the DeepSpec consortium. In particular, this work will be done in the context of interconnected systems, interacting with and building on verified operating systems (CertiKOS, Yale), verified C compilers (CompCert and Verifiable C, Princeton), and verified hardware programming (Kami, MIT).  

The ideal candidate will have a PhD in Computer Science or a related field and experience with the Coq proof assistant or a similar tool. To ensure full consideration, please send a CV and research statement to Benjamin Pierce (bcpierce AT cis.upenn.edu), and arrange for at least three letters of reference to be sent to the same address, by February 15, 2016.  

The University of Pennsylvania  is an equal opportunity employer. All qualified applicants will receive consideration for employment without regard to race, color, religion, sex, national origin, disability status, protected veteran status, or any other characteristic protected by law.

More information about the DeepSpec project is available at deepspec.org.

Looking forward to your application,

  Benjamin Pierce

  Stephanie Weirich

  Steve Zdancewic