In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures.

Property Value
dbo:abstract
  • In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures. The Association for Computing Machinery presented Coquand, Huet, Paulin-Mohring, Barras, Filliâtre, Herbelin, Murthy, Bertot, Castéran with the 2013 ACM Software System Award for Coq. (en)
  • Coq (gallo en francés) es un sistema de ayuda para la demostración de teoremas que maneja aserciones matemáticas, verifica mecánicamente las pruebas de aserciones, ayuda a encontrar pruebas para esas aserciones y extrae programas certificados (correctos) a partir de las pruebas constructivas de aserciones que representan su especificación formal. Coq trabaja basándose en la teoría del Cálculo de Construcciones Inductivas, que es una teoría derivada del Cálculo de Construcciones. Fue desarrollado en Francia, en el proyecto LogiCal, entre el INRIA, la École Polytechnique, la Universidad París XI y el CNRS. Dirigen el desarrollo los investigadores Gilles Dowek y Christine Paulin-Mohring. Coq está escrito en el lenguaje Ocaml. (es)
  • Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 d'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!. Coq a été récompensé du ACM SIGPLAN Programming Languages Software 2013 Award. (fr)
  • Coq ist ein Programm zum maschinengestützten Beweisen mathematischer Aussagen. (de)
  • Coqは証明支援システムの一つ。Coqの核はプログラミング言語Gallinaを用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。 (ja)
  • Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina) с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ. Coq разработан во Франции в рамках проекта TypiCal (ранее — LogiCal), совместно управляемом INRIA, Политехнической школой, Университетом Париж-юг XI и Национальным центром научных исследований, ранее была выделенная группа и в Высшей нормальной школе Лиона. Теоретической базой Coq считается исчисление конструкций; в названии скрыта его аббревиатура (CoC, англ. calculus of constructions) и сокращение от фамилии создателя исчисления — Тьерри Кокана. (ru)
  • Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明中提取出可验证的(certified)程序。Coq 的理论基础是归纳构造演算(calculus of inductive constructions)、一种构造演算(calculus of constructions)的衍生理论。Coq 并非一个自动化定理机器证明语言;然而,它提供了自动化定理证明的策略(tactics)和不同的决策过程。 Coq 同时还是一个依赖类型的函数式编程语言。它由法国PPS实验室的PI.R2团队研究开发,该团队由INRIA、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学和法国国家科学研究中心组成。此前里昂高等师范学校亦曾参与开发。Coq 项目当前由 Gérard Huet、Christine Paulin 和 Hugo Herbelin领导。Coq 使用 OCaml 以及少部分 C 实现。 单词 coq 在法语中意为"公鸡",此命名体现了法国在研究活动中使用动物名称命名工具的传统。 最初,它被简单地称作 Coc,意即构造演算(calculus of constructions)的缩写,同时也暗含了 Thierry Coquand(与 Gérard Huet 共同提出了前述的构造演算)的姓氏。 Coq 自身提供了一套规范语言 Gallina。使用 Gallina 书写的程序具有规范化性质——它们总是会终止。此性质使之避开了停机问题。同时,这也使得 Coq 语言本身并非图灵完全。 (zh)
dbo:genre
dbo:latestReleaseDate
  • 2016-07-11 (xsd:date)
dbo:latestReleaseVersion
  • 8.5pl2
dbo:license
dbo:operatingSystem
dbo:programmingLanguage
dbo:status
  • Active
dbo:thumbnail
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 581974 (xsd:integer)
dbo:wikiPageRevisionID
  • 741581345 (xsd:integer)
dbp:developer
  • The Coq development team
dbp:dialects
dbp:fileExt
  • .v
dbp:language
  • English
dbp:logo
dbp:paradigm
  • Functional
dbp:turingComplete
  • No
dbp:typing
dbp:year
  • 1984 (xsd:integer)
dct:subject
http://purl.org/linguistics/gold/hypernym
rdf:type
rdfs:comment
  • Coq ist ein Programm zum maschinengestützten Beweisen mathematischer Aussagen. (de)
  • Coqは証明支援システムの一つ。Coqの核はプログラミング言語Gallinaを用いる。フランス国立情報学自動制御研究所のPI.R2チーム(PPS研究所内にある)が、エコール・ポリテクニーク、フランス国立工芸院、パリ第7大学、パリ第11大学と(かつてリヨン高等師範学校とも)共同して開発している。Hugo Herbelinが事実上の開発代表者である。 (ja)
  • In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures. (en)
  • Coq (gallo en francés) es un sistema de ayuda para la demostración de teoremas que maneja aserciones matemáticas, verifica mecánicamente las pruebas de aserciones, ayuda a encontrar pruebas para esas aserciones y extrae programas certificados (correctos) a partir de las pruebas constructivas de aserciones que representan su especificación formal. Coq trabaja basándose en la teoría del Cálculo de Construcciones Inductivas, que es una teoría derivada del Cálculo de Construcciones. (es)
  • Coq est un assistant de preuve utilisant le langage Gallina, développé par l'équipe PI.R2 d'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!. (fr)
  • Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем, использующее собственный язык функционального программирования (Gallina) с зависимыми типами. Позволяет записывать математические теоремы и их доказательства, удобно модифицировать их, проверяет их на правильность. Пользователь интерактивно создаёт доказательство сверху вниз, начиная с цели (то есть от гипотезы, которую необходимо доказать). Coq может автоматически находить доказательства в некоторых ограниченных теориях с помощью так называемых тактик. Coq применяется для верификации программ. (ru)
  • Coq 是一个交互式的定理证明辅助工具。它允许用户输入包含数学断言的表达式、机械化地对这些断言执行检查、帮助构造形式化的证明、并从其形式化描述的构造性证明中提取出可验证的(certified)程序。Coq 的理论基础是归纳构造演算(calculus of inductive constructions)、一种构造演算(calculus of constructions)的衍生理论。Coq 并非一个自动化定理机器证明语言;然而,它提供了自动化定理证明的策略(tactics)和不同的决策过程。 Coq 同时还是一个依赖类型的函数式编程语言。它由法国PPS实验室的PI.R2团队研究开发,该团队由INRIA、巴黎综合理工学院、巴黎第十一大学、巴黎第七大学和法国国家科学研究中心组成。此前里昂高等师范学校亦曾参与开发。Coq 项目当前由 Gérard Huet、Christine Paulin 和 Hugo Herbelin领导。Coq 使用 OCaml 以及少部分 C 实现。 单词 coq 在法语中意为"公鸡",此命名体现了法国在研究活动中使用动物名称命名工具的传统。 最初,它被简单地称作 Coc,意即构造演算(calculus of constructions)的缩写,同时也暗含了 Thierry Coquand(与 Gérard Huet 共同提出了前述的构造演算)的姓氏。 (zh)
rdfs:label
  • Coq (en)
  • Coq (Software) (de)
  • Coq (es)
  • Coq (logiciel) (fr)
  • Coq (ja)
  • Coq (ru)
  • Coq (zh)
owl:sameAs
prov:wasDerivedFrom
foaf:depiction
foaf:homepage
foaf:isPrimaryTopicOf
foaf:name
  • Coq (software) (en)
is dbo:influenced of
is dbo:influencedBy of
is dbo:wikiPageRedirects of
is foaf:primaryTopic of