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 Disambiguation Statements Elicitation Referenced by

All labels observed (3)

Label Occurrences
Coq canonical 13
Coq proof assistant 9
Coq type class system 1

How this entity was disambiguated

Statements (56)

Predicate Object
instanceOf dependently typed programming language ⓘ
functional programming language ⓘ
interactive theorem prover ⓘ
proof assistant ⓘ
basedOn dependent type theory ⓘ
canExtractTo Haskell ⓘ
OCaml ⓘ
Scheme ⓘ
developedBy INRIA ⓘ
developedIn France ⓘ
hasApplication certified programming ⓘ
formal verification of mathematical proofs ⓘ
formal verification of software ⓘ
program extraction ⓘ
hasCommunity Coq development team ⓘ
linked to: Inria–Université Paris-Sud–CNRS research community around Coq

Coq users community ⓘ
hasFeature Gallina specification language ⓘ
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 ⓘ
Proof General ⓘ
command-line interface ⓘ
implements Calculus of Inductive Constructions ⓘ
Predicative Calculus of Inductive Constructions ⓘ
linked to: Calculus of Inductive Constructions
initialReleaseYear 1989 ⓘ
license LGPL ⓘ
linked to: GNU Lesser General Public License
namedAfter Thierry Coquand ⓘ
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 ⓘ
website https://coq.inria.fr ⓘ
writtenIn OCaml ⓘ

How these facts were elicited

Referenced by (23)

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 proof assistant ⓘ
linked to: Coq
Vampire automated theorem prover → relatedTo → Coq proof assistant ⓘ
linked to: Coq
Idris → influencedBy → Coq ⓘ
Xavier Leroy → usedToolInResearch → Coq proof assistant ⓘ
linked to: Coq
Curry–Howard correspondence → usedIn → Coq ⓘ
ELPI → isRelatedTo → Coq ⓘ
HOL theorem prover → relatedTo → Coq ⓘ
LCF → influenced → Coq ⓘ
HOL Light → relatedTo → Coq ⓘ
univalent foundations program → relatedTo → Coq ⓘ
Martin-Löf type theory → influenced → Coq ⓘ
homotopy type theory → implementedIn → Coq ⓘ
Calculus of Constructions → influenced → Coq proof assistant ⓘ
subject linked to: calculus of constructions
linked to: Coq
Christine Paulin-Mohring → knownFor → Coq proof assistant ⓘ
subject linked to: Paulin-Mohring
linked to: Coq
Inria–Université Paris-Sud–CNRS research community around Coq → focusesOn → Coq proof assistant ⓘ
linked to: Coq
Inria–Université Paris-Sud–CNRS research community around Coq → uses → Coq ⓘ
Yves Bertot → notableWork → Coq proof assistant ⓘ
linked to: Coq
Interactive Theorem Proving and Program Development → mainSubject → Coq proof assistant ⓘ
subject linked to: Yves Bertot
linked to: Coq
Matthieu Sozeau → notableWork → Coq proof assistant ⓘ
linked to: Coq
Matthieu Sozeau → contributedTo → Coq type class system ⓘ
linked to: Coq
Matthieu Sozeau → toolDeveloperFor → Coq ⓘ