Proof Assistant
Software used to assist in proving mathematical theorems and verifying logical correctness.
Plangs
| Name | Description |
|---|---|
| AbcDatalog | Easy Datalog for research & pedagogy. |
| Agda | Dependently typed functional programming language and proof assistant used for writing and verifying proofs. |
| Ascent | Logic programming language (similar to Datalog) embedded in Rust via macros. |
| Ciao | Modern Prolog implementation focused on portability, extensibility, and modularity. |
| Coq | Interactive theorem prover focused on formal verification and proof checking. |
| ELPI | An embeddable interpreter for a λProlog variant enriched with Constraint Handling Rules. |
| Eqlog | A logic programming language for Datalog with equality support. |
| Formulog | Datalog with support for SMT queries and first-order functional programming. |
| Idris | Purely-functional language for Type-Driven Development with dependent types and optional lazy evaluation. |
| Isabelle | Automated theorem prover for formalizing mathematical proofs in higher-order logic. |
| OCaml | General-purpose, multi-paradigm language extending Caml with OO features. |
| Prolog | Logic programming language used in AI and theorem proving, influenced by first-order logic for declarative tasks. |
| Scryer Prolog | An ISO Prolog implemented in Rust. |
| Standard ML | Functional programming language known for its type inference and usage in compiler writing. |