The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

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 is a relatively new research institute founded in 2019 and is part of the Computer Science area of the Max Planck Society. We are located on the campus of Ruhr University Bochum, in the Rhein-Ruhr 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://catalin-hritcu.github.io

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*. 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). 11 September 2022 (today!).

Partial Dijkstra Monads for All. 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). 2022.

SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq. 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 (CSF). 2021. Distinguished Paper Award.

Dynamic IFC Theorems for Free! Maximilian Algehed, Jean-Philippe Bernardy, and Cătălin Hrițcu. In 34nd IEEE Computer Security Foundations Symposium (CSF). 2021.

Hybrid Enforcement of IO Trace Properties. Cezar-Constantin Andrici. 1st prize in the Student Research Competition of ICFP 2020.

The Next 700 Relational Program Logics. Kenji Maillard, Cătălin Hrițcu, Exequiel Rivas, and Antoine Van Muylder. PACMPL, 4(POPL), 2020.

Dijkstra Monads for All. Kenji Maillard, Danel Ahman, Robert Atkey, Guido Martínez, Cătălin Hrițcu, Exequiel Rivas, and Éric Tanter. PACMPL, 3(ICFP), 2019.

Recalling a Witness: Foundations and Applications of Monotonic State. Danel Ahman, Cédric Fournet, Cătălin Hrițcu, Kenji Maillard, Aseem Rastogi, and Nikhil Swamy. PACMPL, 2(POPL), 2018.