Aya is a proof assistant and dependently-typed programming language. It supports advanced type-theoretic features and is designed for both theorem proving and functional programming.
The language includes dependent types, cubical type theory, pattern matching, termination checking, and literate programming capabilities.
This is free and open source software.
Key Features
- Dependent types including Π-types, Σ-types, and indexed families.
- Set-level cubical type theory.
- Support for quotient-inductive-inductive types.
- Pattern matching with first-match semantics.
- Overlapping and order-independent patterns.
- JIT compiler translating Aya code to higher-order abstract syntax in Java.
- Literate programming mode with inline code fragments.
- Binary operators with precedence specified using partial ordering.
- Termination checker capable of accepting complex recursive definitions.
Website: github.com/aya-prover/aya-dev
Support:
Developer: Aya Prover developers
License: MIT License
Aya is written in Java. Learn Java with our recommended free books and free tutorials.
Related Software
| Proof Assistants | |
|---|---|
| Coq | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Agda | Interactive system for writing and checking proofs |
| Lean | Programming language and theorem prover |
| Matita | Experimental, interactive theorem prover |
Read our verdict in the software roundup.
 Explore our comprehensive directory of recommended free and open source software. Our carefully curated collection spans every major software category.This directory is part of our ongoing series of informative articles for Linux enthusiasts. It features hundreds of detailed reviews, along with open source alternatives to proprietary solutions from major corporations such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. You’ll also find interesting projects to try, hardware coverage, free programming books and tutorials, and much more. Discovered a useful open source Linux program that we haven’t covered yet? Let us know by completing this form. |