Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P.
& Birkedal, L. (2008).
Ynot: Depent Types for Imperative Programs. In
International Conference on Functional Programming: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, (Vol. session 9, pp. 229-240). Association for Computing Machinery.
Liu, Z., Stepanenko, S., Pichon-Pharabod, J., Timany, A., Askarov, A. & Birkedal, L. (2023).
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A.
Proceedings of the ACM on Programming Languages ,
7, 1438-1462.
https://doi.org/10.1145/3591279
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
Bengtson, J., Jensen, J. B., Sieczkowski, F.
& Birkedal, L. (2011).
Verifying object-oriented programs with higher-order separation logic in Coq. In M. V. Eekelen , H. Geuvers, J. Schmaltz & F. Wiedijk (Eds.),
Interactive Theorem Proving: Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings (pp. 22-38). Springer.
https://doi.org/10.1007/978-3-642-22863-6_5
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
Hansen, S. T., Gomes, C., Palmieri, M., Thule, C.
, van de Pol, J. & Woodcock, J. (2021).
Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps. In A. L. Lafuente & A. Mavridou (Eds.),
Formal Methods for Industrial Critical Systems (pp. 3-20). Springer.
https://doi.org/10.1007/978-3-030-85248-1_1
Hansen, S. T., Thule, C.
, Gomes, C., van de Pol, J., Palmieri, M., Inci, E. O., Madsen, F., Alfonso, J., Castellanos, J. Á. & Rodriguez, J. M. (2022).
Verification and synthesis of co-simulation algorithms subject to algebraic loops and adaptive steps.
International Journal on Software Tools for Technology Transfer,
24(6), 999-1024.
https://doi.org/10.1007/s10009-022-00686-8
Spies, S., Gäher, L.
, Gratzer, D., Tassarotti, J., Krebbers, R., Dreyer, D.
& Birkedal, L. (2021).
Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic. In S. N. Freund & E. Yahav (Eds.),
PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 80-95). Association for Computing Machinery.
https://doi.org/10.1145/3453483.3454031
Birkedal, L., Dinsdale-Young, T., Guéneau, A., Jaber, G., Svendsen, K. & Tzevelekos, N. (2021).
Theorems for free from separation logic specifications.
Proceedings of the ACM on Programming Languages ,
5(ICFP), Article 81.
https://doi.org/10.1145/3473586
Haselwarter, P. G., Hvass, B. S., Hansen, L. L., Winterhalter, T., Hriţcu, C.
& Spitters, B. (2024).
The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography. In A. Timany, D. Traytel, B. Pientka & S. Blazy (Eds.),
CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 30-44). Association for Computing Machinery.
https://doi.org/10.1145/3636501.3636961
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
Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M.
& Spitters, B. (2017).
The HoTT Library: A Formalization of Homotopy Type Theory in Coq. In Y. Bertot & V. Vafeiadis (Eds.),
CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017: CPP 2017 (pp. 164-172). Association for Computing Machinery.
https://doi.org/10.1145/3018610.3018615
Bauer, A., Gross, J., Lumsdaine, P. L., Shulman, M., Sozeau, M.
& Spitters, B. (2016).
The HoTT Library: A formalization of homotopy type theory in Coq.
http://arxiv.org/abs/1610.04591
Jung, R., Lepigre, R., Parthasarathy, G., Rapoport, M.
, Timany, A., Dreyer, D. & Jacobs, B. (2020).
The future is ours: prophecy variables in separation logic.
Proceedings of the ACM on Programming Languages ,
4(POPL), Article 45.
https://doi.org/10.1145/3371113
Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.-H., Dreyer, D.
& Birkedal, L. (2017).
The Essence of Higher-Order Concurrent Separation Logic. 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 (pp. 696-723). Springer VS.
https://doi.org/10.1007/978-3-662-54434-1_26
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