github.com/aya-prover/aya-dev ↗

About aya-prover/aya-dev

Aya is a proof assistant and dependently-typed programming language written in Java. It enables users to write programs with advanced type system features including Pi-types, Sigma-types, indexed families, and set-level cubical type theory. The language supports pattern matching with first-match semantics, overlapping patterns, and includes a fairly sophisticated termination checker adapted from Agda that accepts definitions rejected by other proof assistants.

The project includes a JIT compiler that translates Aya code to higher-order abstract syntax in Java, significantly improving runtime performance on tasks like tree sorting. It also supports literate programming with inline code fragments and uses a partial ordering system for binary operator precedence rather than numeric precedence levels. Notable features include support for quotient-inductive-inductive types without forward declarations and demonstrations of advanced proofs like function extensionality.

Aya is still under active development and is available through both direct downloads and as a library via Maven. The project provides comprehensive documentation including installation instructions, tutorials for functional programming and theorem proving, and welcomes contributions and questions from users. The development team particularly values feedback on user interaction and error reporting quality.