Liste des publications importantes en informatique théorique - List of important publications in theoretical computer science
Il s'agit d'une liste de publications importantes en informatique théorique , classées par domaine.
Quelques raisons pour lesquelles une publication particulière peut être considérée comme importante :
- Créateur de sujet – Une publication qui a créé un nouveau sujet
- Breakthrough – Une publication qui a considérablement changé les connaissances scientifiques
- Influence – Une publication qui a considérablement influencé le monde ou qui a eu un impact massif sur l'enseignement de l'informatique théorique.
Calculabilité
Calculabilité de Cutland : une introduction à la théorie des fonctions récursives (Cambridge)
- Cutland, Nigel J. (1980). Calculabilité : une introduction à la théorie des fonctions récursives . Presse de l'Université de Cambridge . ISBN 978-0-521-29465-2.
L'examen de ce premier texte par Carl Smith de l'Université Purdue (dans la Society for Industrial and Applied Mathematics Reviews ), rapporte qu'il s'agit d'un texte avec « un mélange approprié d'intuition et de rigueur… dans l'exposition des preuves » qui présente « les résultats de la théorie de la récursivité classique [RT]... dans un style... accessible aux étudiants de premier cycle avec un minimum de connaissances mathématiques". Alors qu'il déclare qu'il « ferait un excellent texte d'introduction pour un cours d'introduction en [RT] pour les étudiants en mathématiques », il suggère qu'un « instructeur doit être prêt à augmenter substantiellement le matériel… » lorsqu'il est utilisé avec des étudiants en informatique ( étant donné le manque de matériel sur les applications RT dans ce domaine).
Décidabilité des théories du second ordre et des automates sur des arbres infinis
- Michael O. Rabin
- Transactions de l'American Mathematical Society , vol. 141, p. 1-35, 1969
Description : L'article présentait l' automate de l' arbre , une extension des automates . L'automate d'arbre a eu de nombreuses applications aux preuves d' exactitude des programmes .
Les automates finis et leurs problèmes de décision
- Michael O. Rabin et Dana S. Scott
- IBM Journal of Research and Development , vol. 3, p. 114-125, 1959
- Version en ligne
Description : Traitement mathématique des automates , preuve des propriétés du noyau et définition d' un automate fini non déterministe .
Introduction à la théorie des automates, aux langages et au calcul
Description : Un manuel populaire.
Sur certaines propriétés formelles des grammaires
- Chomsky, N. (1959). "Sur certaines propriétés formelles des grammaires" . Informations et contrôle . 2 (2) : 137-167. doi : 10.1016/S0019-9958 (59) 90362-6 .
Description : Cet article a présenté ce qui est maintenant connu sous le nom de hiérarchie de Chomsky , une hiérarchie de confinement de classes de grammaires formelles qui génèrent des langages formels .
Sur des nombres calculables, avec une application au Entscheidungsproblem
- Alain Turing
-
Actes de la London Mathematical Society , série 2 , vol. 42, pp. 230-265, 1937, doi : 10.1112/plms/s2-42.1.230 .
Errata est apparu dans le vol. 43, pp. 544-546, 1938, doi : 10.1112/plms/s2-43.6.544 . - Version HTML , version PDF
Description : Cet article pose les limites de l'informatique. Il définit la Machine de Turing , un modèle pour tous les calculs. D'autre part, il a prouvé l'indécidabilité du problème d'arrêt et du problème d' Entscheidungs et a ainsi trouvé les limites du calcul possible.
Fonctions récursives
- Péter, Rozsa (1951). Fonctions récursives . Presse académique. ISBN 9780125526500.
Le premier manuel sur la théorie des fonctions récursives . Le livre est passé par de nombreuses éditions et a obtenu Péter le prix Kossuth du hongrois gouvernement. Les critiques de Raphael M. Robinson et Stephen Kleene ont félicité le livre pour avoir fourni une introduction élémentaire efficace aux élèves.
Représentation des événements dans les réseaux nerveux et les automates finis
- SC Kleene
- US Air Force Projet Rand Research Memorandum RM-704 , 1951
- Version en ligne
- republié dans : Shannon, Claude ; McCarthy, John , éd. (1956). Études d'automates . OCLC 564148 .
Description : cet article présente les automates finis , les expressions régulières et les langages réguliers , et établit leur connexion.
Théorie de la complexité computationnelle
Arora et de Barak complexité informatique et de Goldreich complexité informatique ( à la fois Cambridge)
- Sanjeev Arora et Boaz Barak, "Computational Complexity: A Modern Approach", Cambridge University Press, 2009, 579 pages, couverture rigide
- Oded Goldreich, "Computational Complexity: A Conceptual Perspective, Cambridge University Press, 2008, 606 pages, couverture rigide
Outre la presse estimable mettant en avant ces textes récents, ils sont très positivement commentés dans SIGACT News de l'ACM par Daniel Apon de l'Université de l'Arkansas, qui les identifie comme "des manuels pour un cours de théorie de la complexité, destiné aux jeunes diplômés… ou... étudiants de premier cycle avancés… [avec] de nombreuses forces uniques et très peu de faiblesses », et déclare que les deux sont :
« d'excellents textes qui couvrent à la fois l'étendue et la profondeur de la théorie de la complexité informatique… [par] des auteurs… chacun [qui] sont des géants de la théorie de l'informatique [où chacun sera]… un texte de référence exceptionnel pour les experts en domaine… [et que] ... les théoriciens, les chercheurs et les instructeurs de n'importe quelle école de pensée trouveront l'un ou l'autre livre utile.
L'examinateur note qu'il y a "une tentative définitive dans [Arora et Barak] d'inclure du matériel très à jour, tandis que Goldreich se concentre davantage sur le développement d'une base contextuelle et historique pour chaque concept présenté", et qu'il "applaudi[s] ] tous… les auteurs pour leurs contributions exceptionnelles."
Une théorie indépendante de la machine de la complexité des fonctions récursives
- Blum, Manuel (1967). « Une théorie indépendante de la machine de la complexité des fonctions récursives » (PDF) . Journal de l'ACM . 14 (2) : 322-336. doi : 10.1145/321386.321395 . S2CID 15710280 .
Description : Les axiomes de Blum .
Méthodes algébriques pour les systèmes de preuve interactifs
- Lund, C. ; Fortnow, L. ; Karloff, H.; Nisan, N. (1992). « Méthodes algébriques pour les systèmes de preuve interactifs ». Journal de l'ACM . 39 (4) : 859-868. CiteSeerX 10.1.1.41.9477 . doi : 10.1145/146585.146605 . S2CID 207170996 .
Description : Cet article a montré que PH est contenu dans IP .
La complexité des procédures de preuve de théorème
- Cook, Stephen A. (1971). « La complexité des procédures de preuve de théorème » (PDF) . Actes du 3e Symposium annuel de l'ACM sur la théorie de l'informatique : 151-158. CiteSeerX 10.1.1.406.395 . doi : 10.1145/800157.805047 . S2CID 7573663 .
Description : Cet article a introduit le concept de NP-Complet et a prouvé que le problème de satisfiabilité booléenne (SAT) est NP-Complet . Notez que des idées similaires ont été développées indépendamment un peu plus tard par Leonid Levin dans "Levin, Universal Search Problems. Problemy Peredachi Informatsii 9(3):265-266, 1973".
Ordinateurs et intraitabilité : un guide de la théorie de la NP-complétude
- Garey, Michael R. ; Johnson, David S. (1979). Ordinateurs et intraitabilité : un guide de la théorie de la NP-complétude . New York : Freeman. ISBN 978-0-7167-1045-5.
Description : L'importance principale de ce livre est due à sa longue liste de plus de 300 problèmes NP-Complets . Cette liste est devenue une référence et une définition communes. Bien que le livre n'ait été publié que quelques années après la définition du concept, une liste aussi longue a été trouvée.
Degré de difficulté du calcul d'une fonction et d'un ordre partiel d'ensembles récursifs
- Rabin, Michael O. (1960). « Degré de difficulté de calculer une fonction et un ordre partiel d'ensembles récursifs » (PDF) . Rapport technique n ° 2 . Jérusalem : Université hébraïque.
Description : Ce rapport technique a été la première publication à parler de ce qui a été rebaptisé plus tard la complexité de calcul
Quelle est la qualité de la méthode simplex?
- Victor Klee et George J. Minty
- Klee, Victor ; Minty, George J. (1972). "Quelle est la qualité de l'algorithme du simplexe ?". Dans Shisha, Oved (éd.). Inequalities III (Actes du troisième symposium sur les inégalités tenu à l'Université de Californie, Los Angeles, Californie, du 1er au 9 septembre 1969, dédié à la mémoire de Theodore S. Motzkin) . New York-Londres : Academic Press. p. 159–175. MR 0332165 .
Description: Construit le « cube Klee-Minty » en dimension D , dont 2 D coins sont chacun visités par Danzig d » algorithme simplex pour l' optimisation linéaire .
Comment construire des fonctions aléatoires
- Goldreich, O. ; Goldwasser, S. ; Micali, S. (1986). "Comment construire des fonctions aléatoires" (PDF) . Journal de l'ACM . 33 (4) : 792-807. doi : 10.1145/6490.6503 . S2CID 17064126 .
Description : Cet article a montré que l'existence de fonctions à sens unique conduit à un calcul aléatoire .
IP = PSPACE
- Shamir, A. (1992). "IP = PSPACE". Journal de l'ACM . 39 (4) : 869-877. doi : 10.1145/146585.146609 . S2CID 315182 .
Description : IP est une classe de complexité dont la caractérisation (basée sur des systèmes de preuve interactifs ) est assez différente des classes de calcul bornées temps/espace habituelles. Dans cet article, Shamir a étendu la technique de l'article précédent de Lund, et al., pour montrer que PSPACE est contenu dans IP , et donc IP = PSPACE, de sorte que chaque problème d'une classe de complexité peut être résolu dans l'autre.
Réductibilité parmi les problèmes combinatoires
- RM Karp
- Dans RE Miller et JW Thatcher, éditeurs, Complexity of Computer Computations , Plenum Press, New York, NY, 1972, pp. 85-103
Description : Cet article a montré que 21 problèmes différents sont NP-Complets et a montré l'importance du concept.
La complexité des connaissances des systèmes de preuve interactifs
- Goldwasser, S. ; Micali, S. ; Rackoff, C. (1989). « La complexité des connaissances des systèmes de preuve interactifs » (PDF) . SIAM J. Comput. 18 (1) : 186-208. doi : 10.1137/0218012 .
Description : Cet article a introduit le concept de connaissance zéro .
Une lettre de Gödel à von Neumann
- Kurt Gödel
- Une lettre de Gödel à John von Neumann , 20 mars 1956
- Version en ligne
Description : Gödel discute de l'idée d'un prouveur de théorème universel efficace.
Sur la complexité calculatoire des algorithmes
- Hartmanis, Juris ; Stearns, Richard (1965). "Sur la complexité computationnelle des algorithmes" . Transactions de l'American Mathematical Society . 117 : 285-306. doi : 10.1090/s0002-9947-1965-0170805-7 .
Description : Cet article a donné son nom et son germe à la complexité informatique .
Chemins, arbres et fleurs
- Edmonds, J. (1965). "Des chemins, des arbres et des fleurs". Revue canadienne de mathématiques . 17 : 449-467. doi : 10.4153/CJM-1965-045-4 .
Description : Il existe un algorithme en temps polynomial pour trouver une correspondance maximale dans un graphe qui n'est pas bipartite et un autre pas vers l'idée de complexité de calcul . Pour plus d'informations, voir [2] .
Théorie et applications des fonctions de trappe
- Yao, AC (1982). « Théorie et application des fonctions de trappe ». 23e Symposium annuel sur les fondements de l'informatique (SFCS 1982) . p. 80-91. doi : 10.1109/SFCS.1982.45 .
Description : Cet article crée un cadre théorique pour les fonctions de trappe et décrit certaines de leurs applications, comme en cryptographie . A noter que le concept de fonctions de trappe a été introduit aux "Nouvelles directions de la cryptographie" six ans plus tôt (Voir section V "Interrelations de problèmes et trappes.").
Complexité informatique
Description : Introduction à la théorie de la complexité computationnelle , le livre explique la caractérisation par son auteur de P-SPACE et d'autres résultats.
Preuves interactives et dureté des cliques approchées
- Feige, U. ; Goldwasser, S. ; Lovász, L. ; Safra, S. ; Szegedy, M. (1996). « Les preuves interactives et la dureté des cliques approchantes » . Journal de l'ACM . 43 (2) : 268-292. doi : 10.1145/226643.226652 .
Vérification probabiliste des preuves : une nouvelle caractérisation de NP
- Arora, S. ; Safra, S. (1998). « Vérification probabiliste des preuves : une nouvelle caractérisation de NP ». Journal de l'ACM . 45 : 70-122. doi : 10.1145/273865.273901 . S2CID 751563 .
Vérification de la preuve et la dureté des problèmes d'approximation
- Arora, S. ; Lund, C. ; Motwani, R. ; Soudan, M. ; Szegedy, M. (1998). « Vérification de preuves et la dureté des problèmes d'approximation ». Journal de l'ACM . 45 (3) : 501-555. CiteSeerX 10.1.1.145.4652 . doi : 10.1145/278298.278306 . S2CID 8561542 .
Description : Ces trois articles ont établi le fait surprenant que certains problèmes en NP restent difficiles même lorsque seule une solution approximative est requise. Voir le théorème PCP .
La difficulté de calcul intrinsèque des fonctions
- Cobham, Alain (1964). « La difficulté intrinsèque de calcul des fonctions » (PDF) . Actes du Congrès international de 1964 pour la logique, la méthodologie et la philosophie des sciences : 24-30.
Description : Première définition de la classe de complexité P. L'un des articles fondateurs de la théorie de la complexité.
Algorithmes
"Un programme machine pour la preuve de théorèmes"
- Davis, M. ; Logemann, G. ; Loveland, D. (1962). « Un programme machine pour la preuve de théorèmes » (PDF) . Communications de l'ACM . 5 (7) : 394-397. doi : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 . S2CID 15866917 .
Description : L' algorithme DPLL . L'algorithme de base pour SAT et d'autres problèmes NP-Complet .
"Une logique orientée machine basée sur le principe de résolution"
- Robinson, JA (1965). « Une logique orientée machine basée sur le principe de résolution ». Journal de l'ACM . 12 : 23-41. doi : 10.1145/321250.321253 . S2CID 14389185 .
Description : Première description de la résolution et de l' unification utilisées dans la démonstration automatique de théorèmes ; utilisé en Prolog et en programmation logique .
"Le problème du voyageur de commerce et des arbres couvrants minimum"
- Tenu, M. ; Karp, RM (1970). « Le problème du voyageur-vendeur et les arbres couvrants minimum ». Recherche opérationnelle . 18 (6) : 1138-1162. doi : 10.1287/opre.18.6.1138 .
Description : L'utilisation d'un algorithme pour l' arbre couvrant minimum comme algorithme d'approximation pour le problème du voyageur de commerce NP-Complet . Les algorithmes d'approximation sont devenus une méthode courante pour faire face aux problèmes NP-Complet.
"Un algorithme polynomial en programmation linéaire"
- LG Khachiyan
- Mathématiques soviétiques - Doklady , vol. 20, p. 191-194, 1979
Description : Pendant longtemps, il n'y avait pas d'algorithme de temps polynomial prouvable pour le problème de programmation linéaire . Khachiyan a été le premier à fournir un algorithme polynomial (et pas seulement assez rapide la plupart du temps comme les algorithmes précédents). Plus tard, Narendra Karmarkar a présenté un algorithme plus rapide à : Narendra Karmarkar, "A new polynomial time algorithm for linear programming", Combinatorica , vol 4, no. 4, p. 373-395, 1984.
"Algorithme probabiliste pour tester la primalité"
- Rabin, M. (1980). "Algorithme probabiliste pour tester la primalité" . Journal de la théorie des nombres . 12 (1) : 128-138. doi : 10.1016/0022-314X(80)90084-0 .
Description : L'article présente le test de primalité de Miller-Rabin et décrit le programme d' algorithmes randomisés .
"Optimisation par recuit simulé"
- Kirkpatrick, S. ; Gelatt, CD ; Vecchi, député (1983). "Optimisation par recuit simulé". Sciences . 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 .
Description : Cet article décrit le recuit simulé , qui est maintenant une heuristique très courante pour les problèmes NP-Complet .
L'art de la programmation informatique
Description : Cette monographie comprend quatre volumes couvrant les algorithmes populaires. Les algorithmes sont écrits en anglais et en assembleur MIX (ou en assembleur MMIX dans les fascicules les plus récents). Cela rend les algorithmes à la fois compréhensibles et précis. Cependant, l'utilisation d'un langage de programmation de bas niveau frustre certains programmeurs plus familiers avec modernes de programmation structurés langues .
Algorithmes + Structures de données = Programmes
- Niklaus Wirth
- Prentice Hall, 1976, ISBN 0-13-022418-9
Description : Un premier livre influent sur les algorithmes et les structures de données, avec des implémentations en Pascal.
La conception et l'analyse d'algorithmes informatiques
- Alfred V. Aho , John E. Hopcroft et Jeffrey D. Ullman
- Addison-Wesley, 1974, ISBN 0-201-00029-6
Description : L'un des textes standard sur les algorithmes pour la période d'environ 1975-1985.
Comment le résoudre par ordinateur
- Dromey, RG (1982). Comment le résoudre par ordinateur . Prentice-Hall International. ISBN 978-0-13-434001-2.
Description : explique le pourquoi des algorithmes et des structures de données. Explique le processus créatif , la ligne de raisonnement , les facteurs de conception derrière les solutions innovantes.
Algorithmes
- Robert Sedgewick
- Addison-Wesley, 1983, ISBN 0-201-06672-6
Description : Un texte très populaire sur les algorithmes à la fin des années 1980. Il était plus accessible et lisible (mais plus élémentaire) que Aho, Hopcroft et Ullman. Il existe des éditions plus récentes.
Introduction aux algorithmes
- Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest et Clifford Stein
- 3e édition, MIT Press, 2009, ISBN 978-0-262-03384-8 .
Description : Ce manuel est devenu si populaire qu'il est presque la norme de facto pour l'enseignement des algorithmes de base. La 1ère édition (avec les trois premiers auteurs) a été publiée en 1990, la 2ème édition en 2001 et la 3ème en 2009.
Théorie algorithmique de l'information
« Sur les tables de nombres aléatoires »
- Kolmogorov, Andreï N. (1963). « Sur les tables de nombres aléatoires ». Sankhya Ser. A . 25 : 369-375. MR 0178484 .
- Kolmogorov, Andreï N. (1963). "Sur les tableaux de nombres aléatoires" . Informatique théorique . 207 (2) : 387-395. doi : 10.1016/S0304-3975(98)00075-9 . MR 1643414 .
Description : Proposition d'une approche computationnelle et combinatoire des probabilités.
"Une théorie formelle de l'inférence inductive"
- Ray Solomonoff
- Information et contrôle , vol. 7, p. 1-22 et 224-254, 1964
- Copie en ligne : partie I , partie II
Description : Ce fut le début de la théorie algorithmique de l'information et de la complexité de Kolmogorov . Notez que bien que la complexité de Kolmogorov porte le nom d' Andrey Kolmogorov , il a dit que les graines de cette idée sont dues à Ray Solomonoff . Andrey Kolmogorov a beaucoup contribué à ce domaine, mais dans des articles ultérieurs.
"Théorie de l'information algorithmique"
- Chaitin, Gregory (1977). "Théorie de l'information algorithmique" (PDF) . Revue IBM de recherche et développement . 21 (4) : 350-359. CiteSeerX 10.1.1.48.3094 . doi : 10.1147/rd.214.0350 . Archivé de l'original (PDF) le 2009-05-30.
Description : Une introduction à la théorie algorithmique de l'information par l'une des personnes importantes dans le domaine.
Théorie de l'information
"Une théorie mathématique de la communication"
- Shannon, CE (1948). "Une théorie mathématique de la communication" . Journal technique du système Bell . 27 (3) : 379-423, 623-656. doi : 10.1002/j.1538-7305.1948.tb01338.x . hdl : 10338.dmlcz/101429 .
Description : Cet article a créé le domaine de la théorie de l' information .
"Codes de détection et de correction d'erreurs"
- Hamming, Richard (1950). "Codes de détection et de correction d'erreurs" . Journal technique du système Bell . 29 (2) : 147-160. doi : 10.1002/j.1538-7305.1950.tb00463.x . hdl : 10945/46756 .
Description : dans cet article, Hamming a introduit l'idée de code correcteur d' erreurs . Il a créé le code de Hamming et la distance de Hamming et développé des méthodes pour les preuves d'optimalité de code.
"Une méthode pour la construction de codes de redondance minimum"
- Huffman, D. (1952). « Une méthode pour la construction de codes de redondance minimale » (PDF) . Actes de l'IRE . 40 (9) : 1098–1101. doi : 10.1109/JRPROC.1952.273898 .
Description : Le codage Huffman .
"Un algorithme universel pour la compression de données séquentielles"
- Ziv, J. ; Lempel, A. (1977). "Un algorithme universel pour la compression séquentielle des données" . Transactions IEEE sur la théorie de l'information . 23 (3) : 337-343. CiteSeerX 10.1.1.118.8921 . doi : 10.1109/TIT.1977.1055714 . hdl : 10338.dmlcz/142947 . Archivé de l'original le 2004-12-04.
Description : L' algorithme de compression LZ77 .
Éléments de théorie de l'information
- T. Couvercle ; J. Thomas (1991). Éléments de théorie de l'information . p. 38-42 . ISBN 978-0-471-06259-2.
Description : Une introduction populaire à la théorie de l'information.
Vérification formelle
Attribuer un sens aux programmes
- Floyd, Robert (1967). « Attribuer un sens aux programmes ». Aspects mathématiques de l'informatique (PDF) . Actes de colloques en mathématiques appliquées. 19 . p. 19-32. doi : 10.1090/psapm/019/0235771 . ISBN 9780821813195.
Description : L'article de référence de Robert Floyd, Assigning Meanings to Programs, présente la méthode des assertions inductives et décrit comment un programme annoté avec des assertions de premier ordre peut être montré pour satisfaire une spécification de pré- et post-condition - l'article introduit également les concepts d'invariance de boucle. et conditions de vérification.
Une base axiomatique pour la programmation informatique
- Hoare, RCA (octobre 1969). "Une base axiomatique pour la programmation informatique" (PDF) . Communications de l'ACM . 12 (10) : 576-580. doi : 10.1145/363235.363259 . S2CID 207726175 . Archivé de l'original (PDF) le 04/03/2016.
Description : L'article de Tony Hoare An Axiomatic Basis for Computer Programming décrit un ensemble de règles d'inférence (c'est-à-dire de preuve formelle) pour des fragments d'un langage de programmation de type Algol décrit en termes de (ce que l'on appelle maintenant) Hoare-triples.
Commandes gardées, non-détermination et dérivation formelle des programmes
- Dijkstra, EW (1975). "Commandes gardées, non-détermination et dérivation formelle de programmes" . Communications de l'ACM . 18 (8) : 453-457. doi : 10.1145/360933.360975 . S2CID 1679242 .
Description : L'article d'Edsger Dijkstra intitulé Guarded Commands, Nondeterminacy and Formal Derivation of Programs (développé par son manuel de niveau universitaire de 1976 A Discipline of Programming) propose qu'au lieu de vérifier formellement un programme après qu'il a été écrit (c'est-à-dire leurs preuves formelles doivent être développées main dans la main (en utilisant des transformateurs de prédicats pour affiner progressivement les préconditions les plus faibles), une méthode connue sous le nom de raffinement (ou dérivation) de programme (ou formel), ou parfois "correction par construction".
Prouver des affirmations sur les programmes parallèles
- Edward A. Ashcroft
- J. Informatique. Syst. Sci. 10(1) : 110-135 (1975) doi : 10.1016/s0022-0000(75)80018-3
Description : L'article qui a introduit les preuves d'invariance des programmes concurrents.
Une technique de preuve axiomatique pour les programmes parallèles I
- Susan S. Owicki , David Gries
- Acta Inform. 6 : 319-340 (1976)
Description : Dans cet article, avec le même article des auteurs "Vérification des propriétés des programmes parallèles : une approche axiomatique. Commun. ACM 19(5) : 279-285 (1976)", l'approche axiomatique de la vérification des programmes parallèles a été présentée.
Une discipline de programmation
- Edsger W. Dijkstra
- 1976
Description : Le manuel classique d'Edsger Dijkstra A Discipline of Programming étend son article précédent Guarded Commands, Nondeterminacy and Formal Derivation of Programs et établit fermement le principe de dérivation formelle des programmes (et de leurs preuves) à partir de leur spécification.
Sémantique dénotationnelle
- Joe Stoy
- 1977
Description : Denotational Semantics de Joe Stoy est le premier ouvrage (niveau postuniversitaire) exposé sur l'approche mathématique (ou fonctionnelle) de la sémantique formelle des langages de programmation (contrairement aux approches opérationnelle et algébrique).
La logique temporelle des programmes
- Pnueli, A. (1977). "La logique temporelle des programmes". 18e Symposium annuel sur les fondements de l'informatique (SFCS 1977) . IEEE. p. 46-57. doi : 10.1109/SFCS.1977.32 . S2CID 117103037 .
Description : L'utilisation de la logique temporelle a été suggérée comme méthode de vérification formelle.
Caractérisation des propriétés de correction des programmes parallèles à l'aide de points fixes (1980)
- E. Allen Emerson , Edmund M. Clarke
- En Proc. 7e Colloque international sur les langages et la programmation des automates, pages 169-181, 1980
Description : La vérification de modèle a été introduite en tant que procédure pour vérifier l'exactitude des programmes concurrents.
Communiquer des processus séquentiels (1978)
- VOITURE Hoare
- 1978
Description : L'article (original) de Tony Hoare sur les processus séquentiels communicants (CSP) introduit l'idée de processus concurrents (c'est-à-dire de programmes) qui ne partagent pas de variables mais coopèrent uniquement en échangeant des messages synchrones.
Un calcul des systèmes de communication
- Robin Milner
- 1980
Description : L'article A Calculus of Communicating Systems (CCS) de Robin Milner décrit une algèbre de processus permettant de raisonner formellement sur des systèmes de processus concurrents, ce qui n'était pas possible pour les modèles antérieurs de concurrence (sémaphores, sections critiques, CSP d'origine).
Développement logiciel : une approche rigoureuse
- Cliff Jones
- 1980
Description : Le manuel de Cliff Jones Software Development: A Rigorous Approach est la première exposition complète de la méthode de développement de Vienne (VDM), qui a évolué (principalement) au laboratoire de recherche d'IBM à Vienne au cours de la décennie précédente et qui combine l'idée de programme le raffinement selon Dijkstra avec celui du raffinement des données (ou réification) par lequel les types de données abstraits définis algébriquement sont formellement transformés en représentations progressivement plus "concrètes".
La science de la programmation
- David Gries
- 1981
Description : Le manuel de David Gries, The Science of Programming, décrit la méthode de précondition la plus faible de Dijkstra pour la dérivation de programmes formels, sauf d'une manière beaucoup plus accessible que la précédente A Discipline of Programming de Dijkstra .
Il montre comment construire des programmes qui fonctionnent correctement (sans bogues, autres que des fautes de frappe). Pour ce faire, il montre comment utiliser des expressions de prédicat préconditionnelles et postconditionnelles et des techniques de preuve de programme pour guider la création de programmes.
Les exemples du livre sont tous à petite échelle et clairement académiques (par opposition au monde réel). Ils mettent l'accent sur les algorithmes de base, tels que le tri et la fusion, et la manipulation de chaînes. Les sous-routines (fonctions) sont incluses, mais les environnements de programmation orientés objet et fonctionnels ne sont pas traités.
Communiquer des processus séquentiels (1985)
- VOITURE Hoare
- 1985
Description : Le manuel Communicating Sequential Processes (CSP) de Tony Hoare (actuellement la troisième référence informatique la plus citée de tous les temps) présente un modèle CSP mis à jour dans lequel les processus de coopération n'ont même pas de variables de programme et qui, comme CCS, permet aux systèmes de processus de raisonner formellement.
Logique linéaire (1987)
- Girard, J.-Y (1987). "Logique linéaire" (PDF) . Informatique théorique . 50 (1) : 1-102. doi : 10.1016/0304-3975(87)90045-4 . Archivé de l'original (PDF) le 2006-11-29.
Description : La logique linéaire de Girard a été une percée dans la conception de systèmes de typage pour le calcul séquentiel et simultané, en particulier pour les systèmes de typage soucieux des ressources.
Un calcul des processus mobiles (1989)
Description : Cet article présente le Pi-Calculus , une généralisation du CCS qui permet la mobilité des processus. Le calcul est extrêmement simple et est devenu le paradigme dominant dans l'étude théorique des langages de programmation, des systèmes de typage et des logiques de programme.
La notation Z : un manuel de référence
- Spivey, JM (1992). La notation Z : Un manuel de référence (2e éd.). Prentice Hall International. ISBN 978-0-13-978529-0. Archivé de l'original le 2016-06-20 . Récupéré le 2009-08-24 .
Description : Le manuel classique de Mike Spivey, The Z Notation : A Reference Manual, résume la notation formelle du langage de spécification Z , qui, bien que créée par Jean-Raymond Abrial, a évolué (principalement) à l'Université d'Oxford au cours de la décennie précédente.
Communication et concurrence
- Robin Milner
- Prentice-Hall International, 1989
Description : Le manuel Communication and Concurrency de Robin Milner est une exposition plus accessible, bien que toujours techniquement avancée, de ses travaux antérieurs sur le CCS.
une théorie pratique de la programmation
- Eric Hehner
- Springer, 1993, édition actuelle en ligne ici
Description : la version mise à jour de la programmation prédicative . La base de l' UTP de CAR Hoare . Les méthodes formelles les plus simples et les plus complètes.
Les références
- Groupe d'intérêt spécial de l'ACM sur les algorithmes et la théorie du calcul (2011). "Prix: Prix Gödel" . Archivé de l'original le 22 avril 2018 . Récupéré le 8 octobre 2011 .