[TYPES/announce] Looking for PostDoc on Program Verification Techniques in F* and Coq

Sun Sep 11 03:02:59 EDT 2022

Hello everyone,

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 (MPI-SP). 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.

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.

MPI-SP <https://urldefense.com/v3/__https://www.mpi-sp.org/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkInaRNIX8$  > is a relatively new research institute
founded in 2019 and is part of the Computer Science area of the Max Planck
Society <https://urldefense.com/v3/__https://www.cis.mpg.de__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIcHrocUQ$  >. We are located on the campus of Ruhr
University Bochum, in the Rhein-Ruhr
<https://urldefense.com/v3/__https://en.wikipedia.org/wiki/Rhine-Ruhr__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIcZnxBUA$  >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.

Do not hesitate to contact me if you are interested in this position! (or
to forward this to someone who could be interested)

Kind Regards,

Catalin Hritcu

https://urldefense.com/v3/__https://catalin-hritcu.github.io__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkITE9O7Dk$  

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:

Verifying non-terminating programs with IO in F*
<https://urldefense.com/v3/__https://theowinterhalter.github.io/res/iodiv-hope.pdf__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkI6EQt480$  >. 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 (HOPE 2022) <https://urldefense.com/v3/__https://icfp22.sigplan.org/home/hope-2022__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIyvSY11g$  >. 11
September 2022 (today!).

Partial Dijkstra Monads for All
<https://urldefense.com/v3/__https://types22.inria.fr/files/2022/06/TYPES_2022_paper_18.pdf__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIXPfhwB8$  >. 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 (TYPES 2022)
<https://urldefense.com/v3/__https://types22.inria.fr/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIaWV_we4$  >. 2022.

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq
<https://urldefense.com/v3/__https://eprint.iacr.org/2021/397/20210526:113037__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIzBeih6I$  >. Carmine Abate, Philipp
G. Haselwarter, Exequiel Rivas, Antoine Van Muylder, Théo Winterhalter,
Cătălin Hrițcu, Kenji Maillard, and Bas Spitters. In 34th IEEE Computer
Security Foundations Symposium (CSF)
<https://urldefense.com/v3/__https://www.ieee-security.org/TC/CSF2021/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIbIsdkcU$  >. 2021. Distinguished Paper
Award.

Dynamic IFC Theorems for Free! <https://urldefense.com/v3/__https://arxiv.org/abs/2005.04722__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIvXYiorI$  >
Maximilian Algehed, Jean-Philippe Bernardy, and Cătălin Hrițcu. In 34nd
IEEE Computer Security Foundations Symposium (CSF)
<https://urldefense.com/v3/__https://www.ieee-security.org/TC/CSF2021/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIbIsdkcU$  >. 2021.

Hybrid Enforcement of IO Trace Properties
<https://urldefense.com/v3/__https://src.acm.org/binaries/content/assets/src/2021/cezar-constantin-andrici.pdf__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIjuBRXT8$  >.
Cezar-Constantin Andrici. 1st prize in the Student Research Competition of ICFP
2020
<https://urldefense.com/v3/__https://icfp20.sigplan.org/track/icfp-2020-student-research-competition*Results__;Iw!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkImet5F0Y$  >
.

The Next 700 Relational Program Logics <https://urldefense.com/v3/__https://arxiv.org/abs/1907.05244__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkI3paNbOs$  >.
Kenji Maillard, Cătălin Hrițcu, Exequiel Rivas, and Antoine Van Muylder.
PACMPL, 4(POPL <https://urldefense.com/v3/__https://popl20.sigplan.org/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIwNgKH1k$  >), 2020.

Dijkstra Monads for All <https://urldefense.com/v3/__https://arxiv.org/abs/1903.01237__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIXrFXagI$  >. Kenji Maillard,
Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hrițcu, Exequiel Rivas,
and Éric Tanter. PACMPL, 3(ICFP <https://urldefense.com/v3/__https://icfp19.sigplan.org/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIBmpMfnE$  >), 2019.

Recalling a Witness: Foundations and Applications of Monotonic State
<https://urldefense.com/v3/__http://arxiv.org/abs/1707.02466__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkI0Ff2RL4$  >. Danel Ahman, Cédric Fournet, Cătălin
Hrițcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. PACMPL, 2(POPL
<https://urldefense.com/v3/__https://popl18.sigplan.org/__;!!IBzWLUs!RyFIxUeMi0ltHMQ9-5t9wrWLjyB73bjk00RlD0_Cm53yM5JR8kX24ufewVt472yH3PiZF4ziz4WRozLvY-_vDo5JqDdfMlkIRjtVLlU$  >), 2018.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20220911/0648defa/attachment-0001.htm>