[TYPES/announce] Postdoc positions at the University of Pennsylvania

[Benjamin C. Pierce]

PENN’S PL CLUB IS LOOKING FOR POSTDOCS

The University of Pennsylvania’s PL group is looking to hire multiple postdoctoral researchers to work on projects related to verification, software specification, and security.

START DATES: Negotiable

DURATION: All positions are one year, with the possibility of extension to a second year.

QUALIFICATIONS: Applicants should have a Ph.D. in computer science and a strong background in one or more topics related to 
formal verification and specification
programming languages
type systems and semantics
the Coq theorem prover
the specific project topics described below.

APPLICATION PROCEDURE:
Upload a CV, statement of interest, and the names of three letter writers to: https://goo.gl/forms/SMu8KmtdHjXKnqWF3 <https://goo.gl/forms/SMu8KmtdHjXKnqWF3>
Direct your letter writers to submit their letters here: https://goo.gl/forms/ElgimgzvDh4C2scu1 <https://goo.gl/forms/ElgimgzvDh4C2scu1>
Contact Steve Zdancewic (stevez at cis.upenn.edu <mailto:stevez at cis.upenn.edu>) or Benjamin Pierce (bcpierce at cis.upenn.edu <mailto:bcpierce at cis.upenn.edu>) if you have any questions.
New applications will be considered starting immediately and will be considered until all the positions are filled.

Successful applicants will join the University of Pennsylvania’s PL Club with opportunities to collaborate on the DeepSpec project and other ongoing activities.


POTENTIAL RESEARCH PROJECTS

DeepWeb - A Formally Verified Web Server

Penn is coordinating a large-scale verification effort that combines technologies from across the DeepSpec project with the aim creating a verified web server: the high-level specification is in terms of the HTTP protocol, and the implementation will be high-performance C software (verfied using Princeton’s VST) hosted by Yale’s CertiKOS, which will itself be run on top of MIT’s verified implementation of the Risc V hardware. This project will tie together specification, verification, and testing across multiple levels of abstraction.

QuickChick - Property-Based Testing for Coq

The QuickChick project investigates the interplay between formal specification / verification and property-based random testing a la Haskell QuickCheck. The QuickChick tool (a QuickCheck-like testing framework for Coq) is heavily used in the DeepSpec project, for example as the specification framework for an executable formal specification of HTTP and related protocols. We are experimenting with using this specification as a bug-finding tool, both for industrial web servers and for initial prototypes of our own server. This requires addressing both foundational and engineering challenges, in the testing technology and in the creation of specifications that are suitable for both verification and testing.

Programming Languages for Differential Privacy

Penn boasts a longstanding and energetic collaborative research effort on putting new privacy technologies – particular statistical techniques such as differential privacy – into practice, involving faculty, students, and postdocs from programming languages, distributed systems, and algorithms, and machine learning. Topics of interest include privacy-protecting type systems and static analyses, distributed implementations of private algorithms, program logics for privacy, and formal verification of randomized algorithms.


THE UNIVERSITY OF PENNSYLVANIA

Penn’s department of Computer and Information Science offers a vibrant research environment with a long tradition of excellence in programming languages and related areas. We are located in Philadelphia, a city that offers a rich array of cultural, historical, and nightlife attractions, parks and outdoor recreation, convenient public transportation, and affordable housing.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20180112/442694b2/attachment.html>