The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I'm giving some thought to applying.  I'm finishing my PhD sometime this Spring and can start shortly afterwards.

In addition to finishing my PhD, I'm working as a software engineer in the medical center.  There is a decent chance that I'll stay in the medical center.  However, I also want to look at other jobs that are closely related to my PhD.

Of the projects mentioned in the email, I'm most interested in Vellvm.  In addition to the work I'm doing with the Coq theorem prover, I've also done quite a bit of iOS development and would be interested in making Vellvm more compatible with the latest LLVM and iOS.  Both the Objective C and Swift programming languages (in which all iOS apps are developed) use LLVM as the basis for their compilers.

For information on my research check out my home page at www.cs.jhu.edu/~roe.  I'm going to be at Princeton Monday, Nov 20 for NJPLS.  I'm giving a talk on my advanced rewriting ml-plugin.

                          - Ken

Ken Roe - Department of Computer Science

Who Am I? I'm a graduate student. I started in the Fall of 2010. I am also a software engineer working for Casey Overby in DHSi. I decided to return to ...

www.cs.jhu.edu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Steve Zdancewic <stevez AT cis.upenn.edu>
Sent: Tuesday, November 14, 2017 8:03 AM
To: types-announce AT lists.seas.upenn.edu; deepspec-pi AT lists.cs.princeton.edu; coq-club AT inria.fr
Subject: [Coq-Club] Postdoc Positions at The University of Pennsylvania

 

PENN’S PL CLUB IS LOOKING FOR POSTDOCS

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

START DATES: Negotiable, beginning as early as January 2018.

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 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://nam04.safelinks.protection.outlook.com/?url="https%3A%2F%2Fgoo.gl%2Fforms%2FSMu8KmtdHjXKnqWF3&data=02%7C01%7Ckendroe%40hotmail.com%7C2f950e7f605045d594bc08d52b797db5%7C84df9e7fe9f640afb435aaaaaaaaaaaa%7C1%7C0%7C636462723195477213&sdata=MsatUapNKB%2BBmwmQx%2FpIYvp6Vi5mUPnQfju%2B97hV9Uw%3D&reserved=0

-   Direct your letter writers to submit their letters via:
     https://nam04.safelinks.protection.outlook.com/?url="https%3A%2F%2Fgoo.gl%2Fforms%2FElgimgzvDh4C2scu1&data=02%7C01%7Ckendroe%40hotmail.com%7C2f950e7f605045d594bc08d52b797db5%7C84df9e7fe9f640afb435aaaaaaaaaaaa%7C1%7C0%7C636462723195477213&sdata=7GFpsYds%2Fct75BPhQz8O8zkRbun%2FtAd2MC0ObUWTIco%3D&reserved=0

-   Contact Steve Zdancewic (mailto:stevez AT cis.upenn.edu) if you have any
     questions.

DEADLINE: Applications will be considered starting on _1 December 2017_
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.


Vellvm II - Verified LLVM

The Vellvm project is building a (verified LLVM), a framework for
reasoning about programs expressed in LLVM’s intermediate representation
and transformations that operate on it. Vellvm provides a mechanized
formal semantics of LLVM’s intermediate representation, its type system,
and properties of its SSA form. Specific research topics include:
developing modular semantics for low-level control-flow-graph and SSA
representations; extending the model to account for concurrency;
building a “decompiler” from SSA to a higher-order functional language;
or using the LLVM semantics to verify correctness of compiler analyses,
optimization passes, and security-relevant program transformations.


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.