Dan Frumin (home page)
About
I am currently a postdoc researcher in Jorge Perez’s group Fundamental Computing. I am interested in concurrency, type theory, logic, and program semantics.
Previously I was a PhD student under the supervision of Herman Geuvers, Freek Wiedijk, and Robbert Krebbers. My thesis is in the last editing stage and will be available online soon. The public defense will happen on the 12th of March 2021, at 11:30.
A lot of my research is supported by Coq formalizations, and during my work I have contributed to Iris, std++ and UniMath. Also check out ReLoC and SeLoC!
Contact information
- Email: d.frumin `at` rug.nl
- Office:
01.01, Mercator 1 building, Toernooiveld 212, Nijmegen 6525 ECworking from home :(
Writings
Publications and preprints
- Mechanized Verification of a Fine-Grained Concurrent Queue from Facebook’s Folly Library with Simon Friis Vindum and Lars Birkedal (draft version, 2020).
- ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity with Robbert Krebbers and Lars Birkedal (preprint 2020, supersedes the lics2018 paper).
- Compositional Non-Interference for Fine-Grained Concurrent Programs with Robbert Krebbers and Lars Birkedal (preprint 2020, accepted for Security & Privacy 2021). See also the slides from the Iris workshop and the Git repository.
- Bicategories in Univalent Foundations with Benedikt Ahrens, Niels van der Weide, and Marco Maggesi (v1 FSCD 2019, v2 is an extended version submitted for publication).
- Semi-automated reasoning about non-determinism in C expressions with Léon Gondelman and Robbert Krebbers (ESOP 2019). Please consult an accompanying web page and the formalization.
- A homotopy-theoretic model of function extensionality in the effective topos with Benno van den Berg (Mathematical Structures in Computer Science, 2018). (older arXiv preprint is available)
- ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency with Robbert Krebbers and Lars Birkedal (LICS 2018). See an accompanying web page with the tech report and additional formalisations. See the slides.
- Finite Sets in Homotopy Type Theory with Herman Geuvers, Léon Gondelman, and Niels van der Weide (CPP 2018). See an associated web page with the artifact and the slides.
Other
- Weak Factorisation Systems in the Effective Topos (MSc. Thesis; under the supervision of Benno van den Berg, 2016)
- Logic and homotopy in the category of assemblies (Study report; under the supervision of Jaap van Oosten, 2016)
- Presheaf models for concurrency (Study report; under the supervision of Giovanni Ciná, 2015)
Notes
- All notes/blog posts
- Notes on the Abadi-Plotkin logic (2016, updated 2019)
- Introduction to delimited continuations (sometime 2017/updated 2018)
- Diagonal argument(s) and Lawvere’s fixed point theorem (2015?)
- Frobenius property of a weak factorisation system (2016?)
Teaching
- Type Theory and Coq, 2019/2020. In the reading group part of the course we look at MetaCoq/TemplateCoq.
- Co-TA (with Niels) for Type Theory and Coq, 2018/2019. The topic for the last part of the course is guarded type theory.
- TA for Berekenbaarheid (Computability), 2018. Extra materials: some exercises on reductions and Rice’s theorem.
- TA for Type Theory and Coq, 2017/2018. In the third part of the course we will be looking at continuation passing style and CPS transformations.
- TA for Type Theory and Coq, 2016/2017. In the third part of the course we looked into logical relations. Extra materials: Contextual equivalence proof for logical relations, example proofs in the Abadi-Plotkin logic. UPDATE: there is now an even more comprehensive introduction to logical relations by Lau Skorstengaard on arXiv: https://arxiv.org/abs/1907.11133.
- TA for Berekenbaarheid (Computability), 2016
Seminars and meetings
- Bernoulli Institute Colloquia Computer Science
- Categories and Types Seminar (CATS) (UvA)
- Software Science Seminar (Radboud)
- Logseminar (Aarhus)
- Amsterdam/Utrecht Colloquium on Mathematical Logic
- Online Worldwide Seminar on Logic and Semantics (OWLS)
