Dan (Daniel) Frumin

I am a logician and a computer scientist in Fundamental Computing group at the University of Groningen. I am interested in concurrent programs and reasoning about their behavior. My research interest include

• semantics of programming languages;
• program verification and concurrent separation logics;
• substructural logics and their proof theory;
• type theory and type systems;
• formal proofs and proof assistants (especially Univalent Foundations).

I finished my PhD under the supervision of Herman Geuvers, Freek Wiedijk, and Robbert Krebbers at Radboud University Nijmegen. My thesis is available online, together with the associated Coq mechanizations. After my PhD, I have been a postdoc with Lars Birkedal at the Logic and Semantics group, and a postdoc with Jorge Pérez at the Fundamental Computing group.

• Modular Denotational Semantics for Effects with Guarded Interaction Trees
  with Amin Timany and Lars Birkedal
  POPL, 2024, Distinguished Paper Award, Coq formalization
• A Minimal Formulation of Session Types
  in submission, 2023, with Alen Arslanagić and Jorge A. Pérez
• Semantic Cut Elimination for the Logic of Bunched Implications and Structural Extensions, Formalized in Coq
  in submission, 2023, Coq formalization, slides the GroLog talk. This is an extended version of the CPP 2022 paper, including more details on the formalization and a new section/formalization on analytic completion of structural rules.
• A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
  with Emanuele D’Osualdo, Bas van den Heuvel, and Jorge A. Pérez
  OOPSLA 2022
• Semantic cut elimination for the logic of Bunched Implications, formalized in Coq
  CPP 2022, Distinguished Paper Award, Coq formalization, slides, video
• Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
  with Simon Friis Vindum and Lars Birkedal
  CPP 2022, Coq formalization as part of ReLoC
• Bicategories in Univalent Foundations
  with Benedikt Ahrens, Niels van der Weide, Marco Maggesi, and Niccolò Veltri
  Mathematical Structures in Computer Science, 2020 (Special Issue on Homotopy Type Theory); extended an overhauled version of the FSCD 2019 paper
• ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
  with Robbert Krebbers and Lars Birkedal
  LMCS, 2021. Supersedes the LICS’18 paper
• Compositional Non-Interference for Fine-Grained Concurrent Programs
  with Robbert Krebbers and Lars Birkedal
  Security & Privacy 2021 Coq sources, Recorded talk
• Bicategories in Univalent Foundations
  with Benedikt Ahrens, Niels van der Weide, and Marco Maggesi
  FSCD 2019. This is superseded by the journal version.
• Semi-automated reasoning about non-determinism in C expressions
  with Léon Gondelman and Robbert Krebbers
  ESOP 2019. Accompanying web page, Coq formalization
• ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
  with Robbert Krebbers and Lars Birkedal
  LICS 2018. This is superseded by the journal version.
• Finite Sets in Homotopy Type Theory
  with Herman Geuvers, Léon Gondelman, and Niels van der Weide
  CPP 2018. Web page with the artifact and the slides
• A homotopy-theoretic model of function extensionality in the effective topos
  with Benno van den Berg
  Mathematical Structures in Computer Science, 2018

• Stroopt seminar (Groningen)
• GroLog seminar (Groningen)
• Bernoulli Institute Colloquia Computer Science (Groningen)
• BI’s Maths Event Calendar (Groningen)
• NetTCS: Network, Types, Coalgebras, Semantics (NL)
• Dutch Categories And Types seminar (NL)
• Logseminar (Aarhus)
• Software Science Seminar (Radboud)
• Online Worldwide Seminar on Logic and Semantics (Worldwide-ish)

• The name of this website is a nod to the ’96 paper of Hofmann and Streicher
• Some misc code/formalisations I wrote
• a very small hott-coq quickref | gnomes wearing hats | hamster.html
• The “What Is…?” column from the Notices of the AMS archive
• Weather | buienradar | Central station
• cs.LO | cs.PL