Krebbers, R., Jung, R.
, Bizjak, A., Jourdan, J.-H., Dreyer, D.
& Birkedal, L. (2017).
The Essence of Higher-Order Concurrent Separation Logic. I H. Yang (red.),
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 (s. 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. I Y. Bertot & V. Vafeiadis (red.),
CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017: CPP 2017 (s. 164-172). Association for Computing Machinery.
https://doi.org/10.1145/3018610.3018615
Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H. B., Spitters, B. & Vezzosi, A. (2016).
Guarded cubical type theory. Abstract fra 22nd International Conference on Types for Proofs and Programs, Novi Sad, Serbien.
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. I J.-M. Talbot & L. Regnier (red.),
CSL 2016: 25th EACSL Annual Conference on Computer Science Logic (s. 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. I B. Jacobs & C. Löding (red.),
Foundations of Software Science and Computation Structures: 19th International Conference, FOSSACS 2016 (Bind 9634, s. 20-35). Springer VS.
https://doi.org/10.1007/978-3-662-49630-5_2
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
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. Artikel 4.
https://doi.org/10.1145/2818638
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. I S. Rajamani (red.),
Conference Record of the Annual ACM Symposium on Principles of Programming Languages (s. 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. I C. Urban & X. Zhang (red.),
Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (s. 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. I A. Pitts (red.),
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 (s. 305-316). Springer VS.
https://doi.org/10.1007/978-3-662-46678-0_26
Bizjak, A. & Birkedal, L. (2015).
Step-indexed logical relations for probability. I A. Pitts (red.),
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 (s. 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. I G. Dowek (red.),
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 (s. 108-123). Springer VS.
https://doi.org/10.1007/978-3-319-08918-8_8
Svendsen, K. & Birkedal, L. (2014).
Impredicative concurrent abstract predicates. I Z. Shao (red.),
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 (s. 149-168 ). Springer.
https://doi.org/10.1007/978-3-642-54833-8_9
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).
Modular Reasoning about Separation of Concurrent Data Structures. I M. Felleisen & P. Gardner (red.),
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 (s. 169-188 ). Springer.
https://doi.org/10.1007/978-3-642-37036-6_11
Bengtson, J.
, Jensen, J. B. & Birkedal, L. (2012).
Charge! A framework for higher-order separation logic in Coq. I L. Beringer & A. Felty (red.),
Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings (Bind 7406, s. 315-331). Springer VS.
https://doi.org/10.1007/978-3-642-32347-8_21