Skip to content

The Aya Prover ‚Äč

Aya is a programming language and an interactive proof assistant designed for type-directed programming and formalizing math.

The type system of Aya features in the following:

  • Univalent features similar to Cubical Agda, redtt, and Arend,
  • Overlapping and order-independent pattern matching,
  • Practical functional programming features similar to Haskell and Idris.