Publications

Sort by: Date | Author | Title

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

Ahmed, A. (Ed.), Benton, N. (Ed.) & Birkedal, L. (2010). 10351 Abstracts Collection Modelling, Controlling and Reasoning About State: Dagstuhl Seminar . Schloss Dagstuhl--Leibniz-Zentrum für Informatik. Dagstuhl Seminar Proceedings Vol. 10351 http://drops.dagstuhl.de/opus/volltexte/2010/2811/

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

Awodey, S. & Birkedal, L. (2003). Elementary axioms for local maps of toposes. Journal of Pure and Applied Algebra, 177(3), 215-230. https://doi.org/10.1016/S0022-4049(02)00283-9

Awodey, S., Birkedal, L. & Scott, D. S. (1999). Local realizability toposes and a modal logic for computability - (Extended Abstract). Electronic Notes in Theoretical Computer Science, 23(1), 13-26. https://doi.org/10.1016/S1571-0661(04)00101-X

Awodey, S., Birkedal, L. & Scott, D. S. (2002). Local realizability toposes and a modal logic for computability. Mathematical Structures in Computer Science, 12(3), 319-334. https://doi.org/10.1017/S0960129502003675

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. & Scott, D. S. (2004). Equilogical spaces. Theoretical Computer Science, 315(1), 35-59. https://doi.org/10.1016/j.tcs.2003.11.012

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. (2007). BI-hyperdoctrines, higher-order separation logic, and abstraction. A C M Transactions on Programming Languages and Systems, 29(5), [1275499]. https://doi.org/10.1145/1275497.1275499

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., Bizjak, A. & Schwinghamme, J. (2013). Step-Indexed Relational Reasoning for Countable Nondeterminism. Logical Methods in Computer Science, 9(4), [4]. https://doi.org/10.2168/LMCS-9(4:4)2013

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

Birkedal, L., Møgelberg, R. E. & Lerchedahl Petersen, R. (2008). Category-theoretic models of linear Abadi & Plotkin Logic. Theory and Applications of Categories, 20(7), 116-151.

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

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., Støvring, K. & Thamsborg, J. J. (2010). The category-theoretic solution of recursive metric-space equations. Theoretical Computer Science, 411(47), 4102-4122.

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

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

Birkedal, L., Debois, S. & Hildebrandt, T. (2008). On the Construction of Sorted Reactive Systems. Lecture Notes in Computer Science, 5201, 218-232. https://doi.org/10.1007/978-3-540-85361-9

Birkedal, L., Reus, B., Schwinghammer, J. & Yang, H. (2008). A Simple Model of Separation Logic for Higher-order Store. Lecture Notes in Computer Science, 348-360.

Birkedal, L. & Yang, H. (2008). Relational Parametricity and Separation Logic. Logical Methods in Computer Science, 4(2), 1-27. https://doi.org/10.2168/LMCS-4(2:6)2008

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

Birkedal, L., Torp-Smith, N. & Yang, H. (2006). Semantics of Separation-logic Typing and Higher-order Frame Rules for Algol-like Languages. Logical Methods in Computer Science, 2(5:1), 1-33. https://doi.org/10.2168/LMCS-2(5:1)2006

Birkedal, L. & Welinder, M. (1995). Binding-time analysis for Standard ML. Higher-Order and Symbolic Computation, 8(3), 191-208. https://doi.org/10.1007/BF01019003

Birkedal, L. (2002). A general notion of realizability. Bulletin of Symbolic Logic, 8(2), 266-282. http://www.scopus.com/inward/record.url?scp=0036017415&partnerID=8YFLogxK

Birkedal, L. & van Oosten, J. (2002). Relative and modified relative realizability. Annals of Pure and Applied Logic, 118(1-2), 115-132. https://doi.org/10.1016/S0168-0072(01)00122-1

Birkedal, L. & Tofte, M. (2001). A constraint-based region inference algorithm. Theoretical Computer Science, 258(1-2), 299-392. https://doi.org/10.1016/S0304-3975(00)00025-6

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. (2000). Developing theories of types and computability via realizability. Elsevier. Electronic Notes in Theoretical Computer Science Vol. 34 https://doi.org/10.1016/S1571-0661(05)80642-5

Birkedal, L. & Harper, R. (1999). Relational Interpretations of Recursive Types in an Operational Setting. Information and Computation, 155(1-2), 3-63. http://www.scopus.com/inward/record.url?scp=0000650306&partnerID=8YFLogxK

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

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., Damgaard, T. C., Glenstrup, A. J. & Milner, R. (2007). Matching of Bigraphs. Electronic Notes in Theoretical Computer Science, 175(4 SPEC. ISS.), 3-19. https://doi.org/10.1016/j.entcs.2007.04.013

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., Møgelberg, R. E. & Petersen, R. L. (2006). Parametric Domain-theoretic Models of Polymorphic Intuitionistic / Linear Lambda Calculus. Electronic Notes in Theoretical Computer Science, 155(1 SPEC. ISS.), 191-217. https://doi.org/10.1016/j.entcs.2005.11.057

Birkedal, L., Torp-Smith, N. & Reynolds, J. C. (2004). Local reasoning about a copying garbage collector. SIGPLAN Notices, 39(1), 220-231. http://www.scopus.com/inward/record.url?scp=1442263140&partnerID=8YFLogxK

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

Displaying results 1 to 50 out of 180

Page 1

Page 2

Page 3

Page 4

Revised 03.08.2021 -

Sofia Rasmussen