21 citations · 32 across the 9 of their papers we have counts for
10 papers
Context-Dependent Effects and Concurrency in Guarded Interaction Trees
Sergei Stepanenko, Emma Nardino, Virgil Marionneau +3
Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Rocq. We present an extension of…
Modular Denotational Semantics for Effects with Guarded Interaction Trees
Dan Frumin, Amin Timany, Lars Birkedal
We present guarded interaction trees -- a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq, inspired by domain…
A Minimal Formulation of Session Types: The Sessions of Trios in Concert
Alen Arslanagić, Jorge A. Pérez, Dan Frumin
Session types are a type-based approach to the verification of message-passing programs. They specify communication structures essential to enforcing program correctness; by relyin…
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 +1
The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical fo…
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
Dan Frumin
The logic of bunched implications (BI) is a substructural logic that forms the backbone of separation logic, the much studied logic for reasoning about heap-manipulating programs.…
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
Dan Frumin, Robbert Krebbers, Lars Birkedal
We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive t…
Compositional Non-Interference for Fine-Grained Concurrent Programs
Dan Frumin, Robbert Krebbers, Lars Birkedal
Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing no…
A benchmark for C program verification
Marko van Eekelen, Daniil Frumin, Herman Geuvers +7
We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verificati…
Bicategories in Univalent Foundations
Benedikt Ahrens, Dan Frumin, Marco Maggesi +2
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent…
A homotopy-theoretic model of function extensionality in the effective topos
Daniil Frumin, Benno van den Berg
We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance.…