Publications

Krishnaswam, N. R. K., Aldrich, J. & Birkedal, L. (2007). Modular Verification of the Subject-Observer Pattern via Higher-order Separation Logic. In Proceedings of 9th Workshop on Formal Techniques for Java-like Programs, FTfJP Fakultät für Informatik, Universität Magdeburg. http://www.cs.cmu.edu/~neelk/observer.pdf

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

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.), 27th European Symposium on Programming, ESOP 2018 (pp. 214-241). Springer VS. Lecture Notes in Computer Science (LNCS) No. 10801 https://doi.org/10.1007/978-3-319-89884-1_8

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

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

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 [8005097] IEEE. Annual Symposium on Logic in Computer Science No. 32 https://doi.org/10.1109/LICS.2017.8005097

Bauer, A. & Birkedal, L. (2000). Continuous Functionals of Dependent Types and Equilogical Spaces. In P. G. Clote & H. Schwichtenberg (Eds.), Computer Science Logic: 14th InternationalWorkshop, CSL 2000 Annual Conference of the EACSL Fischbachau, Germany, August 21 – 26, 2000 Proceedings (pp. 202-216). Springer. Lecture Notes in Computer Science Vol. 1862 https://doi.org/10.1007/3-540-44622-2_13

Bay, J. & Askarov, A. (2020). Reconciling progress-insensitive noninterference and declassification. In 2020 IEEE 33rd Computer Security Foundations Symposium (CSF) (pp. 95-106). IEEE. Proceedings - IEEE Computer Security Foundations Symposium Vol. 2020-June https://doi.org/10.1109/CSF49147.2020.00015

Bengtson, J., Jensen, J. B., Sieczkowski, F. & Birkedal, L. (2011). Verifying object-oriented programs with higher-order separation logic in Coq. In M. V. Eekelen , H. Geuvers, J. Schmaltz & F. Wiedijk (Eds.), Interactive Theorem Proving: Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings (pp. 22-38). Springer. Lecture Notes in Computer Science Vol. 6898 https://doi.org/10.1007/978-3-642-22863-6_5

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. Lecture Notes in Computer Science Vol. 7406 https://doi.org/10.1007/978-3-642-32347-8_21

Biering, B., Birkedal, L. & Torp-Smith, N. (2005). BI hyperdoctrines and higher-order separation logic. In M. Sagiv (Ed.), Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings (pp. 233-247). Springer. Lecture Notes in Computer Science Vol. 3444 https://doi.org/10.1007/978-3-540-31987-0_17

Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J. J. & Yang, H. (2011). Step-Indexed Kripke Models over Recursive Worlds. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, Texas, USA (pp. 119-132). Association for Computing Machinery.

Birkedal, L., Støvring, K. & Thamsborg, J. J. (2009). Relational Parametricity for References and Recursive Types. In A. Kennedy & A. Ahmed (Eds.),  Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009. (pp. 91-104). Association for Computing Machinery.

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 Schloss Dagstuhl--Leibniz-Zentrum für Informatik. Leibniz International Proceedings in Informatics Vol. 16 https://doi.org/10.4230/LIPIcs.CSL.2012.107

Birkedal, L., Støvring, K. & Thamsborg, J. (2009). Realizability semantics of parametric polymorphism, general references, and recursive types. In L. D. Alfaro (Ed.), Foundations of Software Science and Computational Structures: 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings (pp. 456-470). Springer. Lecture Notes in Computer Science Vol. 5504 https://doi.org/10.1007/978-3-642-00596-1_32

Birkedal, L., Støvring, K. & Thamsborg, J. (2009). Solutions of generalized recursive metric-space equations. In R. Matthes & T. Uustalu (Eds.), 6th Workshop on Fixed Points in Computer Science, FICS 2009: Coimbr a, P ortugal, 12-13 September 2009, Proceedings (pp. 18-24). Institute of Cybernetics at Tallinn University of Technology.

Birkedal, L., Swinghammer, J. & Støvring, K. (2010). A Metric Model of Lambda Calculus with Guarded Recursion. In L. Santocanale (Ed.), Fixed Points in Computer Science 2010: Brno, August 21-22, 2010 http://www.diku.dk/~stovring/papers/metric-model-guarded-recursion.pdf

Birkedal, L. & Yang, H. (2007). Relational parametricity and separation logic. In S. Helmut (Ed.), Foundations of Software Science and Computation Structures: 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24-April 1, 2007. Proceedings (pp. 93-107). Springer. Lecture Notes in Computer Science Vol. 4423 https://doi.org/10.1007/978-3-540-71389-0_8

Birkedal, L., Debois, S. & Hildebrandt, T. (2006). Sortings for reactive systems. In C. Baier & H. Hermanns (Eds.), CONCUR 2006 – Concurrency Theory: 17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006. Proceedings (pp. 248-262). Springer. Lecture Notes in Engineering and Computer Science Vol. 4137 https://doi.org/10.1007/11817949_17

Birkedal, L., Debois, S., Elsborg, E., Hildebrandt, T. & Niss, H. (2006). Bigraphical models of context-aware systems. In L. Aceto & A. Ingólfsdóttir (Eds.), Foundations of Software Science and Computation Structures: 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006. Proceedings (Vol. 3921 , pp. 187-201). Springer VS. Lecture Notes in Computer Science Vol. 3921 https://doi.org/10.1007/11690634_13

Birkedal, L., Torp-Smith, N. & Yang, H. (2005). Semantics of Separation-logic Typing and Higher-order Frame Rules. In 20th Annual IEEE Symposium on Logic in Computer Science, 2005. LICS 2005. Proceedings (pp. 260-269). IEEE. https://doi.org/10.1109/LICS.2005.47

Birkedal, L., Tofte, M. & Vejlstrup, M. (1996). From region inference to von Neumann machines via region representation inference. In Proceedings of the 1996 ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages: St.Petersburg, FL, USA; ; 21 January 1996 through 24 January 1996 (pp. 171-183). Association for Computing Machinery. A C M. S I G P L A N - S I G A C T Symposium on Principles of Programming Languages. Annual Conference Record http://www.scopus.com/inward/record.url?scp=0029725194&partnerID=8YFLogxK