<div dir="ltr">A postdoctoral position is available in the <a href="https://urldefense.com/v3/__https://www.bc.edu/bc-web/schools/mcas/departments/computer-science.html__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A80wW_G6A$" target="_blank">Computer Science department</a><div>at <a href="https://urldefense.com/v3/__https://www.bc.edu/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A_VEWsg6Q$" target="_blank">Boston College</a> under the supervision of <a href="https://urldefense.com/v3/__https://jtristan.github.io/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A8-o69J6g$" target="_blank">Jean-BaptisteTristan</a> and</div><div><a href="https://urldefense.com/v3/__http://www.cs.bc.edu/*tassarot/__;fg!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A-NPlTytA$" target="_blank">Joseph Tassarotti</a>. The candidate will join our project on the formally verified</div><div>compilation of probabilistic programs.<br><br>The goal of the project is to use the <a href="https://urldefense.com/v3/__https://coq.inria.fr/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A9fgOuDoQ$" target="_blank">Coq proof assistant</a> to implement<br>a compiler for the <a href="https://urldefense.com/v3/__https://mc-stan.org/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A-DbjA-XQ$" target="_blank">Stan programming language</a> and prove that the<br>generated inference algorithm converges to the distribution specified<br>by the input program. Our project builds upon the <a href="https://urldefense.com/v3/__https://compcert.org/__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A9S6eyDoQ$" target="_blank">CompCert compiler</a><br>and compiles Stan programs with a succession of well-defined program<br>transformations. Candidates are expected to participate in the<br>generalization of existing transformations to more features of the<br>Stan language, the design and implementation of new transformations,<br>the definition of the operational semantics of the intermediate<br>languages, and the proofs of semantics preservation.<br><br>Successful candidates must be proficient in scientific writing and have a track record of expertise in at least one of the following topics:<br><br>* Formal verification using interactive theorem provers<br>* Semantics and compilation of programming languages<br>* Probabilistic programming<br><br>The position is available immediately, with a flexible starting<br>date. It includes funds for travel to conferences and comes with no<br>teaching load.<br><br>Interested candidates should <a href="https://urldefense.com/v3/__https://bc.csod.com/ats/careersite/jobdetails.aspx?site=1&c=bc&id=4776__;!!IBzWLUs!GUgeO-Glg0TTFG8UUr-BwD83uf5QSmvK4dGsC6pqPn14KJTOa0m4gNv_olihUJQQubWP0A9QWE9OEg$">apply at this link</a> and contact <a href="mailto:tristanj@bc.edu" target="_blank">Jean-Baptiste Tristan</a><br><<a href="mailto:tristanj@bc.edu" target="_blank">tristanj@bc.edu</a>> and <a href="mailto:tassarot@bc.edu" target="_blank">Joseph Tassarotti</a> <<a href="mailto:tassarot@bc.edu" target="_blank">tassarot@bc.edu</a>> with a copy<br>of their CV.<font color="#888888"><br></font></div><font color="#888888"><div><br></div>--<br><div dir="ltr"><div dir="ltr">Jean-Baptiste Tristan<div>Associate Professor</div><div>Computer Science Department</div><div>Boston College</div></div></div></font></div>