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:
“It is very important not to become hard. The artist must always have one skin too few in comparison to other people, so you feel the slightest wind.”
—Shusha Guppy (b. 1938)
“But the best read naturalist who lends an entire and devout attention to truth, will see that there remains much to learn of his relation to the world, and that it is not to be learned by any addition or subtraction or other comparison of known quantities, but is arrived at by untaught sallies of the spirit, by a continual self-recovery, and by entire humility.”
—Ralph Waldo Emerson (1803–1882)
“In comparison to the French Revolution, the American Revolution has come to seem a parochial and rather dull event. This, despite the fact that the American Revolution was successful—realizing the purposes of the revolutionaries and establishing a durable political regime—while the French Revolution was a resounding failure, devouring its own children and leading to an imperial despotism, followed by an eventual restoration of the monarchy.”
—Irving Kristol (b. 1920)