<div dir="ltr"><span id="gmail-docs-internal-guid-c16e0407-7fff-1e0b-1fe5-76b5ed29172f"><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Hello everyone,</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">A Postdoctoral Research position on Program Verification Techniques in F* and Coq is available in my group at the Max Planck Institute for Security and Privacy </span>(MPI-SP<span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">). I am looking for candidates with an excellent research track record and publications at top conferences (especially POPL and ICFP). I am particularly looking for someone with research expertise in: formal verification, proof assistants (particularly Coq and/or F*), type theory, effects, monads, functional programming, parametricity, programming language semantics, etc.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Candidates are expected to work collaboratively on topics of joint interest and to help co-advise students, but can also dedicate some of their time to their own independent projects.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__https://www.mpi-sp.org/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkInaRNIX8$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">MPI-SP</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> is a relatively new research institute founded in 2019 and is part of the </span><a href="https://urldefense.com/v3/__https://www.cis.mpg.de__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIcHrocUQ$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">Computer Science area of the Max Planck Society</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. We are located on the campus of Ruhr University Bochum, in the </span><a href="https://urldefense.com/v3/__https://en.wikipedia.org/wiki/Rhine-Ruhr__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIcZnxBUA$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">Rhein-Ruhr </span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">metropolitan region, Germany’s largest academic hub. The working language of MPI-SP is English, and no knowledge of German is required for this job.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:400;font-style:normal;font-variant:normal;text-decoration:none;vertical-align:baseline;white-space:pre-wrap">Do not hesitate to contact me if you are interested in this position! (or to forward this to someone who could be interested)</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><br><span id="gmail-docs-internal-guid-7768a036-7fff-01f6-243f-d20641aa00cf"></span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Kind Regards,</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">Catalin Hritcu</span></p><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__https://catalin-hritcu.github.io__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkITE9O7Dk$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">https://catalin-hritcu.github.io</span></a></p><br><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">PS: If you’re interested in this position, in a couple of days I can also provide you with a large (non-exhaustive) list of potential research topics on which we could work together. In the meantime, here are our recent papers in this space:</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__https://theowinterhalter.github.io/res/iodiv-hope.pdf__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkI6EQt480$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">Verifying non-terminating programs with IO in F*</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. Cezar-Constantin Andrici, Théo Winterhalter, Cătălin Hrițcu, and Exequiel Rivas. To be presented at the 10th ACM SIGPLAN Workshop on Higher-Order Programming with Effects </span><a href="https://urldefense.com/v3/__https://icfp22.sigplan.org/home/hope-2022__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIyvSY11g$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">(HOPE 2022)</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. 11 September 2022 (</span><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">today!</span><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">).</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__https://types22.inria.fr/files/2022/06/TYPES_2022_paper_18.pdf__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIXPfhwB8$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">Partial Dijkstra Monads for All</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. Théo Winterhalter, Cezar-Constantin Andrici, Cătălin Hrițcu, Kenji Maillard, Guido Martínez, and Exequiel Rivas. Presented at the 28th International Conference on Types for Proofs and Programs </span><a href="https://urldefense.com/v3/__https://types22.inria.fr/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIaWV_we4$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">(TYPES 2022)</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. 2022.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__https://eprint.iacr.org/2021/397/20210526:113037__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIzBeih6I$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. Carmine Abate, Philipp G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter, Cătălin Hrițcu, Kenji Maillard, and Bas Spitters. In 34th IEEE Computer Security Foundations Symposium </span><a href="https://urldefense.com/v3/__https://www.ieee-security.org/TC/CSF2021/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIbIsdkcU$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">(CSF)</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. 2021. Distinguished Paper Award.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__https://arxiv.org/abs/2005.04722__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIvXYiorI$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">Dynamic IFC Theorems for Free!</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap"> Maximilian Algehed, Jean-Philippe Bernardy, and Cătălin Hrițcu. In 34nd IEEE Computer Security Foundations Symposium </span><a href="https://urldefense.com/v3/__https://www.ieee-security.org/TC/CSF2021/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIbIsdkcU$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">(CSF)</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. 2021.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__https://src.acm.org/binaries/content/assets/src/2021/cezar-constantin-andrici.pdf__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIjuBRXT8$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">Hybrid Enforcement of IO Trace Properties</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. Cezar-Constantin Andrici. 1st prize in the Student Research Competition of </span><a href="https://urldefense.com/v3/__https://icfp20.sigplan.org/track/icfp-2020-student-research-competition*Results__;Iw!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkImet5F0Y$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">ICFP 2020</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__https://arxiv.org/abs/1907.05244__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkI3paNbOs$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">The Next 700 Relational Program Logics</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. Kenji Maillard, Cătălin Hrițcu, Exequiel Rivas, and Antoine Van Muylder. PACMPL, 4(</span><a href="https://urldefense.com/v3/__https://popl20.sigplan.org/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIwNgKH1k$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">POPL</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">), 2020.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__https://arxiv.org/abs/1903.01237__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIXrFXagI$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">Dijkstra Monads for Al</span><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">l</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hrițcu, Exequiel Rivas, and Éric Tanter. PACMPL, 3(</span><a href="https://urldefense.com/v3/__https://icfp19.sigplan.org/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIBmpMfnE$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">ICFP</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">), 2019.</span></p><br><p dir="ltr" style="line-height:1.38;margin-top:0pt;margin-bottom:0pt"><a href="https://urldefense.com/v3/__http://arxiv.org/abs/1707.02466__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkI0Ff2RL4$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-weight:700;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">Recalling a Witness: Foundations and Applications of Monotonic State</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">. Danel Ahman, Cédric Fournet, Cătălin Hrițcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. PACMPL, 2(</span><a href="https://urldefense.com/v3/__https://popl18.sigplan.org/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIRjtVLlU$" style="text-decoration-line:none"><span style="font-family:Arial;background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;text-decoration-line:underline;vertical-align:baseline;white-space:pre-wrap">POPL</span></a><span style="font-family:Arial;color:rgb(0,0,0);background-color:transparent;font-variant-numeric:normal;font-variant-east-asian:normal;vertical-align:baseline;white-space:pre-wrap">), 2018.</span></p><br></span></div>