Lista ważnych publikacji z zakresu informatyki teoretycznej - List of important publications in theoretical computer science

Jest to lista ważnych publikacji z zakresu informatyki teoretycznej , uporządkowanych według dziedzin.

Oto kilka powodów, dla których dana publikacja może być uznana za ważną:

• Kreator tematów – Publikacja, która stworzyła nowy temat
• Przełom – Publikacja, która znacząco zmieniła wiedzę naukową
• Wpływ – Publikacja, która znacząco wpłynęła na świat lub wywarła ogromny wpływ na nauczanie informatyki teoretycznej.

Obliczalność

Obliczalność Cutlanda : wprowadzenie do teorii funkcji rekurencyjnych (Cambridge)

• Cutland, Nigel J. (1980). Obliczalność: wprowadzenie do teorii funkcji rekurencyjnych . Wydawnictwo Uniwersytetu Cambridge . Numer ISBN 978-0-521-29465-2.

Przegląd tego wczesnego tekstu autorstwa Carla Smitha z Purdue University (w Society for Industrial and Applied Mathematics Reviews ), donosi, że jest to tekst z „odpowiednią mieszanką intuicji i rygoru… w ekspozycji dowodów”, który przedstawia „podstawowe wyniki klasycznej teorii rekurencji [RT]... w stylu... dostępnym dla studentów o minimalnym zapleczu matematycznym". Chociaż stwierdza, że ​​„byłby to doskonały tekst wprowadzający do kursu wprowadzającego w [RT] dla studentów matematyki”, sugeruje, że „instruktor musi być przygotowany do znacznego poszerzenia materiału…”, gdy jest używany ze studentami informatyki ( ze względu na niedostatek materiałów na temat zastosowań RT w tym obszarze).

Rozstrzygalność teorii drugiego rzędu i automatów na drzewach nieskończonych

• Michał O. Rabin
• Transakcje Amerykańskiego Towarzystwa Matematycznego , obj. 141, s. 1–35, 1969

Opis: W referacie przedstawił automat drzewo , przedłużenie automatów . Automat drzewny miał wiele zastosowań do sprawdzania poprawności programów .

Automaty skończone i ich problemy decyzyjne

• Michael O. Rabin i Dana S. Scott
• IBM Journal Badań i Rozwoju , tom. 3, s. 114–125, 1959
• Wersja online

Opis: Matematyczne traktowanie automatów , dowód własności rdzenia i definicja niedeterministycznego automatu skończonego .

Wprowadzenie do teorii automatów, języków i obliczeń

• John E. Hopcroft , Jeffrey D. Ullman i Rajeev Motwani
• Addison-Wesley , 2001, ISBN  0-201-02988-X

Opis: Popularny podręcznik.

O pewnych formalnych własnościach gramatyk

• Chomsky, N. (1959). „O pewnych formalnych własnościach gramatyk” . Informacja i kontrola . 2 (2): 137–167. doi : 10.1016/S0019-9958(59)90362-6 .

Opis: W tym artykule przedstawiono to, co jest obecnie znane jako hierarchia Chomsky'ego , hierarchia zawierająca klasy gramatyk formalnych, które generują języki formalne .

Na liczbach obliczalnych, z podaniem do Entscheidungsproblem

• Alan Turing
• Proceedings of London Mathematical Society , Seria 2 , tom. 42, s. 230–265, 1937, doi : 10.1112/plms/s2-42.1.230 .
  Errata ukazała się w tom. 43, s. 544–546, 1938, doi : 10.1112/plms/s2-43.6.544 .
• Wersja HTML , wersja PDF

Opis: ten artykuł wyznacza granice informatyki. Zdefiniowała maszynę Turinga , model dla wszystkich obliczeń. Z drugiej strony dowiodła nierozstrzygalności problemu zatrzymania i problemu Entscheidungs, a tym samym znalazła granice możliwych obliczeń.

Funkcje rekursywne

• Peter, Rózsa (1951). Funkcje rekursywne . Prasa akademicka. Numer ISBN 9780125526500.

Pierwszy podręcznik teorii funkcji rekurencyjnych . Książka doczekała się wielu wydań i przyniosła Peterowi nagrodę Kossutha od rządu węgierskiego . Recenzje autorstwa Raphaela M. Robinsona i Stephena Kleene pochwaliły książkę za skuteczne wprowadzenie dla uczniów.

Reprezentacja zdarzeń w sieciach nerwowych i automatach skończonych

• SC Kleene
• Amerykańskie Siły Powietrzne Projekt Rand Memorandum RM-704 , 1951
• Wersja online
• publikowane w: Shannon, Claude ; McCarthy, John , wyd. (1956). Badania automatyczne . OCLC  564148 .

Opis: w tym artykule przedstawiono automaty skończone , wyrażenia regularne i języki regularne oraz ustanowiono ich połączenie.

Teoria złożoności obliczeniowej

Arora & Baraka Złożoność obliczeniowa i Goldreich za Złożoność obliczeniowa (zarówno Cambridge)

• Sanjeev Arora i Boaz Barak, „Computational Complexity: A Modern Approach”, Cambridge University Press, 2009, 579 stron, twarda okładka
• Oded Goldreich, „Computational Complexity: A Conceptual Perspective”, Cambridge University Press, 2008, 606 stron, twarda oprawa

Poza szacowną prasą prezentującą te ostatnie teksty, są one bardzo pozytywnie zrecenzowane w ACM SIGACT News przez Daniela Apona z University of Arkansas, który określa je jako „podręczniki do kursu teorii złożoności, skierowanego do wczesnych absolwentów… lub… zaawansowani studenci studiów licencjackich… [z] licznymi, unikalnymi mocnymi stronami i bardzo nielicznymi słabościami” i stwierdza, że ​​obaj są:

„doskonałe teksty, które dokładnie obejmują zarówno szerokość, jak i głębokość teorii złożoności obliczeniowej… [autorów]… każdy [którzy] są gigantami w teorii informatyki [gdzie każdy będzie]… wyjątkowy tekst referencyjny dla ekspertów w dziedzinie dziedzinie… [i to] …teoretycy, badacze i instruktorzy każdej szkoły myślenia uznają każdą książkę za przydatną.”

Recenzent zauważa, że ​​„[Arora i Barak] podjęli zdecydowaną próbę włączenia bardzo aktualnego materiału, podczas gdy Goldreich koncentruje się bardziej na opracowaniu kontekstowych i historycznych podstaw dla każdej prezentowanej koncepcji” i że „przyklaskuje [s. ] wszystkim… autorom za ich wybitny wkład.”

Niezależna od maszyny teoria złożoności funkcji rekurencyjnych

• Blum, Manuel (1967). „Niezależna od maszyny teoria złożoności funkcji rekurencyjnych” (PDF) . Dziennik ACM . 14 (2): 322–336. doi : 10.1145/321386.321395 . S2CID  15710280 .

Opis: Aksjomaty Bluma .

Metody algebraiczne dla interaktywnych systemów dowodowych

• Lund, C .; Fortnow, L .; Karloff, H.; Nisan, N. (1992). „Metody algebraiczne dla interaktywnych systemów dowodowych”. Dziennik ACM . 39 (4): 859–868. CiteSeerX  10.1.1.41.9477 . doi : 10.1145/146585.146605 . S2CID  207170996 .

Opis: Ten artykuł wykazał, że PH jest zawarte w IP .

Złożoność procedur dowodzenia twierdzeń

• Cook, Stephen A. (1971). „Złożoność procedur dowodzenia twierdzeń” (PDF) . Materiały z III Dorocznego Sympozjum ACM z Teorii Informatyki : 151–158. CiteSeerX  10.1.1.406.395 . doi : 10.1145/800157.805047 . S2CID  7573663 .

Opis: Ten artykuł wprowadził pojęcie NP-zupełności i udowodnił, że problem spełnialności logicznej (SAT) jest NP-zupełny . Zauważ, że podobne pomysły zostały opracowane niezależnie nieco później przez Leonida Levina w „Levin, Universal Search Problems. Problemy Peredachi Informatsii 9(3):265-266, 1973”.

Komputery i nierozwiązywalność: przewodnik po teorii NP-zupełności

• Garey, Michael R .; Johnson, David S. (1979). Komputery i nierozwiązywalność: przewodnik po teorii NP-zupełności . Nowy Jork: Freeman. Numer ISBN 978-0-7167-1045-5.

Opis: Główne znaczenie tej książki wynika z obszernej listy ponad 300 problemów NP-Kompletnych . Lista ta stała się powszechnym odniesieniem i definicją. Chociaż książka została opublikowana zaledwie kilka lat po zdefiniowaniu koncepcji, znaleziono tak obszerną listę.

Stopień trudności obliczania funkcji i częściowego uporządkowania zbiorów rekurencyjnych

• Rabin, Michael O. (1960). „Stopień trudności obliczania funkcji i częściowe uporządkowanie zbiorów rekurencyjnych” (PDF) . Raport techniczny nr 2 . Jerozolima: Uniwersytet Hebrajski.

Opis: Ten raport techniczny był pierwszą publikacją mówiącą o tym, co później przemianowano na złożoność obliczeniową

Jak dobra jest metoda simplex?

• Victor Klee i George J. Minty
• Klee, Wiktor ; Minty, George J. (1972). „Jak dobry jest algorytm simpleks?”. W Shisha, Oved (red.). Nierówności III (Proceedings of the Third Symposium on Inequalities, które odbyły się na Uniwersytecie Kalifornijskim w Los Angeles, Kalifornia, 1-9 września 1969, poświęcone pamięci Theodore S. Motzkin) . Nowy Jork-Londyn: Prasa akademicka. s. 159–175. MR  0332165 .

Opis: Wykonany z „Klee-Minty cube” w wymiarze  D , którego 2 ^D rogi każdy odwiedził gdański „s algorytmu simplex do optymalizacji liniowej .

Jak konstruować funkcje losowe

• Goldreich, O .; Goldwasser, S .; Micali, S. (1986). "Jak konstruować funkcje losowe" (PDF) . Dziennik ACM . 33 (4): 792-807. doi : 10.1145/6490.6503 . S2CID  17064126 .

Opis: Ten artykuł wykazał, że istnienie funkcji jednokierunkowych prowadzi do losowości obliczeniowej .

IP = PSPACE

• Szamir, A. (1992). „IP = PSPACE”. Dziennik ACM . 39 (4): 869–877. doi : 10.1145/146585.146609 . S2CID  315182 .

Opis: IP to klasa złożoności, której charakterystyka (oparta na interaktywnych systemach dowodowych ) różni się znacznie od zwykłych klas obliczeniowych ograniczonych czasowo/przestrzennie. W tym artykule Shamir rozszerzył technikę z poprzedniego artykułu autorstwa Lunda i innych, aby pokazać, że PSPACE jest zawarty w IP , a zatem IP = PSPACE, tak że każdy problem w jednej klasie złożoności można rozwiązać w drugiej.

Redukcja wśród problemów kombinatorycznych

• RM Karp
• W RE Miller i JW Thatcher, redaktorzy, Complexity of Computer Computations , Plenum Press, New York, NY, 1972, s. 85-103

Opis: Ten artykuł wykazał, że 21 różnych problemów jest NP-Kompletnych i pokazał wagę tej koncepcji.

Złożoność wiedzy o interaktywnych systemach dowodowych

• Goldwasser, S .; Micali, S .; Rackoff, C. (1989). „Złożoność wiedzy interaktywnych systemów dowodowych” (PDF) . SIAM J. Comput. 18 (1): 186–208. doi : 10.1137/0218012 .

Opis: W tym artykule wprowadzono pojęcie wiedzy zerowej .

List Gödla do von Neumann

• Kurt Gödel
• List Gödla do Johna von Neumanna , 20 marca 1956 r.
• Wersja online

Opis: Gödel omawia ideę efektywnego dowodzenia twierdzeń uniwersalnych.

O złożoności obliczeniowej algorytmów

• Hartmanis, Juris ; Stearns, Richard (1965). „O złożoności obliczeniowej algorytmów” . Transakcje Amerykańskiego Towarzystwa Matematycznego . 117 : 285-306. doi : 10.1090/s0002-9947-1965-0170805-7 .

Opis: Ten artykuł nadał złożoności obliczeniowej nazwę i źródło.

Ścieżki, drzewa i kwiaty

• Edmonds, J. (1965). „Ścieżki, drzewa i kwiaty”. Kanadyjski Dziennik Matematyki . 17 : 449–467. doi : 10.4153/CJM-1965-045-4 .

Opis: istnieje wielomianowy algorytm czasu, który znajduje maksymalne dopasowanie w grafie, które nie jest dwudzielne, i jest kolejnym krokiem w kierunku idei złożoności obliczeniowej . Więcej informacji znajdziesz w [2] .

Teoria i zastosowania funkcji zapadni

• Yao, AC (1982). „Teoria i zastosowanie funkcji zapadni”. 23 Doroczne Sympozjum Podstaw Informatyki (SFCS 1982) . s. 80–91. doi : 10.1109/SFCS.1982.45 .

Opis: Ten artykuł tworzy teoretyczne ramy dla funkcji pułapek i opisuje niektóre z ich zastosowań, na przykład w kryptografii . Zauważ, że koncepcja funkcji zapadni została wprowadzona w "Nowych kierunkach w kryptografii" sześć lat wcześniej (patrz rozdział V "Powiązania problemów i zapadki.").

Złożoność obliczeniowa

• CH Papadimitriou
• Addison-Wesley , 1994, ISBN  0-201-53082-1

Opis: Wprowadzenie do teorii złożoności obliczeniowej , książka wyjaśnia charakterystykę autora P-SPACE i inne wyniki.

Interaktywne dowody i twardość aproksymacji klik

• Feige, U .; Goldwasser, S .; Lovász, L .; Safra, S .; Szegedy, M. (1996). „Dowody interaktywne a twardość aproksymacji klik” . Dziennik ACM . 43 (2): 268–292. doi : 10.1145/226643.226652 .

Probabilistyczne sprawdzanie dowodów: nowa charakterystyka NP

• Arora, S .; Safra, S. (1998). „Probabilistyczne sprawdzanie dowodów: nowa charakterystyka NP”. Dziennik ACM . 45 : 70–122. doi : 10.1145/273865.273901 . S2CID  751563 .

Weryfikacja dowodu i problemy twardości aproksymacji

• Arora, S .; Lund, C .; Motwani, R .; Sudan, M .; Szegedy, M. (1998). „Weryfikacja dowodu i twardość problemów aproksymacji”. Dziennik ACM . 45 (3): 501–555. CiteSeerX  10.1.1.145.4652 . doi : 10.1145/278298.278306 . S2CID  8561542 .

Opis: Te trzy artykuły ustaliły zaskakujący fakt, że niektóre problemy w NP pozostają trudne, nawet gdy wymagane jest tylko przybliżone rozwiązanie. Zobacz twierdzenie PCP .

Wewnętrzna trudność obliczeniowa funkcji

• Cobham, Alan (1964). „Wewnętrzna trudność obliczeniowa funkcji” (PDF) . Materiały Międzynarodowego Kongresu Logiki, Metodologii i Filozofii Nauki z 1964 r .: 24–30.

Opis: Pierwsza definicja klasy złożoności P. Jedna z prac założycielskich teorii złożoności.

Algorytmy

„Program maszynowy do dowodzenia twierdzeń”

• Davis, M .; Logemann, G.; Loveland, D. (1962). „Program maszynowy do dowodzenia twierdzeń” (PDF) . Komunikaty ACM . 5 (7): 394–397. doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 . S2CID  15866917 .

Opis: Algorytm DPLL . Podstawowy algorytm dla SAT i innych problemów NP-Complete .

„Logika zorientowana na maszynę oparta na zasadzie rozdzielczości”

• Robinson, JA (1965). „Logika zorientowana na maszynę oparta na zasadzie rozdzielczości”. Dziennik ACM . 12 : 23–41. doi : 10.1145/321250.321253 . S2CID  14389185 .

Opis: Pierwszy opis rozwiązania i unifikacji używany w automatycznym dowodzeniu twierdzeń ; używany w Prologu i programowaniu logicznym .

"Problem komiwojażera i minimalne drzewa rozpinające"

• Held, M .; Karp, RM (1970). „The Traveling-Salesman Problem i minimalne drzewa opinające”. Badania operacyjne . 18 (6): 1138-1162. doi : 10.1287/opre.18.6.1138 .

Opis: Zastosowanie algorytmu minimalnego drzewa rozpinającego jako algorytmu aproksymacyjnego dla problemu komiwojażera NP-Complete . Algorytmy aproksymacyjne stały się powszechną metodą radzenia sobie z problemami NP-Complete.

„Algorytm wielomianowy w programowaniu liniowym”

• LG Khachiyan
• Matematyka radziecka - Dokłady , tom. 20, s. 191-194, 1979

Opis: przez długi czas nie istniał algorytm wielomianowy, którego można dowieść, dla problemu programowania liniowego . Khachiyan jako pierwszy dostarczył algorytm, który był wielomianowy (i nie tylko był wystarczająco szybki przez większość czasu, jak poprzednie algorytmy). Później Narendra Karmarkar przedstawił szybszy algorytm w: Narendra Karmarkar, „Nowy algorytm wielomianowy do programowania liniowego”, Combinatorica , tom 4, no. 4, s. 373-395, 1984.

„Algorytm probabilistyczny do testowania pierwszości”

• Rabin, M. (1980). „Algorytm probabilistyczny do badania pierwszości” . Czasopismo Teorii Liczb . 12 (1): 128–138. doi : 10.1016/0022-314X(80)90084-0 .

Opis: W pracy przedstawiono test pierwszości Millera-Rabina oraz zarysowano program algorytmów randomizowanych .

„Optymalizacja poprzez symulowane wyżarzanie”

• Kirkpatrick, S .; Gelatt, CD; Vecchi, MP (1983). „Optymalizacja przez symulowane wyżarzanie”. Nauka . 220 (4598): 671-680. Kod Bibcode : 1983Sci...220..671K . CiteSeerX  10.1.1.123.7607 . doi : 10.1126/science.220.4598.671 . PMID  17813860 . S2CID  205939 .

Opis: W tym artykule opisano symulowane wyżarzanie , które jest obecnie bardzo powszechną heurystyką dla problemów NP-Complete .

Sztuka programowania komputerowego

• Donald Knuth

Opis: Ta monografia ma cztery tomy obejmujące popularne algorytmy. Algorytmy są napisane zarówno w języku asemblerowym angielskim, jak i asemblerze MIX (lub w asemblerze MMIX w nowszych zeszytach). Dzięki temu algorytmy są zarówno zrozumiałe, jak i precyzyjne. Jednak użycie języka programowania niskiego poziomu frustruje niektórych programistów bardziej zaznajomionych z nowoczesnymi strukturalnymi językami programowania .

Algorytmy + Struktury danych = Programy

• Niklaus Wirth
• Prentice Hall, 1976, ISBN  0-13-022418-9

Opis: Wczesna, wpływowa książka o algorytmach i strukturach danych, z implementacjami w Pascalu.

Projektowanie i analiza algorytmów komputerowych

• Alfred V. Aho , John E. Hopcroft i Jeffrey D. Ullman
• Addison-Wesley, 1974, ISBN  0-201-00029-6

Opis: Jeden ze standardowych tekstów o algorytmach za okres około 1975-1985.

Jak rozwiązać to za pomocą komputera?

• Dromey, RG (1982). Jak rozwiązać to za pomocą komputera . Prentice-Hall International. Numer ISBN 978-0-13-434001-2.

Opis: Wyjaśnia dlaczego algorytmy i struktury danych. Wyjaśnia proces twórczy , linię rozumowania , czynniki projektowe stojące za innowacyjnymi rozwiązaniami.

Algorytmy

• Robert Sedgewick
• Addison-Wesley, 1983, ISBN  0-201-06672-6

Opis: Bardzo popularny tekst o algorytmach w późnych latach 80-tych. Był bardziej przystępny i czytelny (ale bardziej elementarny) niż Aho, Hopcroft i Ullman. Istnieją nowsze wydania.

Wprowadzenie do algorytmów

• Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest i Clifford Stein
• Wydanie trzecie, MIT Press, 2009, ISBN  978-0-262-03384-8 .

Opis: Ten podręcznik stał się tak popularny, że jest niemal de facto standardem nauczania podstawowych algorytmów. Wydanie I (z pierwszymi trzema autorami) ukazało się w 1990 roku, wydanie II w 2001 roku, a wydanie III w 2009 roku.

Algorytmiczna teoria informacji

„Na tablicach liczb losowych”

• Kołmogorowa, Andriej N. (1963). „Na tablicach liczb losowych”. Sankhyā Ser. . 25 : 369–375. MR  0178484 .
• Kołmogorowa, Andriej N. (1963). „Na tablicach liczb losowych” . Informatyka teoretyczna . 207 (2): 387-395. doi : 10.1016/S0304-3975(98)00075-9 . MR  1643414 .

Opis: Zaproponował obliczeniowe i kombinatoryczne podejście do prawdopodobieństwa.

„Formalna teoria wnioskowania indukcyjnego”

• Ray Solomonoff
• Informacja i kontrola , tom. 7, s. 1-22 i 224-254, 1964 19
• Egzemplarz online: część I , część II

Opis: Był to początek algorytmicznej teorii informacji i złożoności Kołmogorowa . Zauważ, że chociaż złożoność Kołmogorowa została nazwana na cześć Andrieja Kołmogorowa , powiedział on, że zalążek tej idei pochodzi od Raya Solomonoffa . Andriej Kołmogorow wniósł duży wkład w tę dziedzinę, ale w późniejszych artykułach.

„Algorytmiczna teoria informacji”

• Chaitin, Grzegorz (1977). „Algorytmiczna teoria informacji” (PDF) . IBM Journal of Research and Development . 21 (4): 350–359. CiteSeerX  10.1.1.48.3094 . doi : 10.1147/rd.214.0350 . Zarchiwizowane z oryginału (PDF) w dniu 2009-05-30.

Opis: Wprowadzenie do algorytmicznej teorii informacji autorstwa jednej z ważnych osób w okolicy.

Teoria informacji

"Matematyczna teoria komunikacji"

• Shannon, CE (1948). „Matematyczna teoria komunikacji” . Dziennik techniczny systemu Bell . 27 (3): 379–423, 623–656. doi : 10.1002/j.1538-7305.1948.tb01338.x . hdl : 10338.dmlcz/101429 .

Opis: Ten artykuł stworzył dziedzinę teorii informacji .

"Wykrywanie błędów i kody korekcji błędów"

• Hamminga, Richarda (1950). "Kody wykrywania błędów i korekcji błędów" . Dziennik techniczny systemu Bell . 29 (2): 147–160. doi : 10.1002/j.1538-7305.1950.tb00463.x . hdl : 10945/46756 .

Opis: W tym artykule Hamming przedstawił ideę kodu korygującego błędy . Stworzył kod Hamminga i odległość Hamminga oraz opracował metody dowodzenia optymalności kodu.

„Metoda konstrukcji kodów minimalnej redundancji”

• Huffman, D. (1952). „Metoda konstrukcji kodów minimalnej nadmiarowości” (PDF) . Postępowanie IRE . 40 (9): 1098–1101. doi : 10.1109/JRPROC.1952.273898 .

Opis: Kodowanie Huffmana .

"Uniwersalny algorytm do sekwencyjnej kompresji danych"

• Ziv, J .; Lempel, A. (1977). „Uniwersalny algorytm do sekwencyjnej kompresji danych” . Transakcje IEEE dotyczące teorii informacji . 23 (3): 337-343. CiteSeerX  10.1.1.118.8921 . doi : 10.1109/TIT.1977.1055714 . hdl : 10338.dmlcz/142947 . Zarchiwizowane od oryginału w dniu 2003-12-04.

Opis: Algorytm kompresji LZ77 .

Elementy teorii informacji

• T. okładka ; J. Thomas (1991). Elementy teorii informacji . s.  38–42 . Numer ISBN 978-0-471-06259-2.

Opis: Popularne wprowadzenie do teorii informacji.

Weryfikacja formalna

Przypisywanie znaczenia programom

• Floyda, Roberta (1967). „Przypisywanie znaczenia programom”. Matematyczne aspekty informatyki (PDF) . Materiały Sympozjów Matematyki Stosowanej. 19 . s. 19–32. doi : 10.1090/psapm/019/0235771 . Numer ISBN 9780821813195.

Opis: Przełomowy artykuł Roberta Floyda Assigning Meanings to Programs wprowadza metodę asercji indukcyjnych i opisuje, w jaki sposób program z adnotacjami z asercjami pierwszego rzędu może zostać pokazany jako spełniający specyfikację warunku wstępnego i końcowego – w artykule przedstawiono również koncepcje niezmiennika pętli i stan weryfikacji.

Aksjomatyczna podstawa programowania komputerowego

• Hoare, CAR (październik 1969). „Aksjomatyczna podstawa programowania komputerowego” (PDF) . Komunikaty ACM . 12 (10): 576–580. doi : 10.1145/363235.363259 . S2CID  207726175 . Zarchiwizowane z oryginału (PDF) w dniu 2016-03-04.

Opis: Artykuł Tony'ego Hoare'a An Axiomatic Basis for Computer Programming opisuje zbiór reguł wnioskowania (tj. formalnego dowodu) dla fragmentów języka programowania podobnego do Algola, opisanych w kategoriach (tak, jak się teraz nazywa) trójek Hoare'a.

Strzeżone polecenia, nieokreśloność i formalne wyprowadzanie programów

• Dijkstra, EW (1975). "Nakazy strzeżone, nieokreśloność i formalne wyprowadzanie programów" . Komunikaty ACM . 18 (8): 453–457. doi : 10.1145/360933.360975 . S2CID  1679242 .

Opis: Artykuł Edsgera Dijkstry Guarded Commands, Nondeterminacy and Formal Derivation of Programs (poszerzony o jego podręcznik do studiów podyplomowych Dyscyplina programowania z 1976 r.) proponuje, aby zamiast formalnej weryfikacji programu po jego napisaniu (tj. post facto), programy i ich formalne dowody powinny być opracowywane ręka w rękę (używając transformatorów predykatów do stopniowego udoskonalania najsłabszych warunków wstępnych), metodą znaną jako programowe (lub formalne) udoskonalanie (lub wyprowadzenie), lub czasami „poprawność przez konstrukcję”.

Dowodzenie twierdzeń o programach równoległych

• Edward A. Ashcroft
• J. Komputer. Syst. Nauka. 10(1): 110–135 (1975) doi : 10.1016/s0022-0000(75)80018-3

Opis: Artykuł wprowadzający dowody niezmienności programów współbieżnych.

Aksjomatyczna technika dowodowa dla programów równoległych I

• Susan S. Owicki , David Gries
• Acta Inform. 6: 319–340 (1976)

Opis: W niniejszym artykule, wraz z artykułem tych samych autorów „Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19(5): 279–285 (1976)”, przedstawiono aksjomatyczne podejście do weryfikacji programów równoległych.

Dyscyplina programowania

• Edsger W. Dijkstra
• 1976

Opis: Klasyczny podręcznik Edsgera Dijkstry do studiów podyplomowych Dyscyplina programowania rozszerza jego wcześniejszy artykuł Guarded Commands, Nondeterminacy and Formal Derivation of Programs i mocno ustanawia zasadę formalnego wyprowadzania programów (i ich dowodów) z ich specyfikacji.

Semantyka denotacyjna

• Joe Stoy
• 1977

Opis: Semantyka denotacyjna Joego Stoya to pierwsza (na poziomie podyplomowym) obszerna ekspozycja matematycznego (lub funkcjonalnego) podejścia do formalnej semantyki języków programowania (w przeciwieństwie do podejścia operacyjnego i algebraicznego).

Temporalna logika programów

• Pnueli, A. (1977). „Logika czasowa programów”. XVIII Doroczne Sympozjum Podstaw Informatyki (SFCS 1977) . IEEE. s. 46-57. doi : 10.1109/SFCS.1977.32 . S2CID  117103037 .

Opis: Zasugerowano użycie logiki temporalnej jako metody weryfikacji formalnej.

Charakteryzacja właściwości poprawnościowych programów równoległych z wykorzystaniem punktów stałych (1980)

• E. Allen Emerson , Edmund M. Clarke
• W proc. 7th International Colloquium on Automata Languages ​​and Programming, strony 169–181, 1980

Opis: Sprawdzanie modelu zostało wprowadzone jako procedura sprawdzania poprawności programów współbieżnych.

Komunikowanie procesów sekwencyjnych (1978)

• SAMOCHÓD Hoare
• 1978

Opis: Artykuł Tony'ego Hoare'a (oryginalny) komunikujący się sekwencyjny proces (CSP) przedstawia ideę współbieżnych procesów (tj. programów), które nie współdzielą zmiennych, ale zamiast tego współpracują wyłącznie poprzez wymianę synchronicznych wiadomości.

Rachunek systemów komunikacyjnych

• Robin Milner
• 1980

Opis: Artykuł Robina Milnera A Calculus of Communicating Systems (CCS) opisuje algebrę procesów pozwalającą na formalne rozumowanie systemów współbieżnych procesów, co nie było możliwe we wcześniejszych modelach współbieżności (semafory, sekcje krytyczne, oryginalny CSP).

Tworzenie oprogramowania: rygorystyczne podejście

• Cliff Jones
• 1980

Opis: Podręcznik Cliffa Jonesa Tworzenie oprogramowania: rygorystyczne podejście to pierwsza pełnometrażowa prezentacja metody rozwoju wiedeńskiego (VDM), która rozwinęła się (głównie) w wiedeńskim laboratorium badawczym IBM w ciągu ostatniej dekady i która łączy w sobie ideę programu udokładnianie według Dijkstry z udokładnianiem danych (lub reifikacją), w którym algebraicznie zdefiniowane abstrakcyjne typy danych są formalnie przekształcane w coraz bardziej „konkretne” reprezentacje.

Nauka programowania

• David Gries
• 1981

Opis: Podręcznik Davida Griesa Nauka o programowaniu opisuje najsłabszą metodę Dijkstry do formalnego wyprowadzania programów, z wyjątkiem znacznie bardziej przystępnego sposobu niż wcześniejsza dyscyplina programowania Dijkstry .

Pokazuje, jak konstruować programy, które działają poprawnie (bez błędów, poza błędami pisarskimi). Czyni to, pokazując, jak używać wyrażeń predykatów warunku wstępnego i końcowego oraz technik sprawdzania programu, aby kierować sposobem tworzenia programów.

Wszystkie przykłady w książce są na małą skalę i wyraźnie akademickie (w przeciwieństwie do świata rzeczywistego). Kładą nacisk na podstawowe algorytmy, takie jak sortowanie i scalanie oraz manipulowanie ciągami. Uwzględniono podprogramy (funkcje), ale środowiska programowania obiektowego i funkcjonalnego nie są adresowane.

Komunikowanie procesów sekwencyjnych (1985)

• SAMOCHÓD Hoare
• 1985

Opis: Podręcznik Tony'ego Hoare'a Communicating Sequential Processes (CSP) (obecnie trzecie najczęściej cytowane źródło informatyki wszechczasów) przedstawia zaktualizowany model CSP, w którym współpracujące procesy nie mają nawet zmiennych programowych i który, podobnie jak CCS, umożliwia systemom procesów być uzasadnione formalnie.

Logika liniowa (1987)

• Girard, J.-Y (1987). "Logika liniowa" (PDF) . Informatyka teoretyczna . 50 (1): 1-102. doi : 10.1016/0304-3975(87)90045-4 . Zarchiwizowane z oryginału (PDF) w dniu 2006-11-29.

Opis: Liniowa logika Girarda była przełomem w projektowaniu systemów typowania dla obliczeń sekwencyjnych i współbieżnych, zwłaszcza dla systemów typowania świadomych zasobów.

Rachunek procesów mobilnych (1989)

• R. Milner , J. Parrow, D. Walker
• 1989
• Wersja online: część 1 i część 2

Opis: Ten artykuł przedstawia rachunek Pi , uogólnienie CCS, które umożliwia mobilność procesów. Rachunek jest niezwykle prosty i stał się dominującym paradygmatem w teoretycznym badaniu języków programowania, systemów typowania i logiki programu.

Notacja Z: podręcznik referencyjny

• Spivey, JM (1992). Notacja Z: Podręcznik referencyjny (2nd ed.). Prentice Hall International. Numer ISBN 978-0-13-978529-0. Zarchiwizowane od oryginału w dniu 2016-06-20 . Źródło 2009-08-24 .

Opis: Klasyczny podręcznik Mike'a Spivey'a The Z Notation: A Reference Manual podsumowuje formalną specyfikację języka Z, notację Z , która chociaż została stworzona przez Jeana-Raymonda Abriala, rozwinęła się (głównie) na Uniwersytecie Oksfordzkim w ciągu poprzedniej dekady.

Komunikacja i współbieżność

• Robin Milner
• Prentice-Hall International, 1989

Opis: Podręcznik Robina Milnera Communication and Concurrency jest bardziej przystępną, choć wciąż zaawansowaną technicznie, ekspozycją jego wcześniejszych prac CCS.

Praktyczna teoria programowania

• Eric Hehner
• Springer, 1993, aktualne wydanie online tutaj

Opis: aktualna wersja programowania predykatywnego . Podstawa dla UTP firmy CAR Hoare . Najprostsze i najbardziej wszechstronne metody formalne.

Bibliografia