The Coq mailing list

["Andrew W. Appel" <appel AT CS.Princeton.EDU>]

Some coq-club subscribers reported that my e-mail of January 23,
describing an opportunity for postdocs or research scientists,
got caught in a spam filter. In this e-mail I'll just give the link,

http://www.cs.princeton.edu/node/25188

That link gives the "official" description of the job opening.
Here's an informal description of the research projects envisioned:

The Verifiable C program logic, in the Verified Software Toolchain,
   http://vst.cs.princeton.edu
is an expressive higher-order impredicative separation logic for the
C programming language, proved sound with respect to CompCert C.
In order to "tame" such an expressive logic within Coq, we have derived
proof rules and Ltac programming to help automate interactive proofs,
and we're working on efficient interactive symbolic execution via
computational reflection.  Verifiable C has been used to prove functional
correctness of some nontrivial (though small) real-world programs such
as SHA-256 and HMAC.

The semantic model of the VST allows us to prove sound the rules
of Concurrent Separation Logic (CSL) to reason about Dijkstra-Hoare-style
synchronized shared-memory programs.  The question is, how should
a real-world CSL be applied to real-world programs?  Results such as
"Thread-modular shape analysis" (Gotsman/Berdine/Cook/Sagiv, PLDI 2007)
are an interesting start, but that's only a shape analysis--we want to prove
functional correctness of these programs with nontrivial 
application-specific
invariants, all made "foundational" by relating to our CSL proof rules
proved sound with respect to the CompCert operational semantics.
What's the right mixture of sophisticated static-analysis algorithms
with higher-order user-supplied functional-correctness invariants?

We ask this question for both sequential programs and concurrent programs,
and there are many interesting paths we might pursue in this investigation.

The postdoc position is officially listed for just one year, but there is a
very real possibility of extending it for a second or third year.

-- Andrew Appel