Follow
Dan Frumin
Title
Cited by
Cited by
Year
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency
D Frumin, R Krebbers, L Birkedal
LICS, 442-451, 2018
692018
Bicategories in univalent foundations
B Ahrens, D Frumin, M Maggesi, N Veltri, N Van Der Weide
Mathematical Structures in Computer Science 31 (10), 1232-1269, 2021
302021
Finite sets in homotopy type theory
D Frumin, H Geuvers, L Gondelman, N van der Weide
Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018
272018
Branching processes of conservative nested Petri nets
D Frumin, I Lomazova
VPT 2014. Second International Workshop on Verification and Program …, 2014
242014
Compositional Non-Interference for Fine-Grained Concurrent Programs
D Frumin, R Krebbers, L Birkedal
Security & Privacy (Oakland) 1, 1416-1433, 2021
232021
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
D Frumin, R Krebbers, L Birkedal
Logical Methods in Computer Science 17 (3), 2021
20*2021
A homotopy-theoretic model of function extensionality in the effective topos
D Frumin, B van den Berg
Mathematical Structures in Computer Science 29 (4), 588-614, 2019
18*2019
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly Library
SF Vindum, D Frumin, L Birkedal
15*2022
Semi-Automated Reasoning About Non-Determinism in C Expressions
D Frumin, L Gondelman, R Krebbers
ESOP, 2019
102019
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
D Frumin, E D’Osualdo, B van den Heuvel, JA Pérez
Proceedings of the ACM on Programming Languages 6 (OOPSLA2), 841-869, 2022
52022
A Minimal Formulation of Session Types
A Arslanagić, JA Pérez, D Frumin
arXiv preprint arXiv:2301.05301, 2023
32023
Modular Denotational Semantics for Effects with Guarded Interaction Trees
D Frumin, A Timany, L Birkedal
Proceedings of the ACM on Programming Languages 8 (POPL), 332-361, 2024
22024
Semantic cut elimination for the logic of bunched implications, formalized in Coq
D Frumin
Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022
22022
Logic and homotopy in the category of assemblies
D Frumin
http://cs.ru.nl/~dfrumin/pdf/realiz.pdf, 2016
12016
Semantic Cut Elimination for the Logic of Bunched Implications and Structural Extensions, Formalized in Coq
D Frumin
2022
Concurrent Separation Logics for Safety, Refinement, and Security.
D Frumin
Radboud University Nijmegen, 2021
2021
Concurrent Separation Logics for Safety, Refinement, and Security
D Frumin
[Sl: sn], 2021
2021
1-Types versus Groupoids
N van der Weide, D Frumin, H Geuvers
TYPES 2018, 86, 2018
2018
A calculus for logical refinements in separation logic
D Frumin, R Krebbers
CoqPL, 2018
2018
Presheaf models for concurrency
D Frumin
2016
The system can't perform the operation now. Try again later.
Articles 1–20