Seznam důležitých publikací v teoretické informatice - List of important publications in theoretical computer science
Toto je seznam důležitých publikací v teoretické informatice , organizovaných podle oblastí.
Některé důvody, proč lze určitou publikaci považovat za důležitou:
- Autor tématu - Publikace, která vytvořila nové téma
- Průlom - Publikace, která významně změnila vědecké znalosti
- Vliv - Publikace, která významně ovlivnila svět nebo měla obrovský dopad na výuku teoretické informatiky.
Vyčíslitelnost
Cutlandova vypočítatelnost: Úvod do teorie rekurzivních funkcí (Cambridge)
- Cutland, Nigel J. (1980). Vypočítatelnost: Úvod do teorie rekurzivních funkcí . Cambridge University Press . ISBN 978-0-521-29465-2.
Recenze tohoto raného textu Carla Smitha z Purdue University (ve Společnosti pro průmyslovou a aplikovanou matematickou recenzi ) uvádí, že jde o text s „vhodnou kombinací intuice a důslednosti… ve výkladu důkazů“, který představuje „základní výsledky klasické teorie rekurze [RT] ... ve stylu ... přístupném vysokoškolákům s minimálním matematickým pozadím ". I když prohlašuje, že „by byl vynikajícím úvodním textem pro úvodní kurz [RT] pro studenty matematiky“, navrhuje, že „instruktor musí být připraven podstatně rozšířit materiál…“, pokud je používán se studenty počítačových věd ( vzhledem k nedostatku materiálu o RT aplikacích v této oblasti).
Rozhodnutelnost teorií druhého řádu a automatů na nekonečných stromech
- Michael O. Rabin
- Transakce Americké matematické společnosti , sv. 141, s. 1–35, 1969
Popis: Příspěvek představil stromový automat , rozšíření automatů . Stromový automat měl četné aplikace k prokázání správnosti programů .
Konečné automaty a jejich rozhodovací problémy
- Michael O. Rabin a Dana S. Scott
- IBM Journal of Research and Development , sv. 3, str. 114–125, 1959
- Online verze
Popis: Matematické zpracování automatů , důkaz základních vlastností a definice nedeterministického konečného automatu .
Úvod do teorie automatů, jazyků a výpočtu
Popis: Populární učebnice.
O určitých formálních vlastnostech gramatik
- Chomsky, N. (1959). "O určitých formálních vlastnostech gramatik" . Informace a kontrola . 2 (2): 137–167. doi : 10,1016 / S0019-9958 (59) 90362-6 .
Popis: Tento článek představil takzvanou Chomského hierarchii , hierarchii omezení tříd formálních gramatik, které generují formální jazyky .
Na vypočítatelných číslech, s aplikací na Entscheidungsproblem
- Alan Turing
-
Proceedings of the London Mathematical Society , Series 2 , sv. 42, str. 230–265, 1937, doi : 10,1112 / plms / s2-42.1.230 .
Errata se objevila ve sv. 43, str. 544–546, 1938, doi : 10,1112 / plms / s2-43,6,544 . - HTML verze , verze PDF
Popis: Tento článek stanoví limity počítačové vědy. Definoval Turingův stroj , model pro všechny výpočty. Na druhou stranu to dokázalo nerozhodnutelnost problému zastavení a Entscheidungsproblem a našlo tak limity možného výpočtu.
Rekurzivní funkce
- Péter, Rózsa (1951). Rekurzivní funkce . Akademický tisk. ISBN 9780125526500.
První učebnice teorie rekurzivních funkcí . Kniha prošla mnoha vydáními a Péterovi vynesla Kossuthovu cenu od maďarské vlády. Recenze Raphaela M. Robinsona a Stephena Kleene ocenili knihu za poskytnutí účinného základního úvodu pro studenty.
Zastoupení událostí v nervových sítích a konečných automatech
- SC Kleene
- Memorandum o projektu US Air Force Rand Research RM-704 , 1951
- Online verze
- publikováno v: Shannon, Claude ; McCarthy, John , eds. (1956). Studie automatů . OCLC 564148 .
Popis: tento článek představil konečné automaty , regulární výrazy a regulární jazyky a navázal jejich spojení.
Teorie výpočetní složitosti
Arora & Barakova výpočetní složitost a Goldreichova výpočetní složitost (oba Cambridge)
- Sanjeev Arora a Boaz Barak, „Výpočetní složitost: moderní přístup“, Cambridge University Press, 2009, 579 stran, vázaná kniha
- Oded Goldreich, „Výpočetní složitost: Konceptuální perspektiva, Cambridge University Press, 2008, 606 stran, vázaná kniha
Kromě odhadovatelného tisku, který přináší tyto nedávné texty, jsou velmi pozitivně hodnoceny ve zprávách ACM SIGACT News Danielem Aponem z University of Arkansas, který je identifikuje jako „učebnice pro kurz teorie složitosti, zaměřený na předčasné absolventy… nebo ... pokročilí vysokoškoláci… [s] četnými, jedinečnými silnými stránkami a velmi málo slabostmi, “a uvádí, že oba jsou:
„vynikající texty, které důkladně pokrývají jak šíři, tak hloubku teorie výpočetní složitosti ... [od] autorů ... každý [kteří] jsou obry v teorii výpočetní techniky [kde každý bude] ... výjimečný referenční text pro odborníky v pole… [a to] ... teoretikům, vědcům a instruktorům jakékoli myšlenkové školy bude každá kniha užitečná. “
Recenzent konstatuje, že v [Arora a Barak] existuje určitý pokus zahrnout velmi aktuální materiál, zatímco Goldreich se více zaměřuje na rozvoj kontextuálního a historického základu pro každý představený koncept, “a že„ tleská [s ] všichni… autoři za vynikající příspěvky. “
Strojově nezávislá teorie složitosti rekurzivních funkcí
- Blum, Manuel (1967). „Strojově nezávislá teorie složitosti rekurzivních funkcí“ (PDF) . Deník ACM . 14 (2): 322–336. doi : 10,1145 / 321386,321395 . S2CID 15710280 .
Popis: Blumovy axiomy .
Algebraické metody pro interaktivní kontrolní systémy
- Lund, C .; Fortnow, L .; Karloff, H .; Nisan, N. (1992). "Algebraické metody pro interaktivní kontrolní systémy". Deník ACM . 39 (4): 859–868. CiteSeerX 10.1.1.41.9477 . doi : 10,1145 / 146585,146605 . S2CID 207170996 .
Popis: Tento dokument ukázal, že PH je obsažen v IP .
Složitost postupů prokazování věty
- Cook, Stephen A. (1971). „Složitost postupů prokazujících věty“ (PDF) . Sborník z 3. ročníku sympozia ACM o teorii práce s počítači : 151–158. CiteSeerX 10.1.1.406.395 . doi : 10,1145 / 800157,805047 . S2CID 7573663 .
Popis: Tento článek představil koncept NP-úplnosti a prokázal, že problém s booleovskou uspokojivostí (SAT) je NP-Complete . Všimněte si, že podobné myšlenky vyvinul nezávisle o něco později Leonid Levin na „Levin, Problémy univerzálního vyhledávání. Problemy Peredachi Informatsii 9 (3): 265–266, 1973“.
Počítače a neodolatelnost: Průvodce po teorii NP-úplnosti
- Garey, Michael R .; Johnson, David S. (1979). Počítače a neodolatelnost: Průvodce po teorii NP-úplnosti . New York: Freeman. ISBN 978-0-7167-1045-5.
Popis: Hlavní význam této knihy je způsoben jejím rozsáhlým seznamem více než 300 problémů NP-Complete . Tento seznam se stal běžným odkazem a definicí. Ačkoli kniha vyšla jen několik let po definici konceptu, byl nalezen tak rozsáhlý seznam.
Stupeň obtížnosti výpočtu funkce a částečné uspořádání rekurzivních množin
- Rabin, Michael O. (1960). „Stupeň obtížnosti výpočtu funkce a částečné řazení rekurzivních množin“ (PDF) . Technická zpráva č. 2 . Jeruzalém: Hebrejská univerzita.
Popis: Tato technická zpráva byla první publikací, která hovořila o tom, co bylo později přejmenováno na výpočetní složitost
Jak dobrá je simplexní metoda?
- Victor Klee a George J. Minty
- Klee, Victor ; Minty, George J. (1972). "Jak dobrý je simplexní algoritmus?". V Shisha, Oved (ed.). Nerovnosti III (Sborník ze třetího sympozia o nerovnostech konaného na Kalifornské univerzitě v Los Angeles v Kalifornii od 1. do 9. září 1969 věnovaný památce Theodora S. Motzkina) . New York-Londýn: Academic Press. str. 159–175. MR 0332165 .
Popis: Vyrobeno v „Klee-mátový krychle“ o rozměrech D , jehož 2 D rohy jsou vzájemně navštěvují Dantzig ‚s simplex algoritmu pro lineární optimalizaci .
Jak postavit náhodné funkce
- Goldreich, O .; Goldwasser, S .; Micali, S. (1986). "Jak vytvořit náhodné funkce" (PDF) . Deník ACM . 33 (4): 792–807. doi : 10,1145 / 6490,6503 . S2CID 17064126 .
Popis: Tento článek ukázal, že existence jednosměrných funkcí vede k výpočetní náhodnosti .
IP = PSPACE
- Shamir, A. (1992). "IP = PSPACE". Deník ACM . 39 (4): 869–877. doi : 10,1145 / 146585,146609 . S2CID 315182 .
Popis: IP je třída složitosti, jejíž charakterizace (založená na interaktivních důkazních systémech ) se zcela liší od obvyklých výpočetních tříd ohraničených časem a prostorem. V tomto článku Shamir rozšířil techniku předchozí práce Lunda et al., Aby ukázal, že PSPACE je obsažen v IP , a tedy IP = PSPACE, takže každý problém v jedné třídě složitosti je řešitelný v druhé.
Redukovatelnost mezi kombinatorickými problémy
- RM Karp
- V publikaci RE Miller a JW Thatcher, editors, Complexity of Computer Computations , Plenum Press, New York, NY, 1972, str. 85–103
Popis: Tento příspěvek ukázal, že 21 různých problémů je NP-Complete a ukázal důležitost konceptu.
Znalostní složitost systémů interaktivních důkazů
- Goldwasser, S .; Micali, S .; Rackoff, C. (1989). „Znalostní složitost interaktivních zkušebních systémů“ (PDF) . SIAM J. Comput. 18 (1): 186–208. doi : 10.1137 / 0218012 .
Popis: Tento příspěvek představil koncept nulových znalostí .
Dopis od Gödela von Neumannovi
- Kurt Gödel
- Dopis od Gödel do John von Neumann , 20. března 1956
- Online verze
Popis: Gödel pojednává o myšlence účinného univerzálního testeru vět.
O výpočetní složitosti algoritmů
- Hartmanis, Juris ; Stearns, Richard (1965). Msgstr "O výpočetní složitosti algoritmů" . Transakce Americké matematické společnosti . 117 : 285–306. doi : 10.1090 / s0002-9947-1965-0170805-7 .
Popis: Tento příspěvek dal výpočetní složitosti své jméno a semeno.
Cesty, stromy a květiny
- Edmonds, J. (1965). "Cesty, stromy a květiny". Kanadský žurnál matematiky . 17 : 449–467. doi : 10,4153 / CJM-1965-045-4 .
Popis: Existuje polynomiální časový algoritmus k nalezení maximální shody v grafu, který není bipartitní, a další krok k myšlence výpočetní složitosti . Více informací viz [2] .
Teorie a aplikace funkcí padacích dveří
- Yao, AC (1982). "Teorie a aplikace funkcí padacích dveří". 23. výroční sympozium o základech informatiky (SFCS 1982) . 80–91. doi : 10,1109 / SFCS.1982,45 .
Popis: Tento příspěvek vytváří teoretický rámec pro funkce padacích dveří a popisuje některé jejich aplikace, například v kryptografii . Všimněte si, že koncept funkcí padacích dveří byl přinesen v „Nových směrech v kryptografii“ o šest let dříve (viz část V „Problémové vzájemné vztahy a trapové dveře.“).
Výpočetní složitost
Popis: V úvodu do teorie výpočetní složitosti kniha vysvětluje autorovu charakteristiku P-SPACE a další výsledky.
Interaktivní důkazy a tvrdost přibližných klik
- Feige, U .; Goldwasser, S .; Lovász, L .; Safra, S .; Szegedy, M. (1996). "Interaktivní důkazy a tvrdost přibližných klik" . Deník ACM . 43 (2): 268–292. doi : 10,1145 / 226643,226652 .
Pravděpodobnostní kontrola důkazů: nová charakteristika NP
- Arora, S .; Safra, S. (1998). "Pravděpodobnostní kontrola důkazů: nová charakteristika NP". Deník ACM . 45 : 70–122. doi : 10,1145 / 273865,273901 . S2CID 751563 .
Důkazové ověření a tvrdost problémů aproximace
- Arora, S .; Lund, C .; Motwani, R .; Sudan, M .; Szegedy, M. (1998). Msgstr "Ověření důkazu a tvrdost problémů s aproximací". Deník ACM . 45 (3): 501–555. CiteSeerX 10.1.1.145.4652 . doi : 10,1145 / 278298,278306 . S2CID 8561542 .
Popis: Tyto tři práce prokázaly překvapivou skutečnost, že určité problémy v NP zůstávají těžké, i když je vyžadováno pouze přibližné řešení. Viz teorém PCP .
Vnitřní výpočetní obtížnost funkcí
- Cobham, Alan (1964). „Vnitřní výpočetní obtížnost funkcí“ (PDF) . Sborník příspěvků z mezinárodního kongresu logiky, metodologie a filozofie vědy z roku 1964 : 24–30.
Popis: První definice třídy složitosti P. Jeden ze základních článků teorie složitosti.
Algoritmy
„Strojový program pro dokazování věty“
- Davis, M .; Logemann, G .; Loveland, D. (1962). „Strojový program pro dokazování vět“ (PDF) . Komunikace ACM . 5 (7): 394–397. doi : 10,1145 / 368273,368557 . hdl : 2027 / mdp.39015095248095 . S2CID 15866917 .
Popis: Algoritmus DPLL . Základní algoritmus pro SAT a další NP-Complete problémy.
„Strojově orientovaná logika založená na principu rozlišení“
- Robinson, JA (1965). „Strojově orientovaná logika založená na principu rozlišení“. Deník ACM . 12 : 23–41. doi : 10,1145 / 321250,321253 . S2CID 14389185 .
Popis: První popis rozlišení a unifikace použitých při automatizovaném dokazování vět ; používá se v Prologu a logickém programování .
„Problém obchodního cestujícího a minimální kostry“
- Held, M .; Karp, RM (1970). „Problém obchodního cestujícího a minimální rozpětí stromů“. Operační výzkum . 18 (6): 1138–1162. doi : 10,1287 / opre.18.6.1138 .
Popis: Použití algoritmu pro minimální kostru jako aproximačního algoritmu pro problém obchodního cestujícího NP-Complete . Aproximační algoritmy se staly běžnou metodou pro řešení problémů NP-Complete.
"Polynomiální algoritmus v lineárním programování"
- LG Khachiyan
- Sovětská matematika - Doklady , roč. 20, s. 191–194, 1979
Popis: Dlouho neexistoval prokazatelně polynomiální časový algoritmus pro problém lineárního programování . Khachiyan byl první, kdo poskytl algoritmus, který byl polynomiální (a nejen že byl dostatečně rychlý po většinu času jako předchozí algoritmy). Později Narendra Karmarkar představil rychlejší algoritmus na adrese: Narendra Karmarkar, „Nový polynomiální časový algoritmus pro lineární programování“, Combinatorica , svazek 4, č. 4. 4, s. 373–395, 1984.
"Pravděpodobnostní algoritmus pro testování primality"
- Rabin, M. (1980). Msgstr "Pravděpodobnostní algoritmus pro testování primality" . Žurnál teorie čísel . 12 (1): 128–138. doi : 10.1016 / 0022-314X (80) 90084-0 .
Popis: Příspěvek představil Miller-Rabinův test primality a nastínil program randomizovaných algoritmů .
„Optimalizace simulovaným žíháním“
- Kirkpatrick, S .; Gelatt, CD; Vecchi, MP (1983). "Optimalizace simulovaným žíháním". Věda . 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 .
Popis: Tento článek popisuje simulované žíhání , které je nyní velmi běžnou heuristikou problémů NP-Complete .
Umění počítačového programování
Popis: Tato monografie má čtyři svazky pokrývající populární algoritmy. Algoritmy jsou psány jak v angličtině, tak v montážním jazyce MIX (nebo montážním jazyce MMIX v novějších svazcích). Díky tomu jsou algoritmy srozumitelné a přesné. Použití nízkoúrovňového programovacího jazyka však frustruje některé programátory, kteří jsou více obeznámeni s moderními strukturovanými programovacími jazyky .
Algoritmy + datové struktury = programy
- Niklaus Wirth
- Prentice Hall, 1976, ISBN 0-13-022418-9
Popis: Raná, vlivná kniha o algoritmech a datových strukturách s implementacemi v Pascalu.
Návrh a analýza počítačových algoritmů
- Alfred V. Aho , John E. Hopcroft a Jeffrey D. Ullman
- Addison-Wesley, 1974, ISBN 0-201-00029-6
Popis: Jeden ze standardních textů o algoritmech pro období přibližně 1975–1985.
Jak to vyřešit počítačem
- Dromey, RG (1982). Jak to vyřešit počítačem . Prentice-Hall International. ISBN 978-0-13-434001-2.
Popis: Vysvětluje Proč s algoritmů a datových struktur. Vysvětluje tvůrčí proces , linii uvažování , faktory designu za inovativními řešeními.
Algoritmy
- Robert Sedgewick
- Addison-Wesley, 1983, ISBN 0-201-06672-6
Popis: Velmi populární text o algoritmech na konci 80. let. Bylo přístupnější a čitelnější (ale elementárnější) než Aho, Hopcroft a Ullman. Existuje novějších vydání.
Úvod do algoritmů
- Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest a Clifford Stein
- 3. vydání, MIT Press, 2009, ISBN 978-0-262-03384-8 .
Popis: Tato učebnice se stala tak populární, že je téměř de facto standardem pro výuku základních algoritmů. První vydání (s prvními třemi autory) vyšlo v roce 1990, druhé vydání v roce 2001 a třetí v roce 2009.
Algoritmická teorie informací
„Na tabulkách náhodných čísel“
- Kolmogorov, Andrej N. (1963). "Na tabulkách náhodných čísel". Sankhya Ser. . 25 : 369–375. MR 0178484 .
- Kolmogorov, Andrej N. (1963). "Na tabulkách náhodných čísel" . Teoretická informatika . 207 (2): 387–395. doi : 10,1016 / S0304-3975 (98) 00075-9 . MR 1643414 .
Popis: Navrhl výpočetní a kombinatorický přístup k pravděpodobnosti.
„Formální teorie indukční inference“
- Ray Solomonoff
- Information and Control , roč. 7, s. 1–22 a 224–254, 1964
- Kopie online: část I , část II
Popis: To byl začátek algoritmické teorie informací a Kolmogorovovy složitosti . Všimněte si, že ačkoli Kolmogorovova složitost je pojmenována po Andrey Kolmogorovovi , řekl, že zárodky této myšlenky jsou způsobeny Rayem Solomonoffem . Andrey Kolmogorov do této oblasti hodně přispěl, ale v dalších článcích.
"Algoritmická teorie informací"
- 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 / kolo 214.0350 . Archivovány z původního (PDF) 30. května 2009.
Popis: Úvod do algoritmické teorie informací jedním z důležitých osob v této oblasti.
Informační teorie
„Matematická teorie komunikace“
- Shannon, CE (1948). "Matematická teorie komunikace" . Technický deník Bell System . 27 (3): 379–423, 623–656. doi : 10,1002 / j.1538-7305.1948.tb01338.x . hdl : 10338.dmlcz / 101429 .
Popis: Tento příspěvek vytvořil pole teorie informací .
„Kódy pro detekci a opravu chyb“
- Hamming, Richard (1950). Msgstr "Kódy detekce a opravy chyb" . Technický deník Bell System . 29 (2): 147–160. doi : 10,1002 / j.1538-7305.1950.tb00463.x . hdl : 10945/46756 .
Popis: V tomto příspěvku představil Hamming myšlenku kódu opravujícího chyby . Vytvořil Hammingův kód a Hammingovu vzdálenost a vyvinul metody pro ověření optimality kódu.
„Metoda pro konstrukci kódů minimální redundance“
- Huffman, D. (1952). „Metoda pro konstrukci kódů minimální redundance“ (PDF) . Sborník IRE . 40 (9): 1098–1101. doi : 10,1109 / JRPROC.1952.273898 .
Popis: Huffmanovo kódování .
"Univerzální algoritmus pro sekvenční kompresi dat"
- Ziv, J .; Lempel, A. (1977). Msgstr "Univerzální algoritmus pro sekvenční kompresi dat" . Transakce IEEE na teorii informací . 23 (3): 337–343. CiteSeerX 10.1.1.118.8921 . doi : 10.1109 / TIT.1977.1055714 . hdl : 10338.dmlcz / 142947 . Archivovány od originálu dne 2003-12-04.
Popis: Algoritmus komprese LZ77 .
Základy teorie informace
- T. Cover ; J. Thomas (1991). Základy teorie informace . str. 38 - 42 . ISBN 978-0-471-06259-2.
Popis: Populární úvod do teorie informací.
Formální ověření
Přiřazení významu programům
- Floyd, Robert (1967). "Přiřazení významu programům". Matematické aspekty informatiky (PDF) . Sborník sympozií z aplikované matematiky. 19 . 19–32. doi : 10,1090 / psapm / 019/0235771 . ISBN 9780821813195.
Popis: Mezník Robert Floyd Assigning Meanings to Programmes zavádí metodu indukčních tvrzení a popisuje, jak může být program s poznámkami s tvrzeními prvního řádu zobrazen tak, aby vyhovoval specifikaci před a po podmínce - článek také zavádí pojmy invariantní smyčky a ověřovací podmínka.
Axiomatický základ pro počítačové programování
- Hoare, CAR (říjen 1969). „Axiomatický základ pro počítačové programování“ (PDF) . Komunikace ACM . 12 (10): 576–580. doi : 10,1145 / 363235,363259 . S2CID 207726175 . Archivovány z původního (PDF) 04.03.2016.
Popis: Papír Tonyho Hoare Axiomatický základ pro počítačové programování popisuje soubor pravidel pro odvození (tj. Formální důkaz) pro fragmenty programovacího jazyka podobného Algolu popsaného v pojmech (nyní nazývaných) trojic.
Hlídané příkazy, neurčitost a formální odvozování programů
- Dijkstra, EW (1975). "Hlídané příkazy, neurčitost a formální odvozování programů" . Komunikace ACM . 18 (8): 453–457. doi : 10,1145 / 360933,360975 . S2CID 1679242 .
Popis: Papír Edsgera Dijkstra Strážené příkazy, neurčitost a formální odvozování programů (rozšířený o jeho učebnici postgraduálního studia A Disciplína programování z roku 1976) navrhuje, aby místo formálního ověření programu po jeho napsání (tj. Post facto) byly programy a jejich formální důkazy by měly být vyvinuty ruku v ruce (pomocí predikátových transformátorů k postupnému upřesnění nejslabších předpokladů), metoda známá jako programové (nebo formální) zpřesnění (nebo odvození) nebo někdy „správnost podle konstrukce“.
Prokazování tvrzení o paralelních programech
- Edward A. Ashcroft
- J. Comput. Syst. Sci. 10 (1): 110–135 (1975) doi : 10,1016 / s0022-0000 (75) 80018-3
Popis: Článek, který představil důkazy invariance souběžných programů.
Axiomatická důkazní technika pro paralelní programy I
- Susan S.Owicki , David Gries
- Acta Inform. 6: 319–340 (1976)
Popis: V tomto příspěvku, spolu se stejnými autorovými příspěvky „Ověření vlastností paralelních programů: Axiomatický přístup. Komun. ACM 19 (5): 279–285 (1976)“, byl představen axiomatický přístup k verifikaci paralelních programů.
Disciplína programování
- Edsger W. Dijkstra
- 1976
Popis: Klasická postgraduální učebnice Edsgera Dijkstra A Disciplína programování rozšiřuje jeho dřívější práci Strážené příkazy, neurčitost a formální odvozování programů a pevně zakládá princip formálního odvození programů (a jejich důkazů) z jejich specifikace.
Denotační sémantika
- Joe Stoy
- 1977
Popis: Denotační sémantika Joe Stoyho je první (postgraduální úroveň) knižní expozicí matematického (nebo funkčního) přístupu k formální sémantice programovacích jazyků (na rozdíl od provozních a algebraických přístupů).
Časová logika programů
- Pnueli, A. (1977). Msgstr "Časová logika programů". 18. výroční sympozium o základech informatiky (SFCS 1977) . IEEE. str. 46–57. doi : 10,1109 / SFCS.1977,32 . S2CID 117103037 .
Popis: Jako metoda formálního ověření bylo navrženo použití časové logiky .
Charakterizace vlastností správnosti paralelních programů pomocí fixních bodů (1980)
- E. Allen Emerson , Edmund M. Clarke
- V Proc. 7. mezinárodní kolokvium o jazycích a programování automatů, strany 169–181, 1980
Popis: Kontrola modelu byla zavedena jako postup kontroly správnosti souběžných programů.
Komunikující sekvenční procesy (1978)
- CAR Hoare
- 1978
Popis: Dokument Tonyho Hoare (původní) komunikující sekvenční procesy (CSP) zavádí myšlenku souběžných procesů (tj. Programů), které nesdílejí proměnné, ale místo toho spolupracují pouze výměnou synchronních zpráv.
Počet komunikačních systémů
- Robin Milner
- 1980
Popis: Dokument Robin Milner A Calculus of Communicating Systems (CCS) popisuje procesní algebru umožňující formální zdůvodnění systémů souběžných procesů, něco, co u dřívějších modelů souběžnosti (semafory, kritické sekce, původní CSP) nebylo možné.
Vývoj softwaru: přísný přístup
- Cliff Jones
- 1980
Popis: Učebnice Cliffa Jonese Vývoj softwaru: Rigorózní přístup je první celovečerní expozicí metody Vienna Development Method (VDM), která se v minulém desetiletí vyvinula (hlavně) ve vídeňské výzkumné laboratoři IBM a kombinuje myšlenku programu upřesnění podle Dijkstra s upřesněním (nebo reifikací) dat, přičemž algebraicky definované abstraktní datové typy jsou formálně transformovány do postupně „konkrétnějších“ reprezentací.
Věda o programování
- David Gries
- 1981
Popis: Učebnice Davida Griesa The Science of Programming popisuje Dijkstrovu nejslabší předpokladovou metodu odvozování formálního programu, s výjimkou mnohem dostupnějšího způsobu než Dijkstrův dřívější Disciplína programování .
Ukazuje, jak vytvořit programy, které fungují správně (bez chyb, kromě chyb při psaní). Dělá to tím, že ukazuje, jak používat předpokladové a postkondiční predikátové výrazy a techniky dokazování programů jako vodítko při vytváření programů.
Příklady v knize jsou všechny malého rozsahu a jasně akademické (na rozdíl od skutečného světa). Zdůrazňují základní algoritmy, jako je třídění a slučování a manipulace s řetězci. Subrutiny (funkce) jsou zahrnuty, ale objektově orientovaná a funkční programovací prostředí nejsou řešena.
Komunikující sekvenční procesy (1985)
- CAR Hoare
- 1985
Popis: Učebnice Tonyho Hoareho Communicating Sequential Processes (CSP) (v současné době třetí nejcitovanější reference na počítačové vědy všech dob) představuje aktualizovaný model CSP, ve kterém spolupracující procesy nemají ani programové proměnné a který stejně jako CCS umožňuje systémům procesů být formálně odůvodněn.
Lineární logika (1987)
- Girard, J.-Y (1987). „Lineární logika“ (PDF) . Teoretická informatika . 50 (1): 1–102. doi : 10.1016 / 0304-3975 (87) 90045-4 . Archivovány z původního (PDF) 29. 11. 2006.
Popis: Girardova lineární logika byla průlomem v navrhování typovacích systémů pro sekvenční a souběžné výpočty, zejména pro systémy typování založené na zdrojích.
Kalkul mobilních procesů (1989)
Popis: Tento článek představuje Pi-Calculus , zobecnění CCS, které umožňuje mobilitu procesů. Počet je extrémně jednoduchý a stal se dominantním paradigmatem v teoretickém studiu programovacích jazyků, typovacích systémů a programové logiky.
Z notace: Referenční příručka
- Spivey, JM (1992). The Z Notation: A Reference Manual (2nd ed.). Prentice Hall International. ISBN 978-0-13-978529-0. Archivovány od originálu na 2016-06-20 . Citováno 2009-08-24 .
Popis: Klasická učebnice Mikea Spiveyho The Z Notation: A Reference Manual shrnuje formální specifikační Z notaci , která, přestože ji vytvořil Jean-Raymond Abrial, se v minulém desetiletí vyvinula (hlavně) na Oxfordské univerzitě.
Komunikace a souběžnost
- Robin Milner
- Prentice-Hall International, 1989
Popis: Učebnice Robina Milnera Komunikace a souběžnost je přístupnější, i když stále technicky vyspělou, expozicí jeho dřívější práce s CCS.
Praktická teorie programování
- Eric Hehner
- Springer, 1993, aktuální vydání online zde
Popis: aktuální verze Predicative programování . Základ pro UTP společnosti CAR Hoare . Nejjednodušší a nejkomplexnější formální metody.
Reference
- ACM Special Interest Group on Algorithms and Computory Theory (2011). „Ceny: Gödelova cena“ . Archivovány od originálu dne 22. dubna 2018 . Vyvolány 8 October 2011 .