이론 컴퓨터 과학의 중요 출판물 목록

이 글에는 여러 가지 문제가 있다. 이 문제를 개선하거나 대화 페이지에서 토의하십시오. (이러한 템플릿 메시지를 제거하는 방법 및 시기 알아보기) 이 글은 검증을 위해 인용구가 추가로 필요하다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선할 수 있도록 도와주십시오. 공급되지 않은 재료는 도전하여 제거할 수 있다. 출처 찾기: "이론 컴퓨터 과학 분야의 중요 출판물 목록" – 뉴스 · 신문 · 책 · 학자 · JSTOR (2015년 2월) (이 템플릿 메시지를 제거하는 방법과 시기 학습) 이 글에는 아마도 독창적인 연구가 포함되어 있을 것이다. 클레임을 확인하고 인라인 인용문을 추가하여 개선하십시오. 원본 연구로만 구성된 문장은 제거해야 한다. (2015년 2월) (이 템플릿 메시지를 제거하는 방법과 시기 학습) 이 기사는 위키피디아의 품질 기준을 충족시키기 위해 정리가 필요할 수 있다. 구체적인 문제는: 목록에는 객관적으로 발표된 지원 없이 항목별로 제시되며, 여기에는 그 중요성을 확립하는 출처가 뒷받침하지 않는 주요 문헌의 기사 선정이 포함된다(즉, WP 구성:OR. 가능한 경우 이 문서를 개선하는 데 도움을 주십시오. (2015년 2월) (이 템플리트 메시지를 제거하는 방법 및 시기 알아보기) (이 템플릿 메시지를 제거하는 방법 및 시기 알아보기)

분야별로 정리된 이론 컴퓨터 과학의 중요 출판물 목록이다.

특정 출판물이 중요한 것으로 간주될 수 있는 몇 가지 이유:

• 주제 작성자 – 새로운 주제를 만든 출판물
• 획기적인 발전 – 과학 지식을 크게 변화시킨 출판물
• 영향 – 세계에 상당한 영향을 미쳤거나 이론 컴퓨터 과학의 교육에 막대한 영향을 미친 출판물.

계산성

Cutland의 계산 가능성: 재귀함수이론(Cambridge) 소개

• Cutland, Nigel J. (1980). Computability: An Introduction to Recursive Function Theory. Cambridge University Press. ISBN 978-0-521-29465-2.

퍼듀 대학의 칼 스미스(산업 및 응용 수학 평론 협회)가 작성한 이 초기의 본문을 보면,^[1] 이 본문은 "고전적 재귀 이론[RT]의 근본적 결과"를 하나의 스타일로 제시하는 "증거의 설명에 있어서 직관과 엄격함이 적절히 조화된" 본문을 보고한다. "수학적 배경은 최소한으로 학부생들이 접근할 수 있다." 그는 "수학생들을 위한 [RT] 입문 코스의 훌륭한 입문서가 될 것"이라고 말하면서도, 컴퓨터 공학 학생들과 함께 사용할 때 (이 영역에 대한 RT 응용에 대한 자료가 부족할 경우) "강사가 그 자료를 실질적으로 증가시킬 준비를 해야 한다"고 제안한다.^[1]

무한대 나무에서의 2차 이론과 자동화의 결정성

• 마이클 O. 라빈
• 미국수학회의 거래, 제141권, 페이지 1-35, 1969

설명: 그 논문은 자동화의 연장선인 나무 자동화를 제시했다. 나무 자동판매기는 프로그램의 정확성을 증명하는 수많은 응용 프로그램을 가지고 있었다.

유한한 자동화와 그 결정 문제

• 마이클 O. 라빈과 다나 S. 스콧
• IBM Journal of Research and Development, vol. 3, 페이지 114–125, 1959
• 온라인 버전

설명: 오토마타의 수학적 처리, 핵심 성질의 증명, 비결정론적 유한 자동화의 정의.

오토마타 이론, 언어 및 계산 소개

• 존 E. 홉크로프트, 제프리 D. 울만, 그리고 라지브 모트와니
• 애디슨-웨슬리, 2001년 ISBN 0-201-02988-X

설명: 인기 있는 교과서.

그래머의 특정 형식 특성에 대해

• Chomsky, N. (1959). "On certain formal properties of grammars". Information and Control. 2 (2): 137–167. doi:10.1016/S0019-9958(59)90362-6.

설명: 이 기사는 현재 공식 언어를 생성하는 격식어 클래스의 격납 계층인 촘스키 계층 구조로 알려진 것을 소개했다.

Entscheidungsproroblem에 대한 응용 프로그램이 있는 계산 가능한 숫자

• 앨런 튜링
• 런던 수학 학회의 절차, 시리즈 2, 42권, 페이지 230–265, 1937, doi:10.112/plms/s2-42.1.230.
  에라타는 제43권, 페이지 544–546, 1938, doi:10.112/plms/s2-43.6.544에 나타났다.
• HTML 버전, PDF 버전

설명: 이 글은 컴퓨터 과학의 한계를 정했다. 그것은 튜링 머신을 정의했다. 튜링 머신은 모든 연산을 위한 모델이다. 반면에, 그것은 중단 문제와 Entscheidungsproroblem의 불분명함을 증명했고 그렇게 함으로써 가능한 계산의 한계를 찾았다.

리쿠르시브 펑키티엔

• Péter, Rózsa (1951). Rekursive Funktionen. Academic Press. ISBN 9780125526500.

재귀함수 이론에 관한 첫 번째 교과서. 이 책은 많은 판을 거쳤고, 헝가리 정부로부터 페테르에게 코수스 상을 받았다.^[2] 라파엘 M. 로빈슨과 스티븐 클린의 리뷰는 이 책이 학생들에게 효과적인 초등학교 소개를 제공했다고 칭찬했다.^[3]

신경망과 유한 자동자극에서의 사건 표현

• S. C. 클레네
• 미 공군 프로젝트 랜드 연구 비망록 RM-704, 1951
• 온라인 버전
• 에 다시 게시된:

설명: 이 논문은 유한한 오토마타, 정규 표현, 정규 언어를 도입하여 그 연계를 확립하였다.

계산 복잡성 이론

Arora & Barak의 계산 복잡성과 Goldreich의 계산 복잡성(두 캠브리지 모두)

• 산제프 아로라와 보아즈 바락, "컴퓨팅 복잡성: A 모던 어프로치," 케임브리지 대학 출판부, 2009년, 579페이지, 하드커버
• Oedded Goldreich, "Computational Complexity: A 개념적 관점, Cambridge University Press, 2008, 606페이지, Hardcover

ACM의 'SIGACT 뉴스'에서는 ACM의 'SIGACT 뉴스'를 통해 이러한 최신 텍스트들을 "복합 이론의 과정을 위한 교과서, 조기 졸업을 목표로 한다"는 긍정적인 평가를 받고 있다.^[4] 고급 학부생들… 수많은 독특한 강점과 극소수의 약점이 있다."라고 말하며, 두 가지 모두 다음과 같이 말한다.

"컴퓨팅 복잡성 이론의 폭과 깊이를 철저히 다루는 저술가들... [각각]은 계산 이론상 거인이다. [각각 어디에 있을 것인가] ...분야의 전문가들을 위한 예외적인 참고문헌이다. [그리고 그것]어떤 학파의 이론가, 연구자, 그리고 강사들은 어느 책이든 유용하다는 것을 알게 될 것이다.

검토자는 "골드레이히가 제시된 각 개념에 대한 문맥적, 역사적 기초를 개발하는 데 더 중점을 두는 반면, [아로라와 바라크]에서는 매우 최신의 자료를 포함시키려는 확실한 시도가 있다"면서 "뛰어난 기여에 대해 모든 작가들을 인정한다"고 언급했다.^[4]

재귀 기능의 복잡성에 대한 기계 독립적인 이론

• Blum, Manuel (1967). "A Machine-Independent Theory of the Complexity of Recursive Functions" (PDF). Journal of the ACM. 14 (2): 322–336. doi:10.1145/321386.321395. S2CID 15710280.

설명: 블럼 공리는 공리.

대화형 증명 시스템을 위한 대수적 방법

• Lund, C.; Fortnow, L.; Karloff, H.; Nisan, N. (1992). "Algebraic methods for interactive proof systems". Journal of the ACM. 39 (4): 859–868. CiteSeerX 10.1.1.41.9477. doi:10.1145/146585.146605. S2CID 207170996.

설명: 이 논문은 PH가 IP에 포함되어 있다는 것을 보여주었다.

정리 증명 절차의 복잡성

• Cook, Stephen A. (1971). "The Complexity of Theorem-Proving Procedures" (PDF). Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158. CiteSeerX 10.1.1.406.395. doi:10.1145/800157.805047. S2CID 7573663.

설명: 본 논문은 NP-완전성 개념을 도입하여 부울 만족도 문제(SAT)가 NP-완전성임을 증명하였다. Levin, Universal Search Problems 에서 Leonid Levin에 의해 조금 후에 유사한 아이디어가 독립적으로 개발되었다는 점에 유의하십시오. Peremy Peredachi Informatsi 9(3):265–266, 1973"

컴퓨터와 난해성: NP-완전성 이론의 지침서

• Garey, Michael R.; Johnson, David S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. New York: Freeman. ISBN 978-0-7167-1045-5.

설명: 이 책의 가장 큰 중요성은 300개 이상의 NP-완전성 문제의 광범위한 목록 때문이다. 이 목록은 일반적인 참조와 정의가 되었다. 이 책이 출간된 지 불과 몇 년이 지나서야 이런 방대한 목록이 나왔다.

함수의 계산 난이도 및 재귀 집합의 부분 순서

• Rabin, Michael O. (1960). "Degree of difficulty of computing a function and a partial ordering of recursive sets" (PDF). Technical Report No. 2. Jerusalem: Hebrew University.

설명: 이 기술 보고서는 후에 컴퓨터 복잡성으로^[5] 이름이 바뀐 것에 대해 이야기하는 첫 번째 간행물이었다.

심플렉스 방법은 얼마나 좋은가?

• 빅터 클라이와 조지 J. 민티
• Klee, Victor; Minty, George J. (1972). "How good is the simplex algorithm?". In Shisha, Oved (ed.). Inequalities III (Proceedings of the Third Symposium on Inequalities held at the University of California, Los Angeles, Calif., September 1–9, 1969, dedicated to the memory of Theodore S. Motzkin). New York-London: Academic Press. pp. 159–175. MR 0332165.

설명: 치수 D에 "Klee-Minty 큐브"를 구성했으며, 선형 최적화를 위해 Dantzig의 심플렉스 알고리즘에 의해 각각 2개의^D 코너가 방문된다.

랜덤 함수를 구성하는 방법

• Goldreich, O.; Goldwasser, S.; Micali, S. (1986). "How to construct random functions" (PDF). Journal of the ACM. 33 (4): 792–807. doi:10.1145/6490.6503. S2CID 17064126.

설명: 이 논문은 편도함수의 존재가 계산적 무작위로 이어진다는 것을 보여주었다.

IP = PSPACE

• Shamir, A. (1992). "IP = PSPACE". Journal of the ACM. 39 (4): 869–877. doi:10.1145/146585.146609. S2CID 315182.

설명: IP는 (인터랙티브 증명 시스템에 기반한) 특성화가 일반적인 시간/공간 경계 계산 수업과는 상당히 다른 복잡도 수업이다. 샤미르는 본 논문에서 룬드 외 연구진에게 PSPACE가 IP에 포함되어 있다는 것을 보여주기 위해 이전 논문의 기법을 확장하였으며, 따라서 IP = PSPACE가 IP에 포함되어 있으므로, 하나의 복잡성 등급의 각각의 문제를 다른 문제에서 해결할 수 있도록 하였다.

결합 문제 간의 축소 가능성

• R. M. 카프
• R. E. 밀러와 J. W. 대처에서 편집자, 컴퓨터 계산의 복잡성, 플레넘 프레스, 뉴욕, 1972, 페이지 85–103

설명: 본 논문은 21개의 다른 문제들이 NP-완전하다는 것을 보여주었고 개념의 중요성을 보여주었다.

쌍방향 증명 시스템의 지식 복잡성

• Goldwasser, S.; Micali, S.; Rackoff, C. (1989). "The Knowledge Complexity of Interactive Proof Systems" (PDF). SIAM J. Comput. 18 (1): 186–208. doi:10.1137/0218012.

설명: 본 논문은 0지식의 개념을 소개했다.^[6]

괴델이 폰 노이만에게 보낸 편지

• 쿠르트 괴델
• 괴델이 1956년 3월 20일 요한 폰 노이만에게 보낸 편지
• 온라인 버전

설명: 괴델은 효율적인 보편적 정리 프로베라 사상에 대해 논한다.

알고리즘의 계산 복잡성

• Hartmanis, Juris; Stearns, Richard (1965). "On the computational complexity of algorithms". Transactions of the American Mathematical Society. 117: 285–306. doi:10.1090/s0002-9947-1965-0170805-7.

설명: 이 논문은 계산상의 복잡성에 이름과 씨앗을 주었다.

길, 나무, 꽃

• Edmonds, J. (1965). "Paths, trees, and flowers". Canadian Journal of Mathematics. 17: 449–467. doi:10.4153/CJM-1965-045-4.

설명: 초당적이지 않은 그래프에서 최대 일치를 찾기 위한 다항 시간 알고리즘과 계산 복잡성의 개념을 향한 또 다른 단계가 있다. 자세한 내용은 [2]를 참조하십시오.

트랩도어 함수의 이론 및 적용

• Yao, A. C. (1982). "Theory and application of trapdoor functions". 23rd Annual Symposium on Foundations of Computer Science (SFCS 1982). pp. 80–91. doi:10.1109/SFCS.1982.45.

설명: 이 논문은 트랩도어 기능을 위한 이론적 프레임워크를 만들고, 암호학에서와 같이 그들의 응용 프로그램의 일부를 기술했다. 트랩도어 함수의 개념은 6년 전에 "암호화의 새로운 방향"에서 가져온 것임을 유의한다(섹션 V "문제 상호관계와 트랩도어" 참조).

계산 복잡성

• C.H. 파파디미트리오
• 애디슨 웨슬리, 1994년 ISBN 0-201-53082-1

설명: 계산 복잡성 이론에 대한 소개로, 이 책은 P-SPACE의 저자의 특성화와 다른 결과들을 설명한다.

대화식 증명 및 근사치 패거리의 경도

• Feige, U.; Goldwasser, S.; Lovász, L.; Safra, S.; Szegedy, M. (1996). "Interactive proofs and the hardness of approximating cliques". Journal of the ACM. 43 (2): 268–292. doi:10.1145/226643.226652.

확률론적 증거 확인: NP의 새로운 특성화

• Arora, S.; Safra, S. (1998). "Probabilistic checking of proofs: A new characterization of NP". Journal of the ACM. 45: 70–122. doi:10.1145/273865.273901. S2CID 751563.

검증 및 근사 문제 경도

• Arora, S.; Lund, C.; Motwani, R.; Sudan, M.; Szegedy, M. (1998). "Proof verification and the hardness of approximation problems". Journal of the ACM. 45 (3): 501–555. CiteSeerX 10.1.1.145.4652. doi:10.1145/278298.278306. S2CID 8561542.

설명: 이 세 개의 논문은 근접한 해결책만 요구해도 NP의 어떤 문제들은 여전히 딱딱하게 남아 있다는 놀라운 사실을 입증했다. PCP 정리를 참조하십시오.

기능의 본질적 계산 난이도에 관한 연구

• Cobham, Alan (1964). "The Intrinsic Computational Difficulty of Functions" (PDF). Proceedings of the 1964 International Congress for Logic, Methodology, and the Philosophy of Science: 24–30.

설명: 복잡도 등급 P의 첫 번째 정의. 복잡성 이론의 창간지 중 하나.

알고리즘

"정리 증명용 기계 프로그램"

• Davis, M.; Logemann, G.; Loveland, D. (1962). "A machine program for theorem-proving" (PDF). Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. S2CID 15866917.

설명: DPLL 알고리즘. SAT 및 기타 NP-Complete 문제에 대한 기본 알고리즘.

"해결 원칙에 입각한 기계 지향 논리"

• Robinson, J. A. (1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM. 12: 23–41. doi:10.1145/321250.321253. S2CID 14389185.

설명: 자동화된 정리 입증에 사용된 분해능과 통일의 첫 번째 설명, 프롤로그와 논리 프로그래밍에 사용된다.

"여행 판매원 문제와 최소 스패닝 트리"

• Held, M.; Karp, R. M. (1970). "The Traveling-Salesman Problem and Minimum Spanning Trees". Operations Research. 18 (6): 1138–1162. doi:10.1287/opre.18.6.1138.

설명: 최소 스패닝 트리에 대한 알고리즘을 NP-Complete 이동 세일즈맨 문제에 대한 근사 알고리즘으로 사용. 근사 알고리즘은 NP-완전성 문제에 대처하는 일반적인 방법이 되었다.

"선형 프로그래밍의 다항식 알고리즘"

• L. G. 카치얀
• 소비에트 수학 - 독레이디, 191-194, 1979년 페이지 20

설명: 오랫동안 선형 프로그래밍 문제에 대한 다항식 시간 알고리즘은 없었다. 카치얀은 다항식 알고리즘을 최초로 제공했다(이전의 알고리즘처럼 대부분의 시간이 빠르지 않았을 뿐만 아니라). 후에 Narendra Karmarkar는 Narendra Karmarkar, "선형 프로그래밍을 위한 새로운 다항식 시간 알고리즘"에서 더 빠른 알고리즘을 제시하였다. Combinatorica, 제4권, 제4권, 페이지 373–395, 1984.

"선명성 테스트를 위한 확률론적 알고리즘"

• Rabin, M. (1980). "Probabilistic algorithm for testing primality". Journal of Number Theory. 12 (1): 128–138. doi:10.1016/0022-314X(80)90084-0.

설명: 이 논문은 밀러-라빈 원시성 테스트를 제시하고 무작위화된 알고리즘의 프로그램을 개략적으로 설명했다.

" 시뮬레이션된 어닐링을 통한 최적화"

• Kirkpatrick, S.; Gelatt, C. D.; Vecchi, M. P. (1983). "Optimization by Simulated Annealing". Science. 220 (4598): 671–680. Bibcode:1983Sci...220..671K. CiteSeerX 10.1.1.123.7607. doi:10.1126/science.220.4598.671. PMID 17813860. S2CID 205939.

설명: 이 기사는 현재 NP-Complete 문제에 대해 매우 일반적인 경험적 휴리스틱인 시뮬레이션 어닐링을 설명했다.

컴퓨터 프로그래밍의 기술

• 도널드 크누스

설명: 이 모노그래프는 인기 있는 알고리즘을 다루는 네 권의 책을 가지고 있다. 알고리즘은 영어와 MIX 어셈블리 언어(또는 MMIX 어셈블리 언어의 최신 페시클)로 작성된다. 이는 알고리즘을 이해하면서도 정밀하게 만든다. 그러나 낮은 수준의 프로그래밍 언어를 사용하면 일부 프로그래머들이 현대 구조화된 프로그래밍 언어에 더 친숙한 것을 좌절시킨다.

알고리즘 + 데이터 구조 = 프로그램

• 니클라우스 위스
• 프렌티스 홀, 1976, ISBN 0-13-022418-9

설명: Pascal에서 구현된 알고리즘 및 데이터 구조에 대한 초기 영향력 있는 책.

컴퓨터 알고리즘의 설계와 분석

• 알프레드 5세 아호, 존 E. 홉크로프트, 그리고 제프리 D. 울먼
• 애디슨-웨슬리, 1974년 ISBN 0-201-00029-6

설명: 약 1975-1985년 기간 동안 알고리즘에 대한 표준 텍스트 중 하나.

컴퓨터로 해결하는 방법

• Dromey, R. G. (1982). How to Solve it by Computer. Prentice-Hall International. ISBN 978-0-13-434001-2.

설명: 알고리즘과 데이터 구조의 이유 설명 창의적 프로세스, 추론의 선, 혁신적인 솔루션의 설계 요인 설명.

알고리즘

• 로버트 세지윅
• 애디슨 웨슬리, 1983년 ISBN 0-201-06672-6

설명: 1980년대 후반 알고리즘에 관한 매우 유명한 텍스트. 아호, 홉크로프트, 울만보다 접근성이 좋고 가독성이 뛰어났다(그러나 초급이었다). 최근 판이 더 많이 있다.

알고리즘 소개

• 토마스 H. 코멘, 찰스 E. Leiserson, Ronald L. Rivest, 그리고 Clifford Stein
• 제3판 MIT 프레스, 2009년 ISBN 978-0-262-03384-8.

설명: 이 교과서는 기본 알고리즘을 가르치기 위한 거의 사실상의 표준이 될 정도로 인기를 끌었다. 제1판(최초 3명의 저자와 함께)은 1990년에, 제2판은 2001년에, 제3판은 2009년에 출판되었다.

알고리즘 정보 이론

"난수 표에"

• Kolmogorov, Andrei N. (1963). "On Tables of Random Numbers". Sankhyā Ser. A. 25: 369–375. MR 0178484.
• Kolmogorov, Andrei N. (1963). "On Tables of Random Numbers". Theoretical Computer Science. 207 (2): 387–395. doi:10.1016/S0304-3975(98)00075-9. MR 1643414.

설명: 확률에 대한 계산 및 조합 접근 방식 제안.

"유도 추론의 형식적 이론"

• 레이 솔로모노프
• 정보 및 제어, 제7권 페이지 1-22 및 1964년 224-254
• 온라인 카피: 파트 I, 파트 II

설명: 이것이 알고리즘 정보 이론과 콜모고로프 복잡성의 시작이었다. Kolmogorov 복잡성이 Andrey Kolmogorov의 이름을 따서 명명되었지만, 그는 그 생각의 씨앗이 Ray 솔로몬off 때문이라고 말했다. 안드레이 콜모고로프는 이 분야에 많은 기여를 했지만 이후 기사에서 많은 기여를 했다.

"알고리즘 정보 이론"

• Chaitin, Gregory (1977). "Algorithmic information theory" (PDF). IBM Journal of Research and Development. 21 (4): 350–359. CiteSeerX 10.1.1.48.3094. doi:10.1147/rd.214.0350. Archived from the original (PDF) on 2009-05-30.

설명: 해당 지역의 중요한 사람 중 한 명이 만든 알고리즘 정보 이론의 소개.

정보이론

"수학적 의사소통 이론"

• Shannon, C.E. (1948). "A mathematical theory of communication". Bell System Technical Journal. 27 (3): 379–423, 623–656. doi:10.1002/j.1538-7305.1948.tb01338.x. hdl:10338.dmlcz/101429.

설명: 이 논문은 정보 이론의 분야를 창조했다.

"오류 감지 및 코드 수정 오류"

• Hamming, Richard (1950). "Error detecting and error correcting codes". Bell System Technical Journal. 29 (2): 147–160. doi:10.1002/j.1538-7305.1950.tb00463.x. hdl:10945/46756.

설명: 본 논문에서 해밍은 오류 수정 코드의 개념을 소개했다. 그는 해밍 코드와 해밍 거리를 만들고 코드 최적성 증명에 대한 방법을 개발했다.

"최소 중복 코드 구축 방법"

• Huffman, D. (1952). "A Method for the Construction of Minimum-Redundancy Codes" (PDF). Proceedings of the IRE. 40 (9): 1098–1101. doi:10.1109/JRPROC.1952.273898.

설명: 허프먼 코딩.

"순차 데이터 압축을 위한 범용 알고리즘"

• Ziv, J.; Lempel, A. (1977). "A universal algorithm for sequential data compression". IEEE Transactions on Information Theory. 23 (3): 337–343. CiteSeerX 10.1.1.118.8921. doi:10.1109/TIT.1977.1055714. hdl:10338.dmlcz/142947. Archived from the original on 2003-12-04.

설명: LZ77 압축 알고리즘.

정보이론의 요소

• T. Cover; J. Thomas (1991). Elements of Information Theory. pp. 38–42. ISBN 978-0-471-06259-2.

설명: 정보 이론에 대한 통속적인 소개.

형식검증

프로그램에 의미 할당

• Floyd, Robert (1967). "Assigning Meaning to Programs". Mathematical Aspects of Computer Science (PDF). Proceedings of Symposia in Applied Mathematics. 19. pp. 19–32. doi:10.1090/psapm/019/0235771. ISBN 9780821813195.

설명: 로버트 플로이드의 획기적인 논문 "프로그램에 의미 부여"는 귀납적 주장 방법을 소개하고, 1차 주장으로 주석을 단 프로그램이 사전 및 사후 조건 명세서를 충족하도록 어떻게 보여질 수 있는지 설명한다. 이 논문은 또한 루프 불변성과 검증 조건의 개념을 소개한다.

컴퓨터 프로그래밍에 대한 자명적 근거

• Hoare, C. A. R. (October 1969). "An axiomatic basis for computer programming" (PDF). Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259. S2CID 207726175. Archived from the original (PDF) on 2016-03-04.

설명: 토니 호어(Tony Hoare)의 논문 컴퓨터 프로그래밍에 대한 자명적 근거(Axiomatic Basis for Computer Programming)는 호어-트리플(Hoare-Triple)의 관점에서 기술된 알골(Angol) 유사 프로그래밍 언어의 단편들에 대한 일련의 추론(즉, 형식적 증거) 규칙을 기술하고 있다.

보호 명령, 비계측성 및 프로그램의 형식적 파생

• Dijkstra, E. W. (1975). "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM. 18 (8): 453–457. doi:10.1145/360933.360975. S2CID 1679242.

설명: Edsger Dijkstra의 논문 Guarded Commands, Noneterminacy 및 Programs의 형식 유래(즉, 그의 1976년 대학원 수준의 교과서 A Gergulation of Programming)는 프로그램이 작성된 후 프로그램을 공식적으로 검증하는 대신 프로그램과 그 형식적인 증거를 직접 개발해야 한다고 제안한다.가장 약한 사전 조건을 점진적으로 정제하기 위해 변압기를 먹거나, 프로그램(또는 형식) 미세화(또는 파생) 또는 때로는 "구축별 정확성"으로 알려진 방법.

병렬 프로그램에 대한 주장 입증

• 에드워드 A. 애쉬크로프트
• J. 연산. 시스템. Sci. 10(1): 110–135(1975) doi:10.1016/s0022-0000(75)80018-3

설명: 동시 프로그램의 비침투적인 증거를 소개한 논문.

병렬 프로그램에 대한 자명적 증명 기법 I

• 수잔 S. 오위키, 데이비드 그리스
• 액타 알림. 6: 319–340 (1976)

설명: 본 논문에서, 같은 저자의 논문 "병렬 프로그램의 속성 검증: A A A A A A A A A A Axiomatic Access. 코뮌. ACM 19(5): 279–285(1976년), 병렬 프로그램 검증에 대한 자명적 접근법이 제시되었다.

프로그래밍의 규율

• 에드거 디크스트라
• 1976

설명: Edsger Dijkstra의 고전적인 대학원 수준의 교과서인 "프로그램의 규율"은 그의 초기 논문인 "Guarded Commands," "Noneterminacy"와 "Formal Deparation of Programs"를 확장하고 그들의 규격에서 프로그램을 공식적으로 도출하는 원칙을 확고히 확립한다.

변절론적 의미론

• 조 스토이
• 1977

설명: Joe Stoy의 Denotational Semantics는 프로그래밍 언어의 공식 의미론에 대한 수학적(또는 기능적) 접근방식의 (운영적 및 대수적 접근방식과는 대조적으로) 첫 번째 (수학적 수준) 장구적 표현이다.

프로그램의 일시적 논리

• Pnueli, A. (1977). "The temporal logic of programs". 18th Annual Symposium on Foundations of Computer Science (SFCS 1977). IEEE. pp. 46–57. doi:10.1109/SFCS.1977.32. S2CID 117103037.

설명: 시간적 논리의 활용이 형식적인 검증의 방법으로 제시되었다.

고정점을 사용하여 병렬 프로그램의 정확도 특성 지정(1980)

• E. 앨런 에머슨, 에드먼드 M. 클라크
• Proc. 7번째 오토마타 언어 및 프로그래밍 국제 콜로키움, 169-181, 1980페이지

설명: 동시 프로그램의 정확성을 확인하는 절차로 모델 체크를 도입했다.

통신 순차적 프로세스(1978)

• C.A.R. 후아레
• 1978

설명: 토니 호어(원래)의 통신 순차 프로세스(CSP) 논문은 변수를 공유하지 않고 동기식 메시지를 교환하는 것만으로 협력하는 동시 프로세스(즉 프로그램)의 아이디어를 소개한다.

의사소통 시스템의 미적분학

• 로빈 밀너
• 1980

설명: 로빈 밀너의 통신 시스템 미적분학(CCS) 논문은 동시성 초기 모델(세마포어, 임계 섹션, 원본 CSP)에 대해 공식적으로 추론할 수 있는 프로세스 대수학을 설명한다.

소프트웨어 개발: 엄격한 접근 방식

• 클리프 존스
• 1980

설명: Cliff Jones의 교과서 소프트웨어 개발: 엄격한 접근법은 비엔나 개발 방법(VDM)의 첫 번째 전문 전시회로, 지난 10년 동안 IBM의 비엔나 연구소에서 (원론적으로) 진화했으며, Dijkstra에 따른 프로그램 정교화 아이디어와 녹조 정제(또는 재조정) 아이디어를 결합한 것이다.비브라하게 정의된 추상적 데이터 형식은 공식적으로 점진적으로 더 "중요한" 표현으로 변환된다.

프로그래밍의 과학

• 데이비드 그리스
• 1981

설명: David Gries의 교과서 The Science of Programming은 이전의 Dijkstra의 A Pergulation of Programming보다 훨씬 더 접근하기 쉬운 방법을 제외하고, 공식적인 프로그램 파생의 가장 약한 전제조건 방법을 설명한다.

올바르게 작동하는 프로그램(입력 오류 이외의 버그 없이)을 구성하는 방법을 보여준다. 이를 위해 전제조건과 사후 조건 술어 표현, 프로그램 증명 기법 등을 활용해 프로그램이 만들어지는 방식을 안내하는 방법을 보여준다.

이 책에 나오는 예들은 모두 규모가 작고, (실제와는 대조적으로) 분명히 학문적이다. 분류와 병합, 문자열 조작 등 기본 알고리즘을 강조한다. 서브루틴(기능)은 포함되지만 객체 지향 및 기능 프로그래밍 환경은 다루지 않는다.

순차적 프로세스 커뮤니케이션(1985)

• C.A.R. 후아레
• 1985

설명: Tony Hoare의 CSP(Communication Sequential Process) 교과서(현재 역대 세 번째로 많이 인용된 컴퓨터 과학 참조서)는 협력 프로세스에는 프로그램 변수조차 없으며 CCS와 마찬가지로 프로세스 시스템이 공식적으로 설득될 수 있는 업데이트된 CSP 모델을 제시한다.

선형 논리(1987)

• Girard, J.-Y (1987). "Linear Logic" (PDF). Theoretical Computer Science. 50 (1): 1–102. doi:10.1016/0304-3975(87)90045-4. Archived from the original (PDF) on 2006-11-29.

설명: Girard의 선형 논리는 순차 및 동시 연산을 위한 타이핑 시스템, 특히 자원을 의식하는 타이핑 시스템의 설계에 획기적인 발전이었다.

이동프로세스의 미적분학 (1989)

• R. Milner, J. Parrow, D. 워커
• 1989
• 온라인 버전: 1부 및 2부

설명: 본 논문에서는 공정 이동성을 허용하는 CCS의 일반화 Pi-Miculus를 소개한다. 미적분은 극히 단순하며 프로그래밍 언어, 타이핑 시스템, 프로그램 로직의 이론적 연구에서 지배적인 패러다임이 되었다.

Z 표기법: 참조 설명서

• Spivey, J. M. (1992). The Z Notation: A Reference Manual (2nd ed.). Prentice Hall International. ISBN 978-0-13-978529-0. Archived from the original on 2016-06-20. Retrieved 2009-08-24.

설명: 마이크 스피비의 고전 교과서 The Z Motionation: A Reference Manual은 Jean-Raymond Abrial에 의해 유래되었지만, 지난 10년 동안 옥스퍼드 대학에서 (원래적으로) 진화해 온 공식 규격 언어 Z 표기법을 요약하고 있다.

통신 및 동시성

• 로빈 밀너
• 프렌티스 홀 인터내셔널, 1989년

설명: 로빈 밀너의 교과서 "통신과 동시성"은 그의 초기 CCS 작업에 대한 기술적으로는 아직 진보했지만 더 쉽게 접근할 수 있다.

프로그래밍의 실용 이론

• 에릭 헤너
• Springer, 1993년 최신판, 온라인판

설명: 사전 프로그래밍의 최신 버전. C.A.R. Hoare의 UTP의 기초. 가장 단순하고 포괄적인 형식 방법.

참조