Følg
Dan Frumin
Dan Frumin
University of Groningen
Verifisert e-postadresse på rug.nl - Startside
Tittel
Sitert av
Sitert av
År
ReLoC: A mechanised relational logic for fine-grained concurrency
D Frumin, R Krebbers, L Birkedal
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018
762018
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, 2021
38*2021
Finite sets in homotopy type theory
D Frumin, H Geuvers, L Gondelman, N Weide
Proceedings of the 7th ACM SIGPLAN International Conference on Certified …, 2018
322018
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
312021
Compositional non-interference for fine-grained concurrent programs
D Frumin, R Krebbers, L Birkedal
2021 IEEE Symposium on Security and Privacy (SP), 1416-1433, 2021
292021
Branching Processes of Conservative Nested Petri Nets.
D Frumin, IA Lomazova
VPT@ CAV 19, 35, 2014
242014
Mechanized verification of a fine-grained concurrent queue from meta’s folly library
SF Vindum, D Frumin, L Birkedal
Proceedings of the 11th ACM SIGPLAN International Conference on Certified …, 2022
19*2022
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
17*2019
Semi-automated Reasoning About Non-determinism in C Expressions.
D Frumin, L Gondelman, R Krebbers
ESOP, 60-87, 2019
132019
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
102022
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
82024
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
62022
A minimal formulation of session types
A Arslanagić, JA Pérez, D Frumin
arXiv preprint arXiv:2301.05301, 2023
32023
Context-Dependent Effects in Guarded Interaction Trees
S Stepanenko, E Nardino, D Frumin, A Timany, L Birkedal
ESOP, 2025
2025
Around Classical and Intuitionistic Linear Processes
JC Jaramillo, D Frumin, JA Pérez
arXiv preprint arXiv:2407.06391, 2024
2024
The Interval Domain in Homotopy Type Theory
N van der Weide, D Frumin
Logics and Type Systems in Theory and Practice: Essays Dedicated to Herman …, 2024
2024
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. Associated Coq mechanization
D Frumin
Zenodo, 2021
2021
RELOC RELOADED: TECHNICAL APPENDIX
DAN FRUMIN, R KREBBERS, L BIRKEDAL
2020
1-Types versus Groupoids
N van der Weide, D Frumin, H Geuvers
TYPES 2018, 86, 2018
2018
Systemet kan ikke utføre handlingen. Prøv på nytt senere.
Artikler 1–20