The Aya Prover

• Installation Guide
• Tutorial for functional programmers (such as ML, Haskell, or Idris users)
• Tutorial for dependent types or theorem prover users
• Tutorial for VSCode extension
• Tutorial for the fake literate mode

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

The type system of Aya has the following highlights:

• Set-level cubical features so funExt and quotients are available without axioms (like Agda, redtt, and Arend but not higher-dimensional),
• Overlapping and order-independent pattern matching makes simple functions compute better,
• Practical functional programming features similar to Haskell and Idris: dependent pattern matching, typed holes, enchanted synthesis of implicit arguments.

The implementation of the Aya compiler has the following highlights:

• Efficient type checking by JIT-compiling well-typed definitions to JVM higher-order abstract syntax, so substitution does not traverse terms,
• Convenient interactive tools such as a language server for VSCode, a REPL, and hyperlinked document generation (demo),
• Pre-compiled binary release.