Publications

Sort by: Date | Author | Title

Timany, A. & Birkedal, L. (2019). Mechanized relational verification of concurrent programs with continuations. Proceedings of the ACM on Programming Languages , 3(ICFP), 1-28. Article 105. https://doi.org/10.1145/3341709

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

Bloemen, V., Duret-Lutz, A. & van de Pol, J. (2019). Model checking with generalized Rabin and Fin-less automata. International Journal on Software Tools for Technology Transfer, 21(3), 307-324. https://doi.org/10.1007/s10009-019-00508-4

Dijk, T. V., Meijer, J. & van de Pol, J. (2019). Multi-core On-The-Fly Saturation. In 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 (pp. 58-75). Springer. https://doi.org/10.1007/978-3-030-17465-1_4

Skorstengaard, L., Devriese, D. & Birkedal, L. (2019). Reasoning about a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. ACM Transactions on Programming Languages and Systems, 42(1), Article 5. https://doi.org/10.1145/3363519

Skorstengaard, L., Devriese, D. & Birkedal, L. (2019). Reasoning About a Machine with Local Capabilities: Provably Safe Stack and Return Pointer Management. A C M Transactions on Programming Languages and Systems, 41(4), Article 5. https://doi.org/10.1145/3363519

Nielsen, J. B. & Spitters, B. (2019). Smart Contract Interactions in Coq. (0 ed.) ArXiv.

Kordon, F., Leuschel, M., Pol, J. V. D. & Thierry-Mieg, Y. (2019). Software Architecture of Modern Model Checkers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): State of the Art and Perspectives (pp. 393-419). Springer. https://doi.org/10.1007/978-3-319-91908-9_20

Meijer, J. & van de Pol, J. (2019). Sound black-box checking in the LearnLib. Innovations in Systems and Software Engineering, 15(3-4), 267-287. https://doi.org/10.1007/s11334-019-00342-6

Penninckx, W., Timany, A. & Jacobs, B. (2019). Specifying i/o using abstract nested hoare triples in separation logic. In Proceedings of the 21st Workshop on Formal Techniques for Java-Like Programs, FTfJP 2019 - Co-located with ECOOP 2019 Article 5 Association for Computing Machinery. https://doi.org/10.1145/3340672.3341118

Pedersen, M. & Askarov, A. (2019). Static Enforcement of Security in Runtime Systems. In Proceedings - 2019 IEEE 32nd Computer Security Foundations Symposium, CSF 2019 (pp. 335-350). Article 8823712 IEEE. https://doi.org/10.1109/CSF.2019.00030

Skorstengaard, L., Devriese, D. & Birkedal, L. (2019). StkTokens: Enforcing Well-Bracketed Control Flow and Stack Encapsulation Using Linear Capabilities. Proceedings of the ACM on Programming Languages , 3(POPL), Article 19. https://doi.org/10.1145/3290332

Pol, J. V. D. & Meijer, J. (2019). Synchronous or Alternating? LTL Black-Box Checking of Mealy Machines by Combining the LearnLib and LTSmin. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): The What, the How, and the Why Not? (pp. 417-430). Springer. https://doi.org/10.1007/978-3-030-22348-9_24

Bidlingmaier, M. E., Faissole, F. & Spitters, B. (2019). Synthetic topology in Homotopy Type Theory for probabilistic programming. ArXiv.

Timany, A., Stefanesco, L., Krogh-Jespersen, M. & Birkedal, L. (2018). A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST. In Proceedings of the ACM on Programming Languages (Vol. 2, pp. 64:00-64:28). Association for Computing Machinery. https://doi.org/10.1145/3158152

Bizjak, A. & Birkedal, L. (2018). A Model of Guarded Recursion via Generalised Equilogical Spaces. Theoretical Computer Science, 722, 1-18. https://doi.org/10.1016/j.tcs.2018.02.012

Huang, D., Morrisett, G. & Spitters, B. (2018, Jun 20). An Application of Computable Distributions to the Semantics of Probabilistic Programs. Cornell University.

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.-Y. (2018, Jun 19). Computer-aided proofs for multiparty computation with active security. arxiv.org. Computer Security Foundations https://arxiv.org/abs/1806.07197

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

Timany, A. & Sozeau, M. (2018). Cumulative inductive types in coq. In H. Kirchner (Ed.), 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018 Article 29 Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.FSCD.2018.29

Licata, D. R., Orton, I., Pitts, A. M. & Spitters, B. (2018, Jul 1). Internal Universes in Models of Homotopy Type Theory. arxiv.org. https://arxiv.org/abs/1801.07664

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

Bizjak, A. & Birkedal, L. (2018). On Models of Higher-Order Separation Logic. Electronic Notes in Theoretical Computer Science, 336(4), 57-78. https://doi.org/10.1016/j.entcs.2018.03.016

Faissole, F. & Spitters, B. (2018). Preuves constructives de programmes probabilistes. In Journées Francophones des Langages Applicatifs

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

Frumin, D., Krebbers, R. & Birkedal, L. (2018). ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 (pp. 442-451). Association for Computing Machinery. https://doi.org/10.1145/3209108.3209174

Krogh-Jespersen, M., Svendsen, K. & Birkedal, L. (2017). A relational model of types-and-effects in higher-order concurrent separation logic. In POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages: POPL 2017 (pp. 218-231). Association for Computing Machinery. https://doi.org/10.1145/3009837.3009877

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

Pedersen, M. V. & Askarov, A. (2017). From Trash to Treasure: Timing-Sensitive Garbage Collection. In 2017 IEEE Symposium on Security and Privacy, SP 2017 - Proceedings (pp. 693-709). Article 7958605 IEEE Computer Society Press. https://doi.org/10.1109/SP.2017.64

Krebbers, R., Timany, A. & Birkedal, L. (2017). Interactive proofs in higher-order concurrent separation logic. In A. D. Gordon & G. Castagna (Eds.), Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017 (pp. 205-217). Association for Computing Machinery. https://doi.org/10.1145/3009837.3009855

Rijke, E., Shulman, M. & Spitters, B. (2017, Jun 27). Modalities in homotopy type theory. https://arxiv.org/abs/1706.07526

Bahr, P., Grathwohl, H. B. & Møgelberg, R. E. (2017). The clocks are ticking: No more delays! In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017 Article 8005097 IEEE. https://doi.org/10.1109/LICS.2017.8005097

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

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

Birkedal, L., Jaber, G., Sieczkowski, F. & Thamsborg, J. (2016). A Kripke logical relation for effect-based program transformations. Information and Computation, 249, 160-189. https://doi.org/10.1016/j.ic.2016.04.003

Spitters, B. (2016, Oct 17). Cubical sets and the topological topos. https://arxiv.org/pdf/1610.05270v1.pdf

Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A. (2016). Guarded cubical type theory. Abstract from 22nd International Conference on Types for Proofs and Programs, Novi Sad, Serbia. http://www.cs.au.dk/~spitters/TYPES16.pdf

Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A. (2016). Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In J.-M. Talbot & L. Regnier (Eds.), CSL 2016: 25th EACSL Annual Conference on Computer Science Logic (pp. 1 - 17)

Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A. (2016). Guarded Cubical Type Theory. https://arxiv.org/pdf/1611.09263v1.pdf

Bizjak, A., Grathwohl, H. B., Clouston, R., Møgelberg, R. E. & Birkedal, L. (2016). Guarded dependent type theory with coinductive types. In B. Jacobs & C. Löding (Eds.), Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016 (Vol. 9634, pp. 20-35). Springer VS. https://doi.org/10.1007/978-3-662-49630-5_2

Grathwohl, H. B. (2016). Guarded Recursive Type Theory. Department of Computer Science, Aarhus University.

Jung, R., Krebbers, R., Birkedal, L. & Dreyer, D. (2016). Higher-order ghost state. In E. Sumii (Ed.), ICFP 2016 Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (pp. 256-269). Association for Computing Machinery. https://doi.org/10.1145/2951913.2951943

Rijke, E. & Spitters, B. (2016). Homotopy type theory and the formalization of mathematics. Nieuw Archief voor Wiskunde , 5/17(3), 159 - 164. http://www.cs.au.dk/~spitters/naw5-2016-17-3-159.pdf

Birkedal, L. (2016). Preface. Electronic Notes in Theoretical Computer Science, 325, 1-2. https://doi.org/10.1016/j.entcs.2016.09.028

Devriese, D., Birkedal, L. & Piessens, F. (2016). Reasoning about object capabilities with logical relations and effect parametricity. In 2016 IEEE European Symposium on Security and Privacy, EURO S and P 2016 (pp. 147-162). Article 7467352 IEEE Press. https://doi.org/10.1109/EuroSP.2016.22

Clouston, R., Bizjak, A., Grathwohl, H. B. & Birkedal, L. (2016). The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science, 12(3), 1 - 39.

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

Displaying results 151 to 200 out of 336

Revised 17.04.2023

Sofia Hedegaard Rasmussen