Research output per year
Research output per year
- 15 results
Search results
-
2025
Context-Dependent Effects in Guarded Interaction Trees
Stepanenko, S., Nardino, E., Frumin, D., Timany, A. & Birkedal, L., 2025, Programming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Proceedings. Vafeiadis, V. (ed.). Springer Science and Business Media Deutschland GmbH, p. 286-313 28 p. (Lecture Notes in Computer Science; vol. 15695 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
Open AccessFile3 Downloads (Pure) -
2024
Around Classical and Intuitionistic Linear Processes
Jaramillo, J. C., Frumin, D. & Pérez, J. A., Sept-2024, 35th International Conference on Concurrency Theory, CONCUR 2024. Majumdar, R. & Silva, A. (eds.). Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 19 p. 30. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 311).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
Open AccessFile52 Downloads (Pure) -
Modular Denotational Semantics for Effects with Guarded Interaction Trees
Frumin, D., Timany, A. & Birkedal, L., 5-Jan-2024, In: Proceedings of the ACM on Programming Languages. 8, 30 p., 12.Research output: Contribution to journal › Article › Academic › peer-review
Open AccessFile7 Citations (Scopus)76 Downloads (Pure) -
The Interval Domain in Homotopy Type Theory
van der Weide, N. & Frumin, D., 22-May-2024, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Capretta, V., Krebbers, R. & Wiedijk, F. (eds.). Springer Science and Business Media Deutschland GmbH, p. 241-256 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14560 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review
Open AccessFile106 Downloads (Pure) -
2022
A bunch of sessions: a propositions-as-sessions interpretation of bunched implications in channel-based concurrency
Frumin, D., D'Osualdo, E., van den Heuvel, B. & Pérez, J. A., Oct-2022, In: Proceedings of the ACM on Programming Languages. 6, OOPSLA2, p. 841-869 29 p., 155.Research output: Contribution to journal › Article › Academic › peer-review
Open AccessFile4 Citations (Scopus)77 Downloads (Pure) -
Bicategories in univalent foundations
Ahrens, B., Frumin, D., Maggesi, M., Veltri, N. & Van Der Weide, N., 9-Mar-2022, In: Mathematical structures in computer science. 31, SI: 10, p. 1232–1269 38 p.Research output: Contribution to journal › Article › Academic › peer-review
Open AccessFile10 Citations (Scopus)97 Downloads (Pure) -
Mechanized Verification of a Fine-Grained Concurrent Queue from Meta s Folly Library
Vindum, S. F., Frumin, D. & Birkedal, L., 17-Jan-2022, CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022. Popescu, A. & Zdancewic, S. (eds.). Association for Computing Machinery, Inc, p. 100-115 16 p. (CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
Open AccessFile6 Citations (Scopus)154 Downloads (Pure) -
Semantic cut elimination for the logic of bunched implications, formalized in Coq
Frumin, D., 17-Jan-2022, CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022. Popescu, A. & Zdancewic, S. (eds.). Association for Computing Machinery, Inc, p. 291-306 16 p. (CPP 2022 - Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2022).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
Open AccessFile95 Downloads (Pure) -
2021
Compositional non-interference for fine-grained concurrent programs
Frumin, D., Krebbers, R. & Birkedal, L., May-2021, Proceedings - 2021 IEEE Symposium on Security and Privacy, SP 2021. Institute of Electrical and Electronics Engineers Inc., p. 1416-1433 18 p. (Proceedings - IEEE Symposium on Security and Privacy; vol. 2021-May).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
Open AccessFile11 Citations (Scopus)274 Downloads (Pure) -
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
Frumin, D., Krebbers, R. & Birkedal, L., 21-Aug-2021, In: Logical Methods in Computer Science. 17, 3, p. 9:1–9:59Research output: Contribution to journal › Article › Academic › peer-review
Open AccessFile14 Citations (Scopus)142 Downloads (Pure) -
2019
A homotopy-theoretic model of function extensionality in the effective topos
Frumin, D. & Van Den Berg, B., 1-Apr-2019, In: Mathematical structures in computer science. 29, 4, p. 588-614 27 p., 00014.Research output: Contribution to journal › Article › Academic › peer-review
5 Citations (Scopus) -
Bicategories in univalent foundations
Ahrens, B., Frumin, D., Maggesi, M. & van der Weide, N., 1-Jun-2019, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019. Geuvers, H. & Geuvers, H. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 17 p. 5. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 131).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
Open Access7 Citations (Scopus) -
Semi-automated Reasoning About Non-determinism in C Expressions
Frumin, D., Gondelman, L. & Krebbers, R., 2019, Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Caires, L. (ed.). Springer, p. 60-87 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11423 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
Open Access5 Citations (Scopus) -
2018
Finite sets in homotopy type theory
Frumin, D., Gondelman, L., Geuvers, H. & Van Der Weide, N., 8-Jan-2018, CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. Felty, A. & Andronick, J. (eds.). Association for Computing Machinery, Inc, p. 201-214 14 p. (CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018; vol. 2018-January).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
18 Citations (Scopus) -
ReLoC: A mechanised relational logic for fine-grained concurrency
Frumin, D., Krebbers, R. & Birkedal, L., 9-Jul-2018, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Institute of Electrical and Electronics Engineers Inc., p. 442-451 10 p. (Proceedings - Symposium on Logic in Computer Science).Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review
43 Citations (Scopus)