20152020

Research output per year

If you made any changes in Pure these will be visible here soon.

Research Output

  • 5 Conference contribution
  • 3 Article
  • 1 Conference article
2020

Cellular cohomology in homotopy type theory

Buchholtz, U. & Hou, K. B., 2020, In : Logical Methods in Computer Science. 16, 2, p. 1-21 21 p., 7.

Research output: Contribution to journalArticle

2018

Cartesian cubical computational type theory: Constructive reasoning with paths and equalities

Angiuli, C., Hou, K. B. & Harper, R., Aug 1 2018, Computer Science Logic 2018, CSL 2018. Ghica, D. R. & Jung, A. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 6. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 119).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations

Cellular cohomology in homotopy type theory

Buchholtz, U. & Favonia, K. B. H., Jul 9 2018, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Institute of Electrical and Electronics Engineers Inc., p. 521-529 9 p. (Proceedings - Symposium on Logic in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Scopus citations

Covering spaces in homotopy type theory

Favonia, K. B. H. & Harper, R., Oct 1 2018, 22nd International Conference on Types for Proofs and Programs, TYPES 2016. Geuvers, H., Ivetic, J. & Ghilezan, S. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 11. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 97).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

The RedPRL proof assistant (invited paper)

Angiuli, C., Cavallo, E., Favonia, K. B. H., Harper, R. & Sterling, J., Jul 3 2018, In : Electronic Proceedings in Theoretical Computer Science, EPTCS. 274, p. 1-10 10 p.

Research output: Contribution to journalConference article

Open Access
2 Scopus citations
2017

Correctness of compiling polymorphism to dynamic typing

Hou, K. B., Benton, N. & Harper, R., Jan 1 2017, In : Journal of Functional Programming. 27, e1.

Research output: Contribution to journalArticle

2016

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory

Favonia, K. B. H., Finster, E., Licata, D. R. & Lumsdaine, P. L., Jul 5 2016, Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, LICS 2016. Institute of Electrical and Electronics Engineers Inc., p. 565-574 10 p. (Proceedings - Symposium on Logic in Computer Science; vol. 05-08-July-2016).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Scopus citations

The Seifert-van Kampen theorem in homotopy type theory

Favonia, F. & Shulman, M., Aug 1 2016, Computer Science Logic 2016, CSL 2016. Talbot, J-M. & Regnier, L. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, (Leibniz International Proceedings in Informatics, LIPIcs; vol. 62).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Scopus citations
2015

Covering Spaces in Homotopy Type Theory

Hou, K. B., Jan 1 2015, In : Trends in Mathematics. 3, p. 77-82 6 p.

Research output: Contribution to journalArticle

1 Scopus citations