Publications

Sort by: Date | Author | Title

Svendsen, K., Sieczkowski, F. & Birkedal, L. (2016). Transfinite step-indexing: Decoupling concrete and logical steps. In P. Thiemann (Ed.), Programming Languages and Systems (Vol. 9632, pp. 727-751). Springer VS. https://doi.org/10.1007/978-3-662-49498-1_28

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

Paviotti, M., Møgelberg, R. E. & Birkedal, L. (2015). A model of PCF in guarded type theory. Electronic Notes in Theoretical Computer Science, 319, 333–349. https://doi.org/10.1016/j.entcs.2015.12.020

Sieczkowski, F., Svendsen, K., Birkedal, L. & Pichon-Pharabod, J. (2015). A separation logic for fictional sequential consistency. In J. Vitek (Ed.), Programming Languages and Systems : 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 (pp. 736-761). Springer. https://doi.org/10.1007/978-3-662-46669-8_30

Askarov, A., Moore, S., Dimoulas, C. & Chong, S. (2015). Cryptographic Enforcement of Language-Based Information Erasure. In L. Viganò (Ed.), 28th IEEE Computer Security Foundations Symposium CSF 2015 : Proceedings (pp. 334-348). IEEE Computer Society Press. https://doi.org/10.1109/CSF.2015.30

Spitters, B. (2015). Cubical sets as a classifying topos. Abstract from 21st International Conference on Types for Proofs and Programs, , Tallinn, Estonia.

Bizjak, A., Grathwohl, H. B., Clouston, R., Birkedal, L. & Møgelberg, R. E. (2015). Guarded dependent type theory with coinductive types. In Foundations of Software Science and Computation Structures Springer. https://doi.org/10.1007/978-3-662-49630-5_2

Askarov, A., Chong, S. & Mantel, H. A. (2015). Hybrid Monitors for Concurrent Noninterference. In L. Viganò (Ed.), 28th IEEE Computer Security Foundations Symposium CSF 2015 : Proceedings (pp. 137 - 151). IEEE Computer Society Press. https://doi.org/10.1109/CSF.2015.17

Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L. & Dreyer, D. (2015). Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In S. Rajamani (Ed.), Conference Record of the Annual ACM Symposium on Principles of Programming Languages (pp. 637-650). Association for Computing Machinery. https://doi.org/10.1145/2676726.2676980

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

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

Devriese, D., Piessens, F. & Birkedal, L. (2015). Reasoning about Object Capabilities with Logical Relations and Effect Parametricity: Technical Report including Proofs and Details. Association for Computing Machinery. http://cs.au.dk/~birke/papers/object-capabilities-tr.pdf

Bizjak, A. & Birkedal, L. (2015). Step-indexed logical relations for probability. 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. 279-294 ). Springer VS. https://doi.org/10.1007/978-3-662-46678-0_18

Bizjak, A., Birkedal, L. & Miculan, M. (2014). A model of countable nondeterminism in guarded type theory. In G. Dowek (Ed.), Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (pp. 108-123). Springer VS. https://doi.org/10.1007/978-3-319-08918-8_8

Spitters, B., Vickers, S. & Wolters, S. (2014). Gelfand spectra in Grothendieck toposes using geometric mathematics. Electronic Proceedings in Theoretical Computer Science, EPTCS, 158, 77-107. https://doi.org/10.4204/EPTCS.158.7

Svendsen, K. & Birkedal, L. (2014). Impredicative concurrent abstract predicates. In Z. Shao (Ed.), Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (pp. 149-168 ). Springer. https://doi.org/10.1007/978-3-642-54833-8_9

Birkedal, L. (2014). Modular reasoning about concurrent higher-order imperative programs. Abstract from ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, United States. https://doi.org/10.1145/2535838.2537849

Damgaard, T. C., Glenstrup, A. J., Birkedal, L. & Milner, R. (2013). An inductive characterization of matching in binding bigraphs. Formal Aspects of Computing, 25(2), 257-288. https://doi.org/10.1007/s00165-011-0184-5

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

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Higher-order Concurrent Abstract Predicates.

Birkedal, L. & Mogelberg, R. E. (2013). Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. Annual Symposium on Logic in Computer Science, 213-222. https://doi.org/10.1109/LICS.2013.27

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Joins: A case study in modular specification of a concurrent reentrant higher-order library. In G. Castagna (Ed.), 27th European Conference on Object-Oriented Programming, ECOOP 2013; Montpellier; France (pp. 327-351). Springer. https://doi.org/10.1007/978-3-642-39038-8_14

Turon, A. J., Thamsborg, J., Ahmed, A., Birkedal, L. & Dreyer, D. (2013). Logical relations for fine-grained concurrency. In POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 343-356). Association for Computing Machinery. https://doi.org/10.1145/2429069.2429111

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Modular Reasoning about Separation of Concurrent Data Structures. In M. Felleisen & P. Gardner (Eds.), Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (pp. 169-188 ). Springer. https://doi.org/10.1007/978-3-642-37036-6_11

Birkedal, L., Bizjak, A. & Schwinghamme, J. (2013). Step-Indexed Relational Reasoning for Countable Nondeterminism. Logical Methods in Computer Science, 9(4), Article 4. https://doi.org/10.2168/LMCS-9(4:4)2013

Makarov, E. & Spitters, B. (2013). The Picard algorithm for ordinary differential equations in Coq. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings (pp. 463-468) https://doi.org/10.1007/978-3-642-39634-2_34

Krebbers, R. & Spitters, B. (2013). Type classes for efficient exact real arithmetic in CoQ. Logical Methods in Computer Science, 9(1). https://doi.org/10.2168/LMCS-9(1:01)2013

Turon, A., Dreyer , D. & Birkedal, L. (2013). Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In G. Morrisett & T. Uustalu (Eds.), Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13 (pp. 377-390 ). Association for Computing Machinery. https://doi.org/10.1145/2500365.2500600

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Verification of the Joins Library in Higher-Order Separation Logic. http://www.itu.dk/people/kasv/joins-tr.pdf

Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M. & Yang, H. (2013). Views: Compositional reasoning for concurrent programs. In R. Giacobazzi & R. Cousot (Eds.), POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages : Proceedings (pp. 287-299). Association for Computing Machinery. https://doi.org/10.1145/2429069.2429104

Birkedal, L., Sieczkowski, F. & Thamsborg, J. J. (2012). A Concurrent Logical Relation. In P. Cégielski & A. Durand (Eds.), Computer Science Logic 2012: 26th International Workshop. 21th Annual Conference of the EACSL. CSL’12, September 3–6, 2012, Fontainebleau, Franc Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2012.107

Birkedal, L., Støvring, K. & Thamsborg, J. (2012). A relational realizability model for higher-order stateful. Journal of Logic and Algebraic Programming, 81(4), 491-521. http://ac.els-cdn.com.ez.statsbiblioteket.dk:2048/S1567832612000203/1-s2.0-S1567832612000203-main.pdf?_tid=fb853fd6-00fa-11e4-a19b-00000aab0f6b&acdnat=1404204049_088283a10b310a3f6cd3280168eb7093

Heunen, C., Landsman, N. P. & Spitters, B. (2012). Bohrification of operator algebras and quantum logic. Synthese, 186(3), 719-752. https://doi.org/10.1007/s11229-011-9918-4

Bengtson, J., Jensen, J. B. & Birkedal, L. (2012). Charge! A framework for higher-order separation logic in Coq. In L. Beringer & A. Felty (Eds.), Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings (Vol. 7406, pp. 315-331). Springer VS. https://doi.org/10.1007/978-3-642-32347-8_21

Jensen, J. B. & Birkedal, L. (2012). Fictional Separation Logic. In H. Seidl (Ed.), Lecture Notes in Computer Science: 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings (Vol. 7211, pp. 377-396). Springer.

Birkedal, L., Møgelberg, R. E., Schwinghammer, J. & Støvring, K. (2012). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science, 8(4). https://doi.org/10.2168/LMCS-8(4:1)2012

Mehnert, H., Sieczkowski, F., Birkedal, L. & Sestoft, P. (2012). Formalized verification of snapshotable trees: Separation and sharing. In R. Joshi, P. Müller & A. Podelski (Eds.), Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings (pp. 179-195). Springer. https://doi.org/10.1007/978-3-642-27705-4_15

Birkedal, L. (2012). Foundations of Software Science and Computational Structures: 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. Springer. Lecture Notes in Computer Science Vol. 7213 https://doi.org/10.1007/978-3-642-28729-9

Dreyer, D., Neis, G. & Birkedal, L. (2012). The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming, 22(4-5 special issue), 477-528. https://doi.org/10.1017/S0956796812000287

Spitters, B. (2012). The Space of Measurement Outcomes as a Spectral Invariant for Non-Commutative Algebras. Foundations of Physics, 42(7), 896-908. https://doi.org/10.1007/s10701-011-9619-3

Thamsborg, J. J., Birkedal, L. & Yang, H. (2012). Two for the Price of One: Lifting Separation Logic Assertions. Logical Methods in Computer Science, 8(3).

Thamsborg, J. J. & Birkedal, L. (2011). A Kripke Logical Relation for Effect-Based Program Transformations. In ICFP 11. Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (pp. 445-456). Association for Computing Machinery. https://doi.org/10.1145/2034574.2034831

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

Buisse, A., Birkedal, L. & Støvring, K. (2011). A Step-Indexed Kripke Model of Separation Logic for Storable Locks. Electronic Notes in Theoretical Computer Science, 276. https://doi.org/10.1016/j.entcs.2011.09.018

Krebbers, R. & Spitters, B. (2011). Computer certified efficient exact reals in Coq. In Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011 and 10th International Conference, MKM 2011, Proceedings (pp. 90-106) https://doi.org/10.1007/978-3-642-22673-1_7

Birkedal, L., Møgelberg, R. E., Støvring, K. & schwinghammer, J. (2011). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Annual Symposium on Logic in Computer Science, 55-64. https://doi.org/10.1109/LICS.2011.16

Dreyer, D., Ahmed, A. & Birkedal, L. (2011). Logical Step-Indexed Logical Relations. Logical Methods in Computer Science, 7(2:16). https://doi.org/10.2168/LMCS-7(2:16)2011

Jensen, J. B., Birkedal, L. & Sestoft, P. (2011). Modular Verification of Linked Lists with Views via Separation Logic. Journal of Object Technology, 10(1), 21-40. https://doi.org/10.5381/jot.2011.10.1.a2

Schwinghammer, J., Birkedal, L., Reus, B. & Yang, H. (2011). Nested Hoare Triples and Frame Rules for Higher-Order Store. Logical Methods in Computer Science, 7(3:21), 440-454. https://doi.org/10.2168/LMCS-7(3:21)2011

Svendsen, K., Birkedal, L. & Nanevski, A. (2011). Partiality, State, and Dependent Types. In Proceedings of Typed LAmbda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011 (Vol. LNCS 6690, pp. 198-212). Springer.

Displaying results 201 to 250 out of 336

Revised 17.04.2023

Sofia Hedegaard Rasmussen