21 citations · 32 across the 9 of their papers we have counts for
6 papers · 1 filter
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…
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 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.…