Inria–Université Paris-Sud–CNRS research community around Coq

E941108

research community scientific collaboration

The Inria–Université Paris-Sud–CNRS research community around Coq is a collaborative French research group focused on the development, theory, and applications of the Coq proof assistant in formal methods and computer science.

Try in SPARQL Jump to: Surface forms Disambiguation Statements Elicitation Referenced by

All labels observed (2)

Label	Occurrences
Coq development team	2
Inria–Université Paris-Sud–CNRS research community around Coq canonical	1

How this entity was disambiguated

This entity first appeared as the object of triple T11695170 — resolving that mention is where its identity was fixed. The disambiguator weighed these candidate entities and picked the highlighted one (or “None”, minting a new entity). This is how homonymy is resolved: the same surface form can point to different entities.

NED1 Entity disambiguation (via context triple) gpt-5-mini-2025-08-07

Target entity: Inria–Université Paris-Sud–CNRS research community around Coq
Context triple: [Christine Paulin-Mohring, memberOf, Inria–Université Paris-Sud–CNRS research community around Coq]

A. Coq
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.
B. Isabelle proof assistant
Isabelle proof assistant is a widely used interactive theorem prover and generic proof assistant designed for formal verification and mathematical logic, particularly known for its support of higher-order logic.
C. Archive of Formal Proofs
The Archive of Formal Proofs is an online, peer-reviewed collection of machine-checked mathematical and computer science proofs formalized primarily in the Isabelle proof assistant.
D. coq gaulois
Coq gaulois is the French term for the Gallic rooster, a national emblem of France symbolizing courage, pride, and the French nation.
E. LCF theorem prover
The LCF theorem prover is an early interactive proof system that pioneered the use of higher-order logic and the LCF-style architecture, forming the conceptual basis for later provers like HOL and Isabelle.
F. None of above. chosen
G. Unsure - the case is ambiguous/there is not enough information to decide.

NED2 Entity disambiguation (via description) gpt-5-mini-2025-08-07

Target entity: Inria–Université Paris-Sud–CNRS research community around Coq
Target entity description: The Inria–Université Paris-Sud–CNRS research community around Coq is a collaborative French research group focused on the development, theory, and applications of the Coq proof assistant in formal methods and computer science.

A. Coq
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.
B. Isabelle proof assistant
Isabelle proof assistant is a widely used interactive theorem prover and generic proof assistant designed for formal verification and mathematical logic, particularly known for its support of higher-order logic.
C. Archive of Formal Proofs
The Archive of Formal Proofs is an online, peer-reviewed collection of machine-checked mathematical and computer science proofs formalized primarily in the Isabelle proof assistant.
D. coq gaulois
Coq gaulois is the French term for the Gallic rooster, a national emblem of France symbolizing courage, pride, and the French nation.
E. LCF theorem prover
The LCF theorem prover is an early interactive proof system that pioneered the use of higher-order logic and the LCF-style architecture, forming the conceptual basis for later provers like HOL and Isabelle.
F. None of above. chosen

Statements (45)

Predicate	Object
instanceOf	research community ⓘ scientific collaboration ⓘ
aimsTo	advance theory of Coq ⓘ develop applications of Coq in academia ⓘ develop applications of Coq in industry ⓘ
appliesTo	formalization of mathematics ⓘ security protocols verification ⓘ software certification ⓘ verification of critical systems ⓘ
basedOn	calculus of inductive constructions ⓘ linked to: Calculus of Inductive Constructions
collaboratesWith	CNRS ⓘ linked to: Centre National de la Recherche Scientifique Inria ⓘ linked to: INRIA Université Paris-Sud ⓘ
contributesTo	development of Coq ecosystem ⓘ
country	France ⓘ
field	computer science ⓘ formal methods ⓘ mathematical logic ⓘ
focusesOn	Coq proof assistant ⓘ linked to: Coq formal verification of hardware ⓘ formal verification of software ⓘ interactive theorem proving ⓘ type theory ⓘ
hasParticipant	researchers from CNRS ⓘ researchers from Inria ⓘ researchers from Université Paris-Sud ⓘ
languageOfWorkOrName	English ⓘ French ⓘ
locatedIn	Île-de-France ⓘ linked to: Île-de-France region
partOf	European research community on theorem proving ⓘ French formal methods community ⓘ
researchArea	certified programming ⓘ dependent type theory ⓘ formal specification ⓘ interactive proof development ⓘ program verification ⓘ proof assistants ⓘ proof automation ⓘ
uses	Coq ⓘ
usesMethod	formal proof development ⓘ interactive proof assistants ⓘ mechanized reasoning ⓘ
worksOn	extensions of Coq ⓘ libraries for Coq ⓘ tools around Coq ⓘ

How these facts were elicited

Referenced by (3)

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

Christine Paulin-Mohring → memberOf → Inria–Université Paris-Sud–CNRS research community around Coq ⓘ

Coq → hasCommunity → Coq development team ⓘ

linked to: Inria–Université Paris-Sud–CNRS research community around Coq

Matthieu Sozeau → affiliation → Coq development team ⓘ