Coq

E446868
dependently typed programming language functional programming language interactive theorem prover proof assistant

Coq is an interactive theorem prover and functional programming language based on dependent type theory, widely used for formally verifying mathematical proofs and software correctness.

Try in SPARQL Jump to: Surface forms Statements Referenced by

Observed surface forms (1)

Surface form Occurrences
Coq proof assistant 2

Statements (56)

Predicate Object
instanceOf dependently typed programming language ⓘ
functional programming language ⓘ
interactive theorem prover ⓘ
proof assistant ⓘ
basedOn dependent type theory ⓘ
canExtractTo Haskell NERFINISHED ⓘ
OCaml NERFINISHED ⓘ
Scheme ⓘ
developedBy INRIA NERFINISHED ⓘ
developedIn France NERFINISHED ⓘ
hasApplication certified programming ⓘ
formal verification of mathematical proofs ⓘ
formal verification of software ⓘ
program extraction ⓘ
hasCommunity Coq development team NERFINISHED ⓘ
Coq users community ⓘ
hasFeature Gallina specification language NERFINISHED ⓘ
Ltac tactic language ⓘ
coercions ⓘ
interactive proof mode ⓘ
module system ⓘ
notations ⓘ
proof scripts ⓘ
standard library ⓘ
universe polymorphism ⓘ
hasInterface Coq support in Emacs ⓘ
Coq support in VS Code ⓘ
Coq support in Vim ⓘ
CoqIDE NERFINISHED ⓘ
Proof General NERFINISHED ⓘ
command-line interface ⓘ
implements Calculus of Inductive Constructions NERFINISHED ⓘ
Predicative Calculus of Inductive Constructions NERFINISHED ⓘ
initialReleaseYear 1989 ⓘ
license LGPL NERFINISHED ⓘ
namedAfter Thierry Coquand NERFINISHED ⓘ
repository https://github.com/coq/coq ⓘ
supports coinductive types ⓘ
constructive logic ⓘ
dependent types ⓘ
extraction to functional programming languages ⓘ
higher-order logic ⓘ
inductive types ⓘ
modules ⓘ
pattern matching ⓘ
proof automation ⓘ
tactics ⓘ
type classes ⓘ
usedFor teaching logic ⓘ
teaching type theory ⓘ
usedIn CompCert C compiler verification ⓘ
Feit–Thompson theorem formalization ⓘ
Four Color Theorem formalization ⓘ
Verified Software Toolchain NERFINISHED ⓘ
website https://coq.inria.fr ⓘ
writtenIn OCaml NERFINISHED ⓘ

Referenced by (4)

Full triples — surface form annotated when it differs from this entity's canonical label.

Gödel's ontological proof → verifiedIn → Coq ⓘ
OCaml → influenced → Coq ⓘ
Christine Paulin-Mohring → notableWork → Coq ⓘ
this entity surface form: Coq proof assistant
Vampire automated theorem prover → relatedTo → Coq ⓘ
this entity surface form: Coq proof assistant