Adamsen, C. Q., Møller, A., Karim, R., Sridharan, M., Tip, F. & Sen, K. (2017).
Repairing Event Race Errors by Controlling Nondeterminism. In
Proceedings - 2017 IEEE/ACM 39th International Conference on Software Engineering, ICSE 2017 (pp. 289-299). Article 7985670 IEEE Press.
https://doi.org/10.1109/ICSE.2017.34
Krebbers, R., Jung, R.
, Bizjak, A., Jourdan, J.-H., Dreyer, D.
& Birkedal, L. (2017).
The Essence of Higher-Order Concurrent Separation Logic. In H. Yang (Ed.),
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 (pp. 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. 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.3018615Birkedal, 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, Aug 1).
Guarded Cubical Type Theory.
https://doi.org/10.4230/LIPIcs.CSL.2016.23
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.04591Dodds, 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/2818638Livshits, B., Sridharan, M., Smaragdakis, Y., Lhoták, O., Amaral, J. N., Chang, B.-Y. E., Guyer, S. Z., Khedker, U. P.
, Møller, A. & Vardoulakis, D. (2015).
In Defense of Soundiness: A Manifesto.
Communications of the A C M,
58(2).
https://doi.org/10.1145/2644805Jung, 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.2676980Sieczkowski, 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
Jensen, C. S., Møller, A., Raychev, V., Dimitrov, D. & Vechev, M. (2015).
Stateless Model Checking of Event-Driven Applications. In
OOPSLA 2015 : Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (pp. 57-73). Association for Computing Machinery.
https://doi.org/10.1145/2814270.2814282
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
