This HTML5 document contains 143 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dbpedia-elhttp://el.dbpedia.org/resource/
n36https://www.zhihu.com/topic/
dbpedia-fihttp://fi.dbpedia.org/resource/
dbrhttp://dbpedia.org/resource/
n31http://dx.doi.org/10.5281/
n12http://fr.dbpedia.org/resource/Modèle:
schemahttp://schema.org/
n23http://commons.wikimedia.org/wiki/Special:FilePath/
n6http://
n38https://directory.fsf.org/wiki/
dbpedia-frhttp://fr.dbpedia.org/resource/
n18https://www.openhub.net/p/
n35https://github.com/
dcthttp://purl.org/dc/terms/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n48http://www.pps.univ-paris-diderot.fr/pi.r2/
n21http://g.co/kg/m/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n16http://babelnet.org/rdf/
xsdhhttp://www.w3.org/2001/XMLSchema#
dbpedia-ukhttp://uk.dbpedia.org/resource/
n46https://packages.debian.org/stable/
n34http://www.labri.fr/perso/casteran/CoqArt/
prop-frhttp://fr.dbpedia.org/property/
n29https://packages.ubuntu.com/
dbohttp://dbpedia.org/ontology/
n15https://ncatlab.org/nlab/show/
dbpedia-pthttp://pt.dbpedia.org/resource/
dbpedia-jahttp://ja.dbpedia.org/resource/
n10https://www.archlinux.org/packages/
n25https://www.irif.fr/inria/pi.r2/
n33http://commons.dbpedia.org/resource/Category:
n27https://framalibre.org/content/
dbpedia-dehttp://de.dbpedia.org/resource/
dbpedia-ruhttp://ru.dbpedia.org/resource/
wikidatahttp://www.wikidata.org/entity/
n47https://www.quora.com/topic/
n43https://commons.wikimedia.org/wiki/Category:
n28https://packages.gentoo.org/packages/sci-mathematics/
n24https://apps.fedoraproject.org/packages/
provhttp://www.w3.org/ns/prov#
foafhttp://xmlns.com/foaf/0.1/
wikipedia-frhttp://fr.wikipedia.org/wiki/
dbpedia-zhhttp://zh.dbpedia.org/resource/
n42http://coq.inria.fr/
n9http://fileformats.archiveteam.org/wiki/
dbpedia-eshttp://es.dbpedia.org/resource/
category-frhttp://fr.dbpedia.org/resource/Catégorie:
owlhttp://www.w3.org/2002/07/owl#

Statements

Subject Item
dbpedia-fr:Coq_(logiciel)
rdf:type
schema:CreativeWork owl:Thing wikidata:Q7397 dbo:Work dbo:Software wikidata:Q386724
rdfs:label
Coq Coq (logiciel) Coq Coq (Software)
rdfs:comment
Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 de l’Inria au sein du laboratoire PPS du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université Paris-Sud (et antérieurement l'École normale supérieure de Lyon). Le nom du logiciel (initialement CoC) est particulièrement adéquat car : il est français ; il est fondé sur le calcul des constructions (CoC abrégé en anglais) introduit par Thierry Coquand. Dans la même veine, son langage est Gallina et Coq possède un wiki dédié, baptisé Cocorico!.
rdfs:seeAlso
n9:Coq n10:coq n10:coq-doc n10:coqide n15:Coq n18:coq n24:coq n27:coq n28:coq n29:coq n35:coq n36:20008098 n38:Coq n43:Coq_(programming_language) n46:coq n47:Coq-proof-assistant
owl:sameAs
dbr:Coq dbpedia-fi:Coq n16:s03400740n n21:02s7zd dbpedia-de:Coq_(Software) dbpedia-ja:Coq n31:ZENODO.1003420 dbpedia-el:Coq n33:Coq_(programming_language) dbpedia-pt:Coq wikidata:Q1131652 dbpedia-uk:Coq dbpedia-zh:Coq dbpedia-es:Coq dbpedia-ru:Coq
dbo:wikiPageID
86532
dbo:wikiPageRevisionID
191087028
dbo:wikiPageWikiLink
dbpedia-fr:P_Hpair%5D dbpedia-fr:C_(langage) dbpedia-fr:Anglais dbpedia-fr:École_normale_supérieure_de_Lyon dbpedia-fr:Christine_Paulin-Mohring dbpedia-fr:Correspondance_de_Curry-Howard dbpedia-fr:Mizar_(système) dbpedia-fr:Benjamin_Werner dbpedia-fr:PhoX_(logiciel) dbpedia-fr:Calcul_des_constructions dbpedia-fr:Isabelle_(logiciel) dbpedia-fr:Logiciel_libre dbpedia-fr:Open_source dbpedia-fr:Théorème_de_Feit-Thompson dbpedia-fr:Démonstration_automatique_de_théorèmes dbpedia-fr:Institut_national_de_recherche_en_informatique_et_en_automatique category-fr:Assistant_de_preuve category-fr:Théorie_de_la_démonstration dbpedia-fr:Assistant_de_preuve dbpedia-fr:École_polytechnique_(France) dbpedia-fr:Centre_national_de_la_recherche_scientifique dbpedia-fr:Environnement_de_développement dbpedia-fr:Licence_publique_générale_limitée_GNU category-fr:Théorie_des_types dbpedia-fr:CompCert dbpedia-fr:Oméga_(procédure_de_décision) dbpedia-fr:Chaînage_arrière dbpedia-fr:Théorème_des_quatre_couleurs dbpedia-fr:Conservatoire_national_des_arts_et_métiers dbpedia-fr:Gallina category-fr:Logiciel_libre_sous_licence_LGPL dbpedia-fr:Logique_d'ordre_supérieur dbpedia-fr:Théorie_des_types dbpedia-fr:Gérard_Huet dbpedia-fr:OCaml dbpedia-fr:Arithmétique_de_Presburger dbpedia-fr:Université_Paris-Sud dbpedia-fr:Special_Interest_Group_on_Programming_Languages dbpedia-fr:Georges_Gonthier dbpedia-fr:Université_Paris-Diderot dbpedia-fr:Thierry_Coquand dbpedia-fr:Lambda-calcul dbpedia-fr:Langage_de_programmation dbpedia-fr:Prototype_Verification_System
dbo:wikiPageExternalLink
n6:www.pps.univ-paris-diderot.fr n25:index n34:coqartF.pdf n42: n42:cocorico n48:
dbo:wikiPageLength
9106
dct:subject
category-fr:Assistant_de_preuve category-fr:Théorie_des_types category-fr:Théorie_de_la_démonstration category-fr:Logiciel_libre_sous_licence_LGPL
foaf:name
prop-fr:wikiPageUsesTemplate
n12:En n12:Infobox_Logiciel n12:Références n12:Portail n12:Fr n12:Oui n12:Voir_homonymes n12:Ébauche n12:Github n12:Blanc
prov:wasDerivedFrom
wikipedia-fr:Coq_(logiciel)?oldid=191087028&ns=0
foaf:depiction
n23:Coq_logo.png n23:CoqProofOfDecidablityOfEqualityOnNaturalNumbers.png
prop-fr:couleurBoîte
CBA275
prop-fr:légende
CoqIde : l'environnement de développement de Coq.
prop-fr:type
dbpedia-fr:Assistant_de_preuve
prop-fr:langues
dbpedia-fr:Anglais
prop-fr:licence
dbpedia-fr:Licence_publique_générale_limitée_GNU
prop-fr:logo
Coq logo.png
prop-fr:politiqueDePrix
Gratuit et open source
prop-fr:développeurs
dbpedia-fr:École_normale_supérieure_de_Lyon dbpedia-fr:Université_Paris-Sud dbpedia-fr:Université_Paris-Diderot dbpedia-fr:École_polytechnique_(France) dbpedia-fr:Institut_national_de_recherche_en_informatique_et_en_automatique
prop-fr:environnements
-
dbo:thumbnail
n23:Coq_logo.png?width=300
foaf:isPrimaryTopicOf
wikipedia-fr:Coq_(logiciel)
dbo:abstract
Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 de l’Inria au sein du laboratoire PPS du CNRS et en partenariat avec l'École polytechnique, le CNAM, l'Université Paris Diderot et l'Université Paris-Sud (et antérieurement l'École normale supérieure de Lyon). Le nom du logiciel (initialement CoC) est particulièrement adéquat car : il est français ; il est fondé sur le calcul des constructions (CoC abrégé en anglais) introduit par Thierry Coquand. Dans la même veine, son langage est Gallina et Coq possède un wiki dédié, baptisé Cocorico!. En 2013, Coq a été récompensé du Programming Languages Software Award par l'ACM SIGPLAN. Coq a reçu en 2022 le premier « prix science ouverte logiciel libre de la recherche » dans la catégorie « scientifique et technique ».
dbo:award
wikidata:Q110827069 wikidata:Q61890391
dbo:computingPlatform
dbpedia-fr:Logiciel_multiplateforme
dbo:country
dbpedia-fr:France
dbo:developer
dbpedia-fr:Institut_national_de_recherche_en_informatique_et_en_automatique
dbo:language
dbpedia-fr:Anglais
dbo:license
wikidata:Q18534390 dbpedia-fr:Licence_publique_générale_limitée_GNU
dbo:publisher
dbpedia-fr:École_polytechnique_(France) dbpedia-fr:Université_Paris-Sud dbpedia-fr:Université_Paris-Diderot dbpedia-fr:Institut_national_de_recherche_en_informatique_et_en_automatique dbpedia-fr:École_normale_supérieure_de_Lyon
dbo:type
dbpedia-fr:Assistant_de_preuve