Coq (소프트웨어)

Coq (소프트웨어)
개발자	코크 개발팀
최초출시	1989년 5월 1일; 34년 전( (버전 4.10)
안정적인 방출	8.18.0 / 2023년 9월 8일, 2개월 전
저장소	github.com/coq/coq
작성자	OCaml
운영체제	크로스 플랫폼
에서 사용 가능	영어
유형	증명도우미
면허증.	LGPLv2.1
웹사이트	coq.inria.fr

코크는 1989년에 처음 발표된 상호작용 정리 속담입니다. 수학적 주장을 표현할 수 있도록 하고, 이러한 주장의 증명을 기계적으로 확인하며, 공식 증명을 찾는 데 도움을 주며, 공식 사양의 건설적인 증명에서 인증된 프로그램을 추출합니다. Coq는 귀납적 구성의 미적분학 이론 내에서 작동하며, 구성의 미적분학의 파생물입니다. Coq는 자동화된 정리 속담은 아니지만 자동 정리 증명 전술(절차)과 다양한 결정 절차를 포함합니다.

컴퓨터 기계 협회는 티에리 코캉, 제라드 휴트, 크리스틴 폴린 모링, 브루노 바라스, 장 크리스토프 필리트르, 휴고 허벨린, 체탄 머시, 이브 베르토, 피에르 카스테란에게 2013년 ACM 소프트웨어 시스템 상을 수여했습니다.

"Coq"라는 이름은 티에리 코캉드(Thierry Coquand), 건설 미적분학 또는 CoC(CoC)의 이름을 딴 말장난으로, 소프트웨어의 이름을 동물의 이름으로 짓는 프랑스 컴퓨터 과학 전통(프랑스어로 coq는 수탉을 의미함)을 따릅니다.^[2]

개요

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

coq라는 이름은 프랑스어로 '우렁이'를 의미하며, 연구 개발 도구에 동물 이름을 붙이는 프랑스 전통에서 유래했습니다.^[5] 1991년까지 Coquand는 Constructions의 미적분학이라고 불리는 언어를 구현하고 있었고, 이 당시에는 단순히 CoC라고 불렸습니다. 1991년, 확장된 귀납적 구성의 미적분학에 기초한 새로운 구현이 시작되었고, 제라드 휴트와 함께 구성의 미적분학을 개발하고 크리스틴 폴린-모링과 함께 귀납적 구성의 미적분학에 기여한 코콴드에 대한 간접적인 언급으로 이름이 CoC에서 Coq로 변경되었습니다.^[6]

Coq는 Gallina^[7](라틴어, 스페인어, 이탈리아어, 카탈루냐어로 "hen")라는 사양 언어를 제공합니다. Gallina로 작성된 프로그램은 정규화 속성이 약해 항상 종료됩니다. 이것은 다른 프로그래밍 언어에서 무한 루프(비종료 프로그램)가 일반적이며 중단 ^[8]문제를 피하는 한 가지 방법이기 때문에 언어의 독특한 특성입니다.

예를 들어, 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_ S H)      (m + S y)      (플러스_n_Sm m y)) n      : 만고의 n m : 낫, n + m = m + n

nat_ind 는 수학적 귀납법을 의미합니다. eq_ind 등분 대체를 위해, 그리고 f_equal 평등의 양쪽에서 동일한 기능을 수행하기 위해. $m=m+0$ = $m=m+0$ + $m=m+0$ 0 $displaystyle$ m = m $+0$ } 및 S(m + y ) = m + Sy {\displaystyle S(m + y) = m을 표시하는 이전 정리를 참조합니다. $+Sy$

주목할 만한 용도

4색 정리 및 SSR 반사 확장

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

한 개 또는 두 개의 컨스트럭터가 있는 유도 유형에 대한 반박 및 반박 패턴 매칭을 위한 추가 편리한 표기법
고차 함수로 프로그래밍할 때 유용한 0 인수에 적용되는 함수에 대한 암시적 인수
간결한 익명의 논법
개선된 set 더 강력한 일치를 보이는 전술
반사 지지

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

기타 응용프로그램

CompCert: 대부분 C 프로그래밍 언어를 위한 최적화 컴파일러로, COq에서 정확한 것으로 입증되었습니다.
이산 집합 데이터 구조: Coq의 정확성 증명은 2007년에 발표되었습니다.^[12]
Feit-Thompson 정리: Coq를 사용한 공식적인 증명은 2012년 9월에 완료되었습니다.^[13]

참고 항목

참고문헌

^ "Release 8.18.0". 8 September 2023. Retrieved 18 September 2023.
^ "Alternative names · coq/coq Wiki". GitHub. Retrieved 3 March 2023.
^ Coq에 대한 간단한 소개
^ Avigad, Jeremy; Mahboubi, Assia (3 July 2018). Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as ... Springer. ISBN 9783319948218. Retrieved 21 October 2018.
^ "Frequently Asked Questions". GitHub. Retrieved 2019-05-08.
^ "Introduction to the Calculus of Inductive Constructions". Retrieved 21 May 2019.
^ 아담 클리팔라. "의존형으로 인증된 프로그래밍": "도서관 대학".
^ 아담 클리팔라. "의존형으로 인증된 프로그래밍": "도서관 General Rec". "도서관 유도형".
^ 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". GitHub.
^ Conchon, Sylvain; Filliâtre, Jean-Christophe (October 2007), "A Persistent Union-Find Data Structure", ACM SIGPLAN Workshop on ML, Freiburg, Germany{{citation}}: CS1 maint: 위치 누락 게시자(링크)
^ "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 proof assist – 공식 영어 웹사이트
coq/coq – GitHub에 있는 프로젝트의 소스 코드 저장소
JsCoq Interactive Online System – 별도의 소프트웨어 설치 없이 웹 브라우저에서 Coq를 실행할 수 있습니다.
Allectryon – 문서에 포함된 Coq 스니펫을 처리하는 라이브러리로, 각 Coq 문장에 대한 목표와 메시지를 보여줍니다.
코크 위키
Mathematical Components 라이브러리 – 널리 사용되는 수학적 구조의 라이브러리(SSR 반사 증명 언어)
Nijmegen의 건설적인 Coq 저장소
수학 수업
코캣 오픈 허브

교재

Coq'Art – Yves Bertot과 Pierre Castéran의 Coq에 관한 책
종속 유형 인증 프로그래밍 – Adam Chlipala의 온라인 및 인쇄 교재
소프트웨어 재단 – Benjamin C의 온라인 교과서. 피어스 외.
Coq의 소규모 성찰 소개 - Georges Gonthier와 Assia Mahboubi의 SSR 성찰 튜토리얼

자습서

Coq Proof Assistant 소개 – Andrew Appel Institute for Advanced Study의 비디오 강의
안드레이 바우어의 코크 프루프 어시스턴트 비디오 튜토리얼.

[wikidata-c1ecbf83f6185aad89e83bfdcd1d9fb3e402f207-v9-1] "Release 8.18.0". 8 September 2023. Retrieved 18 September 2023.

[2] "Alternative names · coq/coq Wiki". GitHub. Retrieved 3 March 2023.

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

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

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

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

[7] 아담 클리팔라. "의존형으로 인증된 프로그래밍": "도서관 대학".

[8] 아담 클리팔라. "의존형으로 인증된 프로그래밍": "도서관 General Rec". "도서관 유도형".

[: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". GitHub.

[12] Conchon, Sylvain; Filliâtre, Jean-Christophe (October 2007), "A Persistent Union-Find Data Structure", ACM SIGPLAN Workshop on ML, Freiburg, Germany{{citation}}: CS1 maint: 위치 누락 게시자(링크)

[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