Svendsen, K.
, Birkedal, L. & Nanevski, A. (2011).
Partiality, State, and Dependent Types. In
Proceedings of Typed LAmbda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011 (Vol. LNCS 6690, pp. 198-212). Springer.
Schwinghammer, J.
, Birkedal, L., Reus, B. & Yang, H. (2009).
Nested hoare triples and frame rules for higher-order store. In E. Grädel & R. Kahle (Eds.),
Computer Science Logic: 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings (pp. 440-454). Springer.
https://doi.org/10.1007/978-3-642-04027-6_32
Krebbers, R., Jourdan, J.-H., Jung, R., Tassarotti, J., Kaiser, J.-O.
, Timany, A., Charguéraud, A. & Dreyer, D. (2018).
MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
PACMPL,
2(ICFP), 77:1-77:30. Article 3236772.
https://doi.org/10.1145/3236772
Sieczkowski, F., Bizjak, A.
& Birkedal, L. (2015).
ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. In C. Urban & X. Zhang (Eds.),
Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (pp. 375-390). Springer.
https://doi.org/10.1007/978-3-319-22102-1_25
Nieto, A., Daby-Seesaram, A.
, Gondelman, L., Timany, A. & Birkedal, L. (2023).
Modular Verification of State-Based CRDTs in Separation Logic. In K. Ali & G. Salvaneschi (Eds.),
37th European Conference on Object-Oriented Programming, ECOOP 2023 Article 22 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing.
https://doi.org/10.4230/LIPIcs.ECOOP.2023.22
Nieto, A., Gondelman, L., Reynaud, A.
, Timany, A. & Birkedal, L. (2022).
Modular verification of op-based CRDTs in separation logic.
Proceedings of the ACM on Programming Languages,
6(OOPSLA2), 1788-1816. Article 188.
https://doi.org/10.1145/3563351
Svendsen, K.
, Birkedal, L. & Parkinson, M. (2013).
Modular Reasoning about Separation of Concurrent Data Structures. In M. Felleisen & P. Gardner (Eds.),
Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (pp. 169-188 ). Springer.
https://doi.org/10.1007/978-3-642-37036-6_11
Gratzer, D., Cavallo, E., Kavvos, G. A., Guatto, A.
& Birkedal, L. (2022).
Modalities and Parametric Adjoints.
ACM Transactions on Computational Logic,
23(3), Article 18.
https://doi.org/10.1145/3514241
Birkedal, L., Clouston, R., Mannaa, B., Ejlers Møgelberg, R., Pitts, A. M.
& Spitters, B. (2020).
Modal dependent type theory and dependent right adjoints.
Mathematical Structures in Computer Science,
30(2), 118-138.
https://doi.org/10.1017/S0960129519000197
André, É., Bloemen, V., Petrucci, L.
& Pol, J. V. D. (2019).
Minimal-Time Synthesis for Parametric Timed Automata. In L. Zhang & T. Vojnar (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings (Vol. II, pp. 211-228). Springer.
https://doi.org/10.1007/978-3-030-17465-1_12
Guéneau, A., Hostert, J., Spies, S., Sammler, M.
, Birkedal, L. & Dreyer, D. (2023).
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C.
Proceedings of the ACM on Programming Languages ,
7(OOPSLA2), 716-744. Article 247.
https://doi.org/10.1145/3622823