Aya is a proof assistant and dependently-typed programming language. It supports advanced type-theoretic features.
Read more
Tag: proof assistant
F* – general-purpose, proof-oriented programming language
F* (pronounced F star) is a programming language designed for writing programs together with machine-checked proofs of their properties.
Read more
PVS – specification and verification system
PVS is a specification and verification system that combines an expressive specification language with support tools and an interactive theorem prover.
Read more
LISA (LISA Is Sets Automated) – proof assistant
LISA (LISA Is Sets Automated) is a proof assistant based on first-order logic sequent calculus and set theory.
Read more
Lambdapi – interactive proof assistant
Lambdapi is an interactive proof assistant based on the λΠ-calculus modulo rewriting.
Read more
HOL Light – interactive theorem prover
HOL Light is an interactive theorem prover and proof checker for formalising and proving mathematical theorems.
Read more
HOL4 – interactive theorem prover
HOL4 is an interactive theorem prover for classical higher-order logic. It provides a platform for formalising mathematics.
Read more
Lean – programming language and theorem prover
The Lean mathematical library, mathlib, is a unified library of mathematics formalized in the Lean proof assistant.
Read more
Isabelle – generic proof assistant
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language.
Read more
Rocq Prover – formal proof management system
Rocq Prover is a formal proof management system. This is free and open source software developed by a wide range of institutions.
Read more
Agda – interactive system for writing and checking proofs
Agda is a proof assistant. It is an interactive system for writing and checking proofs.
Read more
Matita – experimental, interactive theorem prover
Matita (means pencil in italian) is an experimental, interactive theorem prover.
Read more