Publications

This is a list of publications and write-ups related to Aya by the Aya developers.

Papers

• A simpler encoding of indexed types, by Tesla Zhang
  TyDe 2021
  arXiv preprint | doi
  Describes the simple syntax for defining type families in Aya.

Notes

• (Co)conditions hit the path, by Tesla Zhang
  arXiv preprint
  An interesting language feature, no longer used in Aya. This document describes the type checking algorithm, and does not discuss any metatheory. Still used in Arend.
• Two tricks to trivialize higher-indexed families, by Tesla Zhang
  arXiv preprint
  Not directly related to Aya, but discusses the idea of Fording, which is used in Aya.
• A tutorial on implementing De Morgan cubical type theory, by Tesla Zhang
  arXiv preprint
  Describes how to type check De Morgan cubical primitives and partial elements. The part about partial elements is still relevant to Aya.
• Elegant elaboration with function invocation, by Tesla Zhang
  arXiv preprint
  Describes how δ-reduction works in Aya.