[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Join Penn as a postdoc on the DeepSpec <http://deepspec.org/> 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 <http://deepspec.org/research/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 <http://deepspec.org/research/Haskell/>
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 <http://deepspec.org/research/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
([email protected] <mailto:[email protected]>), 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
<http://deepspec.org/>.
Looking forward to your application,
Benjamin Pierce
Stephanie Weirich
Steve Zdancewic
