Homotopy Type Theory: Programming and Verification

Project: Research

Filter
Conference contribution book

Search results

  • 2020

    Three equivalent ordinal notation systems in cubical Agda

    Nordvall Forsberg, F., Xu, C. & Ghani, N., 24 Jan 2020, CPP 2020 : Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. Blanchette, J. & Hritcu, C. (eds.). New York, p. 172–185 14 p.

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

    Open Access
    File
    7 Citations (Scopus)
    66 Downloads (Pure)
  • 2019

    Generic level polymorphic N-ary functions

    Allais, G., 18 Aug 2019, TyDe 2019 - Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development, co-located with ICFP 2019. Darais, D. & Gibbons, J. (eds.). New York, p. 14-26 13 p.

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

    Open Access
    File
    50 Downloads (Pure)
  • 2017

    Type-and-scope safe programs and their proofs

    Allais, G., Chapman, J., McBride, C. & McKinna, J., 16 Jan 2017, CPP 2017 : Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. Bertot, Y. & Vafeiadis, V. (eds.). New York, 13 p.

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

    Open Access
    File
    33 Citations (Scopus)
    139 Downloads (Pure)
  • Do Be Do Be Do

    Lindley, S., McBride, C. & McLaughlin, C., 15 Jan 2017, POPL'2017 : Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Gordon, A. (ed.). New York, p. 500-514 15 p.

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

    Open Access
    File
    56 Citations (Scopus)
    229 Downloads (Pure)
  • 2016

    Proof-relevant parametricity

    Ghani, N., Nordvall Forsberg, F. & Orsanigo, F., 25 Mar 2016, A List of Successes That Can Change the World. Lindley, S., McBride, C., Trinder, P. & Sannella, D. (eds.). Switzerland: Springer-Verlag, p. 109-131 23 p. (Lecture Notes in Computer Science; vol. 9600).

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

    Open Access
    File
    3 Citations (Scopus)
    36 Downloads (Pure)
  • Comprehensive parametric polymorphism: categorical models and type theory

    Ghani, N., Nordvall Forsberg, F. & Simpson, A., 22 Mar 2016, International Conference on Foundations of Software Science and Computation Structures [FoSSaCS 2016]. Jacobs, B. & Löding, C. (eds.). Berlin: Springer-Verlag, Vol. 9634. p. 3-19 17 p. (Lecture Notes in Computer Science).

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

    Open Access
    File
    7 Citations (Scopus)
    217 Downloads (Pure)