The Coq mailing list

[Lennart Beringer <eberinge AT cs.princeton.edu>]

Applications are invited for a postdoc position at Princeton University,
in connection with an NSF-funded collaboration with William Mansky at
UI Chicago on concurrency aspects of the Verified Software Toolchain
(VST, https://vst.cs.princeton.edu).

Specifically, the researcher will use the Coq proof assistant to develop
proof rules, semantic foundations, and proof automation for low-level
concurrency primitives in concurrent separation logic, and will apply
these techniques to high-performance data structures and algorithms in C.
Additional information about the envisioned research is available at
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1811894.

Candidates are expected to have a PhD in a relevant area of programming
language research, formal methods, or systems programming, and be proficient 
in a modern proof assistant (Coq, Agda, Lean, Isabelle/HOL,...).

The position is initially available for one year, with a flexible start date.
In addition to daily interactions with other members of the VST group, the
successful candidate will have the opportunity to participate in activities
and events of the DeepSpec initiative (https://deepspec.org).

Applications should be submitted via the link provided at

https://puwebp.princeton.edu/AcadHire/apply/index.xhtml

under reference number D-20-COS-00007, and should include a statement of
research interests and accomplishments, a CV, and contact information
for at least two references.

There is no formal application deadline; applications submitted by
January 10th will be guaranteed to be considered.

Interested candidates are invited to contact me by email for informal
inquiries 
(eberinge AT cs.princeton.edu).