Publications

Sort by: Date | Author | Title

Birkedal, L. & Welinder, M. (1995). Binding-time analysis for Standard ML. In PEPM'94 - ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, Walt Disney World Vilage, Orlando, Florida, USA, 25 June 1994, Proceedings: Technical Report 94/9. (pp. 61-71). University of Melbourne. Department of Computer Science.

Birkedal, L., Carboni, A., Rosolini, G. & Scott, D. S. (1998). Type theory via exact categories. In K. Kelly (Ed.), Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science: 21-24 Jun 1998, Indianapolis, IN (pp. 188 - 198 ). IEEE. https://doi.org/10.1109/LICS.1998.705655

Birkedal, L. & Hildebrandt, T. (2004). Bigraphical Programming Languages: A LaCoMoCo research project .

Birkedal, L., Bundgaard, M., Debois, S., Elsborg, E., Glenstrup, A. J., Hildebrandt, T., Milner, R. & Niss, H. (2006). Bigraphical Programming Languages for Pervasive Computing. In T. Strang, V. Cahill & A. Quigley (Eds.), Proceedings of Pervasive 2006 International Workshop on Combining Theory and Systems Building in Pervasive Computing (CTSB'06 (pp. 653-658)

Birkedal, L., Støvring, K. & Thamsborg, J. (2010). Realisability semantics of parametric polymorphism, general references and recursive types. Mathematical Structures in Computer Science, 20(4), 655-703. https://doi.org/10.1017/S0960129510000162

Birkedal, L. & Harper, R. (1997). Relational interpretations of recursive types in an operational setting: (Summary). In M. Abadi & T. Ito (Eds.), Theoretical Aspects of Computer Software: Third International Symposium, TACS'97 Sendai, Japan, September 23–26, 1997 Proceedings (pp. 458-490). Springer. Lecture Notes in Engineering and Computer Science Vol. 1281 https://doi.org/10.1007/BFb0014563

Birkedal, L. & Welinder, M. (1994). Hand-writing program generator generators. In M. Hermenegildo & J. Penjam (Eds.), Programming Language Implementation and Logic Programming: 6th International Symposium, PLILP '94 Madrid, Spain, September 14–16, 1994 Proceedings (pp. 198-214). Springer VS. Lecture Notes in Computer Science Vol. 844 https://doi.org/10.1007/3-540-58402-1_15

Birkedal, L. (Ed.) (2004). Proceedings of the 10th Conference on Category Theory in Computer Science (CTCS 2004). Elsevier. Electronic Notes in Theoretical Computer Science Vol. 122 https://doi.org/10.1016/j.entcs.2004.11.009

Birkedal, L., Escardo, M., Jung, A. & Rosolini, G. (Eds.) (2004). Recent Developments in Domain Theory: A collection of papers in honour of Dana S. Scott. Elsevier. Theoretical Computer Science Vol. 316 No. 1-3 http://www.sciencedirect.com/science/journal/03043975/316/1-3

Birkedal, L., Rosolini, G., Scott, D. S. & van Oosten, J. (Eds.) (2002). Proceedings of the Tutorial Workshop on Realizability Semantics and Applications: held June 30 and July 1, 1999 in Trento, Italy, as one of the satellite workshops associated to the Federated Logic Conference. Elsevier. Mathematical Structures in Computer Science Vol. 12 No. 3, special issue http://journals.cambridge.org/action/displayIssue?decade=2000&jid=MSC&volumeId=12&issueId=03&iid=114628

Birkedal, L., van Oosten, J., Rosolini, G. & Scott, D. S. (Eds.) (1999). Proceedings of the Tutorial Workshop on Realizability Semantics and Applications: held June 30 and July 1, 1999 in Trento, Italy, as one of the satellite workshops associated to the Federated Logic Conference. Elsevier. Electronic Notes in Theoretical Computer Science Vol. 23 No. 1 http://www.journals.elsevier.com/electronic-notes-in-theoretical-computer-science/

Birkedal, L., Støvring, K. & Thamsborg, J. (2010). Realizability semantics of parametric polymorphism, general references, and recursive types. Mathematical Structures in Computer Science, 20(4), 655-703. https://doi.org/10.1017/S0960129510000162

Birkedal, L., Bundgaard, M., Debois, S., Grohmann, D. & Hildebrandt, T. (2009). Higher-order contexts via games and the Int-construction. (pp. 32). IT University of Copenhagen. I T University. Technical Report Series Vol. TR-2009-117

Birkedal, L. (2007). Book reviews of S. Awodey: Category Theory. Clarendon Press. Studia Logica: An International Journal for Symbolic Logic, 86(1). https://doi.org/10.1007/s11225-007-9053-x

Birkedal, L., Petersen, R. L., Møgelberg, R. E. & Warming, C. (2006). LILY Operational Semantics and Models of Linear Abadi-Plotkin Logic. IT University of Copenhagen. I T University. Technical Report Series No. TR-2006-83

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

Birkedal, L., Møgelberg, R. E. & Lerc Petersen, R. (2006). Linear Abadi and Plotkin Logic. Logical Methods in Computer Science, 2(5), [2]. https://doi.org/10.2168/LMCS-2(5:2)2006

Birkedal, L. & Møgelberg, R. E. (2005). Categorical models for Abadi and Plotkin's logic for parametricity. Mathematical Structures in Computer Science, 15(4), 709-772. https://doi.org/10.1017/S0960129505004834

Birkedal, L. (2000). A general notion of realizability. In 15th Annual IEEE Symposium on Logic in Computer Science, 2000. Proceedings. (pp. 7 - 17). IEEE Signal Processing Society. https://doi.org/10.1109/LICS.2000.855751

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). Leibniz International Proceedings in Informatics Vol. 62

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

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., 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

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

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

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

Birkedal, L. (2020). Editorial message. Proceedings of the ACM on Programming Languages, 4(POPL).

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), [81]. https://doi.org/10.1145/3473586

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. Lecture Notes in Computer Science Vol. 8560 https://doi.org/10.1007/978-3-319-08918-8_8

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. Lecture Notes in Computer Science Vol. 9034 https://doi.org/10.1007/978-3-662-46678-0_18

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. Lecture Notes in Computer Science https://doi.org/10.1007/978-3-662-49630-5_2

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. Lecture Notes in Computer Science Vol. 9634 https://doi.org/10.1007/978-3-662-49630-5_2

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

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

Bizjak, A., Gratzer, D., Krebbers, R. & Birkedal, L. (2019). Iron: managing obligations in higher-order concurrent separation logic. Proceedings of the ACM on Programming Languages, 3(POPL), 1-30. [65]. https://doi.org/10.1145/3290378

Blaabjerg, J. F. & Askarov, A. (2021). Towards Language-Based Mitigation of Traffic Analysis Attacks. Paper presented at 34th IEEE Computer Security Foundations Symposium, Online, United States.

Bohr, N. & Birkedal, L. (2006). Relational reasoning for recursive types and references. In N. Kobayashi (Ed.), Programming Languages and Systems (Vol. 4279 LNCS, pp. 79-96). Lecture Notes in Computer Science Vol. 4279 https://doi.org/10.1007/11924661_5

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

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. Lecture Notes in Computer Science Vol. 9034 https://doi.org/10.1007/978-3-662-46678-0_26

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.

Damgaard, T. C. & Birkedal, L. (2006). Axiomatizing binding bigraphs. Nordic Journal of Computing, 33(1), 58 - 77 . http://dl.acm.org/citation.cfm?id=1161598&CFID=557689612&CFTOKEN=63942596

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

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

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). [7467352] IEEE Press. https://doi.org/10.1109/EuroSP.2016.22

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

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 (Vol. 10201, pp. 420-447). Springer VS. Lecture Notes in Computer Science Vol. 10201 https://doi.org/10.1007/978-3-662-54434-1_16

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, 4:1 - 4:72. [4]. https://doi.org/10.1145/2818638

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

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).

Dreyer, D., Neis, G., Rossberg, A. & Birkedal, L. (2010). A relational modal logic for higher-order stateful ADTs. In M. Hermenegildo & J. Palsberg (Eds.), Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010 (pp. 185-198). Association for Computing Machinery. https://doi.org/http://doi.acm.org/10.1145/1706299.1706323

Displaying results 51 to 100 out of 180

Page 1

Page 2

Page 3

Page 4

Revised 16.11.2021 -

Sofia Rasmussen