Dan Frumin (home page)


I am a postdoc researcher in Jorge Perez’s group Fundamental Computing.

My research is focused around program logics and semantics of programming languages, especially with applications to concurrency. More broadly, I am interested in logic, both pure and with applications to computer science (concurrency, type theory).

I did my PhD under the supervision of Herman Geuvers, Freek Wiedijk, and Robbert Krebbers. My thesis is available online, together with the associated Coq mechanizations.

Some of the Coq formalizations I work(ed) on:

  • ReLoC: concurrent separation logic for proving refinements programs
  • SeLoC: concurrent separation logic for proving non-interference
  • BI-cutelim: semantic cut elimination for BI

Contact information

  • Email: d.frumin `at` rug.nl
  • Office: 01.01, Mercator 1 building, Toernooiveld 212, Nijmegen 6525 EC working from home


Preprints / drafts