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
Seisenberger, M., ter Beek, M. H., Fan, X., Ferrari, A., Haxthausen, A. E., James, P., Lawrence, A., Luttik, B.
, van de Pol, J. & Wimmer, S. (2022).
Safe and Secure Future AI-Driven Railway Technologies: Challenges for Formal Methods in Railway. In T. Margaria & B. Steffen (Eds.),
Leveraging Applications of Formal Methods, Verification and Validation. Practice - 11th International Symposium, ISoLA 2022, Proceedings (pp. 246-268). Springer.
https://doi.org/10.1007/978-3-031-19762-8_20
Schwinghammer, J.
, Birkedal, L. & Støvring, K. (2011).
A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces. In M. Hofmann (Ed.),
Foundations of Software Science and Computational Structures: 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26–April 3, 2011. Proceedings (pp. 305-319). Springer.
https://doi.org/10.1007/978-3-642-19805-2_21
Schwinghammer, J.
, Birkedal, L., Pottier, F., Reus, B., Støvring, K. & Yang, H. (2013).
A step-indexed Kripke model of hidden state.
Mathematical Structures in Computer Science,
23(1), 1-54.
https://doi.org/10.1017/S0960129512000035
Schwinghammer, J., Yang, H.
, Birkedal, L., Pottier, F. & Reus, B. (2010).
A semantic foundation for hidden state. In L. Ong (Ed.),
Foundations of Software Science and Computational Structures: 13th International Conference, FOSSACS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, March 20-28, 2010. Proceedings (pp. 2-17). Springer.
https://doi.org/10.1007/978-3-642-12032-9_2
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
Schivo, S., Khurana, S., Govindaraj, K., Scholma, J., Kerkhofs, J., Zhong, L., Huang, X.
, van de Pol, J., Langerak, R., van Wijnen, A. J., Geris, L., Karperien, M. & Post, J. N. (2020).
ECHO, the executable CHOndrocyte: A computational model to study articular chondrocytes in health and disease.
Cellular Signalling,
68, Article 109471.
https://doi.org/10.1016/j.cellsig.2019.109471
Rao, X.
, Georges, A. L., Legoupil, M., Watt, C.
, Pichon-Pharabod, J., Gardner, P.
& Birkedal, L. (2023).
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs.
Proceedings of the ACM on Programming Languages ,
7, Article 151.
https://doi.org/10.1145/3591265
Pientka, B., Blazy, S., Traytel, D.
& Timany, A. (2024).
Welcome from the Chairs. In
CPP 2024 - Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with: POPL 2024 (pp. iii-iv)
Oortwijn, W., Huisman, M., Joosten, S. J. C.
& van de Pol, J. (2020).
Automated verification of parallel nested DFS. In A. Biere & D. Parker (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems- 26th International Conference, TACAS 2020, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Proceedings, Part I (pp. 247-265). Springer.
https://doi.org/10.1007/978-3-030-45190-5_14
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
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
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
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.
Nanevski, A., Ahmed, A., Morrisett, G.
& Birkedal, L. (2007).
Abstract predicates and mutable ADTs in hoare type theory. In R. D. Nicola (Ed.),
Programming Languages and Systems: 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24 - April 1, 2007. Proceedings (pp. 189-204). Springer VS.
https://doi.org/10.1007/978-3-540-71316-6_14