20152018
If you made any changes in Pure, your changes will be visible here soon.

Fingerprint The Fingerprint is created by mining the titles and abstracts of the person's research outputs and projects/funding awards to create an index of weighted terms from discipline-specific thesauri.

Homotopy Theory Mathematics
Homotopy Type Mathematics
Type Theory Mathematics
Mechanization Mathematics
Gluing Engineering & Materials Science
Covering Space Mathematics
Polymorphism Engineering & Materials Science
Cohomology Mathematics

Network Recent external collaboration on country level. Dive into details by clicking on the dots.

Research Output 2015 2018

  • 5 Conference contribution
  • 2 Article
  • 1 Conference article
1 Citation (Scopus)

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

Semantics
1 Citation (Scopus)

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

Homotopy Theory
Homotopy Type
Type Theory
Cohomology
Cell Complex

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

Topology
2 Citations (Scopus)

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

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

Polymorphism
Terminology