Branching Processes of Conservative Nested Petri Nets. - Daniil Frumin; Irina A. Lomazova (VPT@CAV, 2014)

Finite sets in homotopy type theory. - Dan Frumin; Herman Geuvers; Léon Gondelman; Niels van der Weide (CPP, 2018)

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. - Dan Frumin; Robbert Krebbers; Lars Birkedal (LICS, 2018)

Semi-automated Reasoning About Non-determinism in C Expressions. - Dan Frumin; Léon Gondelman; Robbert Krebbers (ESOP, 2019)

Bicategories in Univalent Foundations. - Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niels van der Weide (FSCD, 2019)

A benchmark for C program verification. - Marko C. J. D. van Eekelen; Daniil Frumin; Herman Geuvers; Léon Gondelman; Robbert Krebbers; Marc Schoolderman; Sjaak Smetsers; Freek Verbeek; Benoît Viguier; Freek Wiedijk (CoRR, 2019)

A homotopy-theoretic model of function extensionality in the effective topos. - Daniil Frumin; Benno van den Berg (Math. Struct. Comput. Sci., 2019)

Compositional Non-Interference for Fine-Grained Concurrent Programs. - Dan Frumin; Robbert Krebbers; Lars Birkedal (SP, 2021)

ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. - Dan Frumin; Robbert Krebbers; Lars Birkedal (Log. Methods Comput. Sci., 2021)

Bicategories in univalent foundations. - Benedikt Ahrens; Dan Frumin; Marco Maggesi; Niccolò Veltri; Niels van der Weide (Math. Struct. Comput. Sci., 2021)

Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library - Coq Artefact. - Simon Friis Vindum; Dan Frumin; Lars Birkedal (Zenodo, 2021)

Coq development for "Mechanized Verification of a Fine-Grained Concurrent Queue from Meta's Folly Library". - Simon Friis Vindum; Dan Frumin; Lars Birkedal (Zenodo, 2021)

Semantic cut elimination for the logic of bunched implications, formalized in Coq. - Dan Frumin (CPP, 2022)

Mechanized verification of a fine-grained concurrent queue from meta's folly library. - Simon Friis Vindum; Dan Frumin; Lars Birkedal (CPP, 2022)

A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency. - Dan Frumin; Emanuele D'Osualdo; Bas van den Heuvel 001; Jorge A. Pérez 001 (Proc. ACM Program. Lang., 2022)

A Minimal Formulation of Session Types. - Alen Arslanagic; Jorge A. Pérez 001; Dan Frumin (CoRR, 2023)

The Interval Domain in Homotopy Type Theory. - Niels van der Weide; Dan Frumin (Logics and Type Systems in Theory and Practice, 2024)

Around Classical and Intuitionistic Linear Processes. - Juan C. Jaramillo; Dan Frumin; Jorge A. Pérez 001 (CONCUR, 2024)

Modular Denotational Semantics for Effects with Guarded Interaction Trees. - Dan Frumin; Amin Timany; Lars Birkedal (Proc. ACM Program. Lang., 2024)

Context-Dependent Effects in Guarded Interaction Trees. - Sergei Stepanenko; Emma Nardino; Dan Frumin; Amin Timany; Lars Birkedal (ESOP (2), 2025)

Context-Dependent Effects in Guarded Interaction Trees. - Sergei Stepanenko; Emma Nardino; Dan Frumin; Amin Timany; Lars Birkedal (Zenodo, 2025)

Context-Dependent Effects in Guarded Interaction Trees. - Sergei Stepanenko; Emma Nardino; Dan Frumin; Amin Timany; Lars Birkedal (Zenodo, 2025)