Hammond, A.
, Liu, Z., Pérami, T., Sewell, P.
, Birkedal, L. & Pichon-Pharabod, J. (2024).
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic.
Proceedings of the ACM on Programming Languages ,
8, 604-637. Article 21.
https://doi.org/10.1145/3632863
Haagh, H., Karbyshev, A., Oechsner, S.
, Spitters, B. & Strub, P. (2018).
Computer-Aided Proofs for Multiparty Computation with Active Security. In
Proceedings - IEEE 31st Computer Security Foundations Symposium, CSF 2018 (Vol. 2018, pp. 119-131). Article 8429300 IEEE.
https://doi.org/10.1109/CSF.2018.00016
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
Gregersen, S. O., Aguirre, A., Haselwarter, P. G., Tassarotti, J.
& Birkedal, L. (2024).
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic.
Proceedings of the ACM on Programming Languages ,
8(POPL), Article 26.
https://doi.org/10.1145/3632868
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
Gondelman, L., Gregersen, S. O., Nieto, A., Timany, A. & Birkedal, L. (2021).
Distributed causal memory: Modular specification and verification in higher-order distributed separation logic.
Proceedings of the ACM on Programming Languages ,
5(POPL), Article 42.
https://doi.org/10.1145/3434323
Gondelman, L., Hinrichsen, J. K., Pereira, M.
, Timany, A. & Birkedal, L. (2023).
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols.
Proceedings of the ACM on Programming Languages ,
7(ICFP), 847-877. Article 217.
https://doi.org/10.1145/3607859
Giarrusso, P. G., Stefanesco, L.
, Timany, A., Birkedal, L. & Krebbers, R. (2020).
Scala step-by-step: Soundness for DOT with step-indexed logical relations in Iris.
Proceedings of the ACM on Programming Languages ,
4(ICFP), Article 114.
https://doi.org/10.1145/3408996
Georges, A. L., Guéneau, A., Van Strydonck, T.
, Timany, A., Trieu, A., Huyghebaert, S., Devriese, D.
& Birkedal, L. (2021).
Efficient and provable local capability revocation using uninitialized capabilities.
Proceedings of the ACM on Programming Languages ,
5(POPL), Article 6.
https://doi.org/10.1145/3434287
Georges, A. L., Guéneau, A., Van Strydonck, T.
, Timany, A., Trieu, A., Devriese, D.
& Birkedal, L. (2021).
Cap’ ou pas cap’ ?: Preuve de programmes pour une machine à capacités en présence de code inconnu. In
Journées Francophones des Langages Applicatifs 2021 Institut de Recherche en Informatique Fondamentale.
https://researchportal.vub.be/en/publications/cap-ou-pas-cap-preuve-de-programmes-pour-une-machine-%C3%A0-capacit%C3%A9s-
Georges, A. L., Guéneau, A., Van Strydonck, T.
, Timany, A., Trieu, A., Devriese, D.
& Birkedal, L. (2024).
Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code.
Journal of the ACM,
71(1), Article 3.
https://doi.org/10.1145/3623510
Garavel, H., ter Beek, M. H.
& van de Pol, J. (2020).
The 2020 Expert Survey on Formal Methods. In M. H. ter Beek & D. Nickovic (Eds.),
Formal Methods for Industrial Critical Systems - 25th International Conference, FMICS 2020, Proceedings: FMICS 2020, Vienna, Austria, September 2-3, 2020, Proceedings (pp. 3-69). Springer.
https://doi.org/10.1007/978-3-030-58298-2_1
Dreyer, D., Neis, G.
& Birkedal, L. (2010).
The impact of higher-order state and control effects on local relational reasoning. In S. Weirich & P. Hudak (Eds.),
Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010 (pp. 143-156). Association for Computing Machinery.
https://doi.org/http://doi.acm.org/10.1145/1863543.1863566
Dreyer, D., Neis, G., Rossberg, A.
& Birkedal, L. (2010).
A relational modal logic for higher-order stateful ADTs. In M. Hermenegildo & J. Palsberg (Eds.),
Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010 (pp. 185-198). Association for Computing Machinery.
https://doi.org/http://doi.acm.org/10.1145/1706299.1706323
Dodds, M., Jagannathan, S., Parkinson, M. J., Svendsen, K.
& Birkedal, L. (2016).
Verifying custom synchronisation constructs using higher-order separation logic.
ACM Transactions on Programming Languages and Systems,
38/2(2), 4:1 - 4:72. Article 4.
https://doi.org/10.1145/2818638
Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K. J. A.
& Birkedal, L. (2017).
Caper: Automatic Verification for Fine-Grained Concurrency. In H. Yang (Ed.),
Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings: 26th European Symposium on Programming, ESOP 2017 (Vol. 10201, pp. 420-447). Springer VS.
https://doi.org/10.1007/978-3-662-54434-1_16
Clouston, R., Bizjak, A.
, Grathwohl, H. B. & Birkedal, L. (2015).
Programming and reasoning with guarded recursion for coinductive types. In A. Pitts (Ed.),
Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (pp. 305-316). Springer VS.
https://doi.org/10.1007/978-3-662-46678-0_26