Birkedal, L., Rosolini, G., Scott, D. S. & van Oosten, J. (Eds.) (2002).
Proceedings of the Tutorial Workshop on Realizability Semantics and Applications: held June 30 and July 1, 1999 in Trento, Italy, as one of the satellite workshops associated to the Federated Logic Conference. Elsevier. Mathematical Structures in Computer Science Vol. 12 No. 3, special issue
http://journals.cambridge.org/action/displayIssue?decade=2000&jid=MSC&volumeId=12&issueId=03&iid=114628
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
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. (2019).
Guarded Cubical Type Theory.
Journal of Automated Reasoning,
63(2), 211-253.
https://doi.org/10.1007/s10817-018-9471-7,
https://doi.org/10.1007/s10817-018-9471-7
Birkedal, L., Clouston, R., Mannaa, B., Ejlers Møgelberg, R., Pitts, A. M.
& Spitters, B. (2020).
Modal dependent type theory and dependent right adjoints.
Mathematical Structures in Computer Science,
30(2), 118-138.
https://doi.org/10.1017/S0960129519000197
Birkedal, L., Dinsdale-Young, T.
, Guéneau, A., Jaber, G., Svendsen, K. & Tzevelekos, N. (2021).
Theorems for free from separation logic specifications.
Proceedings of the ACM on Programming Languages ,
5(ICFP), Article 81.
https://doi.org/10.1145/3473586
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.
https://doi.org/10.1007/978-3-540-31987-0_17
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.
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.
https://doi.org/10.1007/978-3-642-32347-8_21
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
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
André, É., Bloemen, V., Petrucci, L.
& Pol, J. V. D. (2019).
Minimal-Time Synthesis for Parametric Timed Automata. In L. Zhang & T. Vojnar (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings (Vol. II, pp. 211-228). Springer.
https://doi.org/10.1007/978-3-030-17465-1_12
André, É., Marinho, D.
& Pol, J. V. D. (2021).
A Benchmarks Library for Extended Parametric Timed Automata. In F. Loulergue & F. Wotawa (Eds.),
Tests and Proofs - 15th International Conference, TAP 2021, Held as Part of STAF 2021, Proceedings: 15th International Conference, TAP 2021, Held as Part of STAF 2021, Virtual Event, June 21–22, 2021, Proceedings (pp. 39-50). Springer.
https://doi.org/10.1007/978-3-030-79379-1_3
André, É., Arias, J., Petrucci, L.
& Pol, J. V. D. (2021).
Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata. In J. F. Groote & K. G. Larsen (Eds.),
Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021: 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part I (pp. 311-329). Springer.
https://doi.org/10.1007/978-3-030-72016-2_17
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.),
Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings (pp. 214-241). Springer VS.
https://doi.org/10.1007/978-3-319-89884-1_8
Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Katsumata, S. Y. & Sato, T. (2021).
Higher-order probabilistic adversarial computations: categorical semantics and program logics.
Proceedings of the ACM on Programming Languages ,
5(ICFP), Article 93.
https://doi.org/10.1145/3473598