Research Output per year

## 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

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 proceeding › Conference 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 proceeding › Conference 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 proceeding › Conference 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 journal › Conference 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 journal › Article

Polymorphism

Terminology