[TYPES/announce] Several postdoc positions at Cornell and UCL

[Alexandra Silva]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all,

We invite applications for postdoctoral researchers at Cornell
University and University College London in the areas of networking,
programming languages, and verification.
These positions are part of the NetKAT project, which seeks to develop
new language abstractions for controlling, managing, and securing
networks. The primary goal of our current work is to extend the
language to support quantitative and probabilistic reasoning. Support
for these positions is provided by the ERC-funded ProFoundNet project
and the NSF-funded project "AiTF: Algorithms and Probabilistic
Semantics for Next-Generation Networks," as well as gifts from Cisco,
Facebook, Google, and Fujitsu.

Applicants should hold a PhD in Computer Science and have a desire to
work in an interdisciplinary team. Prior knowledge of measure theory
is a plus but not required. Successful candidates will be provided
with opportunities for professional development and for exploring
ideas that expand the scope of the project. The positions are for one
year initially but may be extended to additional years.

To apply, please send a CV, research statement, and the names of three
references to Nate Foster (jnfos...@cs.cornell.edu), Dexter Kozen
(ko...@cs.cornell.edu), and Alexandra Silva
(alexandra.si...@ucl.ac.uk). We especially welcome applications from
women and members of under-represented minority groups.

Nate Foster (Cornell)
Dexter Kozen (Cornell)
Alexandra Silva (UCL)

[TYPES/announce] Postdoc position at Penn on the DeepSpec project

[Benjamin C. Pierce]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


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 
(bcpie...@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