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. In Y. Bertot & V. Vafeiadis (Eds.),
CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, co-located with POPL 2017: CPP 2017 (pp. 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 from 22nd International Conference on Types for Proofs and Programs, Novi Sad, Serbia.
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. In J.-M. Talbot & L. Regnier (Eds.),
CSL 2016: 25th EACSL Annual Conference on Computer Science Logic (pp. 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. 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.
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. Article 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. 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
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
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
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. 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
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.