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
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
Nielsen, J. B.
& Spitters, B. (2020).
Smart contract interactions in coq. In E. Sekerinski, N. Moreira, J. N. Oliveira, D. Ratiu, R. Guidotti, M. Farrell, M. Luckcuck, D. Marmsoler, J. Campos, T. Astarte, L. Gonnord, A. Cerone, L. Couto, B. Dongol, M. Kutrib, P. Monteiro & D. Delmas (Eds.),
Formal Methods- FM 2019 International Workshops - Revised Selected Papers (pp. 380-391). Springer.
https://doi.org/10.1007/978-3-030-54994-7_29
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
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
Birkedal, L., Bizjak, A., Clouston, R.
, Grathwohl, H. B., Spitters, B. & Vezzosi, A. (2019).
Guarded Cubical Type Theory.
Journal of Automated Reasoning,
63(2), 211-253.
https://doi.org/10.1007/s10817-018-9471-7,
https://doi.org/10.1007/s10817-018-9471-7
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
Karbyshev, A., Svendsen, K.
, Askarov, A. & Birkedal, L. (2018).
Compositional Non-interference for Concurrent Programs via Separation and Framing. In L. Bauer & R. Küsters (Eds.),
Principles of Security and Trust - 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (Vol. 10804, pp. 53-78). Springer VS.
https://doi.org/10.1007/978-3-319-89722-6_3
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
JUNG, RALF., KREBBERS, ROBBERT., JOURDAN, JACQUES.-HENRI., BIZJAK, ALEŠ.
, BIRKEDAL, LARS. & DREYER, DEREK. (2018).
Iris from the ground up: A modular foundation for higher-order concurrent separation logic.
Journal of Functional Programming,
28, 1-73. Article e20.
https://doi.org/10.1017/S0956796818000151
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
Skorstengaard, L., Devriese, D.
& Birkedal, L. (2018).
Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. In A. Ahmed (Ed.),
Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (Vol. 10801, pp. 475-501). Springer VS.
https://doi.org/10.1007/978-3-319-89884-1_17
Aguirre, A., Barthe, G.
, Birkedal, L., Bizjak, A., Gaboardi, M. & Garg, D. (2018).
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In A. Ahmed (Ed.),
Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (pp. 214-241). Springer VS.
https://doi.org/10.1007/978-3-319-89884-1_8
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