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. Here's a piece of Aya code that defines singly-linked lists and a map function:

open inductive List (A : Type) : Type
| [] : List A
| infixr :> (x : A) (xs : List A) : List A

def map {A B : Type} (f : A → B) (xs : List A) : List B elim xs
| [] ⇒ []
| x :> xs' ⇒ f x :> map f xs'

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.