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
- Observational Equality: Now for Good, by ,POPL 2022
- Copatterns: programming infinite structures by observations, by , , ,POPL 2013
- Staged Compilation with Two-Level Type Theory, byICFP 2022
Universes
- Crude but Effective Stratification, by
- Generalized Universe Hierarchies and First-Class Universe Levels, by
- Dependently typed lambda calculus with a lifting operator, by
- An Order-Theoretic Analysis of Universe Polymorphism, by , ,POPL 2023
- Impredicative Observational Equality, by ,POPL 2023
Univalent Type Theory
- Separating Path and Identity Types in Presheaf Models of Univalent Type Theory, by
- A Syntax for Higher Inductive-Inductive Types, by ,FSCD 2018
- Signatures and Induction Principles for Higher Inductive-Inductive Types, by ,LMCS 2020
- Contributions to Multimode and Presheaf Type Theory, by
Cubical Type Theory
- Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types, by , ,ICFP 2019
- Normalization for Cubical Type theory, by ,LICS 2020
- Automating Kan composition, by
- Syntax and models of Cartesian cubical type theory, by , , , , ,MSCS 2021
- A cubical type theory for higher inductive types, by
- Cubical Type Theory: a constructive interpretation of the univalence axiom, by , , ,TYPES 2015
- On Higher Inductive Types in Cubical Type Theory, by , ,LICS 2018
- Computational Semantics of Cartesian Cubical Type Theory, byPhD thesis
- A Cubical Language for Bishop Sets, by , ,LMCS 2022
- Cubical Syntax for Reflection-Free Extensional Equality, by , ,FSCD 2019
Implementation
- A Categorical Perspective on Pattern Unification, by ,
- The "Elaboration Zoo", by
- Elaboration with First-Class Implicit Function Types, byICFP 2020
- Higher-Order Constraint Simplification In Dependent Type Theory, byLFMTP 2009
- Overlapping and Order-Independent Patterns, by , ,
- Elaborating Dependent (Co)Pattern Matching, by ,ICFP 2018