Comparison
See also: Proof assistant#Comparison| Language | Actively developed | Paradigm | Tactics | Proof terms | Termination checking | Types can depend on | Universes | Proof irrelevance | Program extraction | Extraction erases irrelevant terms |
|---|---|---|---|---|---|---|---|---|---|---|
| Agda | Yes | Purely functional | Few/limited | Yes | Yes (optional) | Any term | Yes (optional) | Proof-irrelevant arguments (experimental) | Haskell, Javascript | Yes |
| ATS | Yes | Functional / imperative | No | Yes | Yes | ? | ? | ? | Yes | ? |
| Cayenne | No | Purely functional | No | Yes | No | Any term | No | No | ? | ? |
| Coq | Yes | Purely functional | Yes | Yes | Yes | Any term | Yes | No | Haskell, Scheme and OCaml | Yes |
| Dependent ML | No | ? | ? | Yes | ? | Natural numbers | ? | ? | ? | ? |
| Epigram 2 | Yes | Purely functional | No | Coming soon | By construction | Any term | Coming soon | Coming soon | Coming soon | Coming soon |
| Guru | Yes | Purely functional | hypjoin | Yes | Yes | Any term | No | Yes | Carraway | Yes |
| Idris | Yes | Purely functional | Yes | Yes | Coming soon | Any term | No | No | Yes | Yes, aggressively |
| Matita | Yes | Purely functional | Yes | Yes | Yes | Any term | Yes | ? | OCaml | ? |
| NuPRL | No | Purely functional | Yes | Yes | Yes | Any term | Yes | ? | Yes | ? |
| PVS | Yes | ? | Yes | ? | ? | ? | ? | ? | ? | ? |
| Typed Racket | Yes | No | ? | ? | ? | ? | ? | ? | ? | ? |
| Sage | ? | Hybrid typechecking | ? | ? | ? | ? | ? | ? | ? | ? |
| Twelf | Yes | Logic programming | ? | Yes | Yes (optional) | Any (LF) term | No | No | ? | ? |
| Xanadu | No | Imperative | ? | ? | ? | ? | ? | ? | ? | ? |
Read more about this topic: Dependent Type
Famous quotes containing the word comparison:
“In everyone’s youthful dreams, philosophy is still vaguely but inseparably, and with singular truth, associated with the East, nor do after years discover its local habitation in the Western world. In comparison with the philosophers of the East, we may say that modern Europe has yet given birth to none.”
—Henry David Thoreau (1817–1862)
“When we reflect on our past sentiments and affections, our thought is a faithful mirror, and copies its objects truly; but the colours which it employs are faint and dull, in comparison of those in which our original perceptions were clothed.”
—David Hume (1711–1776)
“Certainly there is not the fight recorded in Concord history, at least, if in the history of America, that will bear a moment’s comparison with this, whether for the numbers engaged in it, or for the patriotism and heroism displayed.”
—Henry David Thoreau (1817–1862)