동작

Coq(소프트웨어)
개발자	Coq 개발팀
초기 릴리즈	1989년 5월 1일; 33년전( (버전 4.10)
안정된 릴리스	8.15.2 / 2022년 5월 31일; 2개월 전 ()
저장소	github.com/coq/coq
기입처	OCaml
운영 체제	크로스 플랫폼
이용가능기간:	영어
유형	프루프 어시스턴트
면허증.	LGPLv2.1
웹 사이트	coq.inria.fr

Coq의 대화형 증명 세션IDE: 왼쪽에 프루프 스크립트가 표시되고 오른쪽에 프루프 상태가 표시됩니다.

Coq는 1989년에 처음 출시된 인터랙티브 정리 프로버입니다.수학적 주장을 표현하고, 이러한 주장의 증거를 기계적으로 체크하고, 공식 증거를 찾는 데 도움을 주며, 공식 명세서의 구성적 증명에서 인증된 프로그램을 추출합니다.Coq는 구성 미적분의 파생물인 귀납적 구성 미적분 이론 내에서 작동합니다.Coq는 자동정리프로버는 아니지만 자동정리증명전술(절차)과 다양한 결정절차를 포함한다.

컴퓨팅 머신 협회(Association for Computing Machine)는 2013년 ACM 소프트웨어 어워드에서 티에리 코캉, 제라르 훼, 크리스틴 폴랭-모링, 브루노 바라, 장 크리스토프 필리아트르, 휴고 헤르벨린, 체탄 머시, 이브 베르토, 피에르 카스테랑을 수상했습니다.

Coq는 Tierry Coquand, 건설 미적분 또는 CoC의 이름에 대한 단어 놀이이며, 도구의 이름을 동물의 이름을 따서 짓는 프랑스 전통에 따르고 있습니다.^[2]

개요

프로그래밍 언어로 볼 때 Coq는 의존적으로 유형화된 ^[3]함수 프로그래밍 언어를 구현하고, 논리 시스템으로 볼 때 고차 유형 이론을 구현합니다.Coq의 개발은 1984년부터 INRIA가 지원하고 있으며, 현재는 에콜 폴리테크니크, 파리 수드 대학, 파리 디드로 대학 및 CNRS와 협력하고 있습니다.1990년대에는 ENS Lyon도 이 프로젝트의 일부였습니다.Coq의 개발은 제라르 후에와 티에리 코캉이 주도했으며, 개발 초기부터 40명 이상의 연구자들이 핵심 시스템에 특징을 부여했다.구현팀은 제라르 휴에, 크리스틴 폴린 모링, 휴고 허벨린, 마티유 소조에 의해 연속적으로 조정되었습니다.Coq는 주로 약간의 C를 가진 OCaml에서 구현됩니다.코어 시스템은 플러그인 ^[4]메커니즘을 통해 확장할 수 있습니다.

coq라는 이름은 프랑스어로 "rooster"를 의미하며 연구 개발 도구에 ^[5]동물의 이름을 붙이는 프랑스의 전통에서 유래했다.1991년까지, Coquand는 건설의 미적분이라고 불리는 언어를 실행하고 있었고, 그것은 이 시기에 CoC라고 불렸다.1991년 확장 미적분에 기초한 새로운 구현이 시작되었고, 제라르 훼와 함께 구성 미적분을 개발하고 크리스틴 폴린 모링과 함께 ^[6]귀납적 구성 미적분에 기여한 코콴드를 간접적으로 언급하여 CoC에서 Coq로 이름을 변경하였다.

Coq는 갈리나(라틴어, 스페인어, 이탈리아어, 카탈로니아어로 "헨")라고^[7] 불리는 사양 언어를 제공합니다.갈리나어로 작성된 프로그램은 정규화 특성이 약하며, 이는 항상 종료된다는 것을 의미합니다.무한 루프(종단되지 않는 프로그램)는 다른 프로그래밍 ^[8]언어에서 공통적으로 사용되기 때문에 이는 언어의 고유한 속성이며 정지 문제를 회피하는 한 가지 방법입니다.

4색 정리 및 SSRefect 확장

영국 캠브리지에 있는 마이크로소프트 리서치의 조르주 곤티에와 INRIA의 벤자민 베르너는 Coq를 사용하여 4색 정리에 대한 측량 가능한 증거를 만들었고,^[9] 이는 2002년에 완성되었다.이들의 작업은 SSReflex("Small Scale Reflection") 패키지의 개발로 이어졌으며, 이는 Coq의 ^[10]중요한 확장이었습니다.이름에도 불구하고 SSReflex에 의해 Coq에 추가된 대부분의 기능은 범용 기능이며 증명의 계산 반영 스타일에 국한되지 않습니다.이러한 기능은 다음과 같습니다.

1개 또는 2개의 컨스트럭터가 있는 유도형 패턴에 대해 반박할 수 없는 패턴 및 반박할 수 있는 패턴 매칭을 위한 추가 편리한 표기
제로 인수에 적용되는 함수에 대한 암묵적 인수. 고차 함수를 사용하여 프로그래밍할 때 유용합니다.
간결한 익명 인수
개량된set보다 강력한 궁합을 가진 전술
반영 지원

SSRefelect 1.11은 무료로 사용할 수 있으며, 오픈 소스 CeCIL-B 또는 CeCIL-2.0 라이센스로 이중 라이센스가 있으며 Coq 8.11과 ^[11]호환됩니다.

적용들

CompCert: Coq에서 주로 프로그래밍되고 증명된 거의 모든 C 프로그래밍 언어를 위한 최적화 컴파일러입니다.
Disconsulated-set data structure: Coq의 정확성 증명은 ^[12]2007년에 발표되었다.
Feit-Thompson 정리: Coq를 사용한 공식 증명은 2012년 ^[13]9월에 완료되었습니다.
Coq를 사용한 공식 증명이라는 4색 정리가 2005년에 ^[9]완성되었습니다.

「」를 참조해 주세요.

레퍼런스

^ "Release Coq 8.15.2". 31 May 2022. Retrieved 4 June 2022.
^ "Alternative names · coq/coq Wiki". GitHub. Retrieved 2021-11-11.
^ Coq에 대한 간단한 소개
^ Avigad, Jeremy; Mahboubi, Assia (3 July 2018). Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as ... ISBN 9783319948218. Retrieved 21 October 2018.
^ "Frequently Asked Questions". Retrieved 2019-05-08.
^ "Introduction to the Calculus of Inductive Constructions". Retrieved 21 May 2019.
^ 아담 치팔라."인정된 종속형 프로그래밍": "라이브러리 유니버스"
^ 아담 치팔라.「인정된 프로그래밍과 의존 타입」: 「라이브러리 GeneralRec」."라이브러리 유도형"
^ ^a ^b Gonthier, Georges (2008), "Formal Proof—The Four-Color Theorem" (PDF), Notices of the American Mathematical Society, vol. 55, no. 11, pp. 1382–1393, MR 2463991
^ 조르주 곤티에, 아시아 마흐부비"Coq에서의 소규모 성찰 소개": "정식화된 추리 저널"
^ "The Mathematical Components Library 1.11.0".
^ Conchon, Sylvain; Filliâtre, Jean-Christophe (October 2007), "A Persistent Union-Find Data Structure", ACM SIGPLAN Workshop on ML, Freiburg, Germany
^ "Feit-Thompson theorem has been totally checked in Coq". Msr-inria.inria.fr. 2012-09-20. Archived from the original on 2016-11-19. Retrieved 2012-09-25.

외부 링크

Coq 인증 어시스턴트– 공식 영어 웹사이트
coq/coq – 프로젝트의 소스 코드 저장소 GitHub
JsCoq Interactive Online System – 소프트웨어 설치 없이 Coq를 웹 브라우저에서 실행할 수 있습니다.
Alexryon – 문서에 내장된 Coq 스니펫을 처리하는 라이브러리. 각 Coq 문장의 목표와 메시지를 보여줍니다.
Coq 위키
수학 컴포넌트 라이브러리– 널리 사용되는 수학 구조 라이브러리. SSRelect 증명 언어도 포함되어 있습니다.
Nijmegen의 Constructive Coq 저장소
수학 수업
오픈 허브에서의 Coq

교재

The Coq'Art – 이브 베르토와 피에르 카스테랑의 Coq에 관한 책
Adam Chlipala의 온라인 및 인쇄된 교재(종류별)에 의한 인정 프로그래밍
소프트웨어 재단– Benjamin C의 온라인 교과서 피어스 등
Coq에서의 소규모 성찰 소개– Georges Gonthier와 Assia Mahboubi의 SSReflect에 대한 튜토리얼

튜토리얼

Coq Proof Assistant 소개– Advanced Study Institute의 Andrew Appel 비디오 강의
Andrej Bauer의 Coq 인증 어시스턴트 비디오 튜토리얼.

[wikidata-4bbcf9a62f0de81266378e4f0fdd76c1a5b2a7f4-v3-1] "Release Coq 8.15.2". 31 May 2022. Retrieved 4 June 2022.

[2] "Alternative names · coq/coq Wiki". GitHub. Retrieved 2021-11-11.

[3] Coq에 대한 간단한 소개

[4] Avigad, Jeremy; Mahboubi, Assia (3 July 2018). Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as ... ISBN 9783319948218. Retrieved 21 October 2018.

[5] "Frequently Asked Questions". Retrieved 2019-05-08.

[6] "Introduction to the Calculus of Inductive Constructions". Retrieved 21 May 2019.

[7] 아담 치팔라."인정된 종속형 프로그래밍": "라이브러리 유니버스"

[8] 아담 치팔라.「인정된 프로그래밍과 의존 타입」: 「라이브러리 GeneralRec」."라이브러리 유도형"

[:0-9] Gonthier, Georges (2008), "Formal Proof—The Four-Color Theorem" (PDF), Notices of the American Mathematical Society, vol. 55, no. 11, pp. 1382–1393, MR 2463991

[10] 조르주 곤티에, 아시아 마흐부비"Coq에서의 소규모 성찰 소개": "정식화된 추리 저널"

[11] "The Mathematical Components Library 1.11.0".

[12] Conchon, Sylvain; Filliâtre, Jean-Christophe (October 2007), "A Persistent Union-Find Data Structure", ACM SIGPLAN Workshop on ML, Freiburg, Germany

[13] "Feit-Thompson theorem has been totally checked in Coq". Msr-inria.inria.fr. 2012-09-20. Archived from the original on 2016-11-19. Retrieved 2012-09-25.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

Search

동작

네임스페이스

더

목차

개요

4색 정리 및 SSRefect 확장

적용들

「」를 참조해 주세요.

레퍼런스

외부 링크

Coq의 자연수에 대한 덧셈의 교환성 증명.
플러스_콤 = 재밌어요 n m : 내트 => nat_ind (재밌어요 n0 : 내트 => n0 + m = m + n0) (플러스_n_0 m) (재밌어요 (y : 내트) (H : y + m = m + y) => eq_ind (S (m + y)) (재밌어요 n0 : 내트 => S (y + m) = n0) (f_filename(f_filename(f_module) S H) (m + S y) (플러스_n_Sm m y)) n : 전면적으로 n m : 내트, n + m = m + n
`nat_ind`수학적 귀납을 의미하고`eq_ind`대등하게 치환하기 위해`f_equal`평등 양쪽에서 동일한 기능을 취하기 때문입니다.이전 정리에서는 m $m=m+0$ + $m=m+0$ ({ $displaystyle$ m $=$ $m+0})$ 및 $m=m+0$ $S(m+y)=m+Sy$ + $S(m+y)=m+Sy$ ) $S(m+y)=m+Sy$ + $({displaystyle$ S $(m+y$ )= $m$ 을 $m=m+0$ . $+Sy$

Search

동작

개요

4색 정리 및 SSRefect 확장

적용들

「 」를 참조해 주세요.

레퍼런스

외부 링크

「」를 참조해 주세요.