[TYPES/announce] Funded postdoc position in Formal Verified Compilation of Probabilistic Programming Languages at Boston College

[Jean-Baptiste Tristan]

A postdoctoral position is available in the Computer Science department
<https://urldefense.com/v3/__https://www.bc.edu/bc-web/schools/mcas/departments/computer-science.html__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A80wW_G6A$ >
at Boston College <https://urldefense.com/v3/__https://www.bc.edu/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A_VEWsg6Q$ > under the supervision of
Jean-BaptisteTristan <https://urldefense.com/v3/__https://jtristan.github.io/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A8-o69J6g$ > and
Joseph Tassarotti <https://urldefense.com/v3/__http://www.cs.bc.edu/*tassarot/__;fg!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A-NPlTytA$ >. The candidate will
join our project on the formally verified
compilation of probabilistic programs.

The goal of the project is to use the Coq proof assistant
<https://urldefense.com/v3/__https://coq.inria.fr/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A9fgOuDoQ$ > to implement
a compiler for the Stan programming language <https://urldefense.com/v3/__https://mc-stan.org/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A-DbjA-XQ$ > and
prove that the
generated inference algorithm converges to the distribution specified
by the input program. Our project builds upon the CompCert compiler
<https://urldefense.com/v3/__https://compcert.org/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A9S6eyDoQ$ >
and compiles Stan programs with a succession of well-defined program
transformations. Candidates are expected to participate in the
generalization of existing transformations to more features of the
Stan language, the design and implementation of new transformations,
the definition of the operational semantics of the intermediate
languages, and the proofs of semantics preservation.

Successful candidates must be proficient in scientific writing and have a
track record of expertise in at least one of the following topics:

* Formal verification using interactive theorem provers
* Semantics and compilation of programming languages
* Probabilistic programming

The position is available immediately, with a flexible starting
date. It includes funds for travel to conferences and comes with no
teaching load.

Interested candidates should apply at this link
<https://urldefense.com/v3/__https://bc.csod.com/ats/careersite/jobdetails.aspx?site=1&c=bc&id=4776__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A9QWE9OEg$ >
and contact Jean-Baptiste Tristan <tristanj at bc.edu>
<tristanj at bc.edu> and Joseph Tassarotti <tassarot at bc.edu> <tassarot at bc.edu>
with a copy
of their CV.

--
Jean-Baptiste Tristan
Associate Professor
Computer Science Department
Boston College
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20210812/67cd8599/attachment.htm>