Skip to content

Recommended Reading

This is a list of documents that are helpful or simply related to the design & implementation of Aya, randomly ordered.

Beware that you are encouraged to suggest changes to this page! Just go to the bottom of this page and there will be a link. Apart from this list, Jon Sterling's cubical bibliography is also a good source of information.

General Type Theory


Univalent Type Theory

Cubical Type Theory



  • Coq's Vibrant Ecosystem for Verification Engineering, by Andrew W. Appel
    CPP 2022
  • The End of History? Using a Proof Assistant to Replace Language Design with Library Design, by Adam Chlipala, Benjamin Delaware, Samuel Duchovni, Jason Gross, Clément Pit-Claudel, Sorawit Suriyakarn, Peng Wang, Katherine Ye
    SNAPL 2017