# Liste de publications importantes en informatique théorique

Voici une liste de publications importantes en informatique théorique, organisés par domaine.
Quelques raisons pour lesquelles une publication peut être considérée comme importante:
* Sujet créateur – Une publication qui a créé un nouveau sujet
* Découverte – Une publication qui a changé de manière significative 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é
### Decidability of second order theories and automata on infinite trees

* Michael O. Rabin
* Transactions of the American Mathematical Society, vol. 141, p. 1–35, 1969
Description : ce document présente l'automate d'arbres, une extension de l'automate. l'automate d'arbres a eu de nombreuses applications lors de vérification formelle.

### On computable numbers, with an application to the Entscheidungsproblem

* Alan Turing
* London Mathematical Society, Série 2, vol. 42, p. 230–265, 1937, DOI 10.1112/plms/s2-42.1.230.
* DOI 10.1112/plms/s2-43.6.544.
* HTML version, PDF version
Description : Cet article fixe les limites de l'informatique. Il a défini la machine de Turing, un modèle pour tous calculs. D'autre part, il a prouvé l'indécidabilité du problème de l'arrêt et de l'Entscheidungsproblem et a ainsi trouvé les limites possible du calcul.

## Automates et langages formels
### Finite automata and their decision problems

* Michael O. Rabin et Dana S. Scott
* IBM Journal of Research and Development, vol. 3, p. 114–125, 1959
Description : le traitement mathématique des automates, la preuve de propriétés de base, et la définition d'automate fini non déterministe.

### On certain formal properties of grammars

* N. Chomsky, « On certain formal properties of grammars », Information and Control, vol. 2, n$^o$ 2,‎ 1959, p. 137–167 (DOI 10.1016/S0019-9958(59)90362-6)
Description : Cet article introduit ce qui est maintenant connu comme la hiérarchie de Chomsky, une hiérarchie des classes de grammaires formelles qui génèrent des langages formels.

### Introduction to Automata Theory, Languages, and Computation

* John E. Hopcroft, Jeffrey D. Ullman, et Rajeev Motwani
* Addison-Wesley, 2001
Description : Un manuel populaire.

## Théorie de la complexité
### Computational Complexity de Arora & Barak et Computational Complexity de Goldreich's (Cambridge)

* Sanjeev Arora et Boaz Barak, Computational Complexity: A Modern Approach, Cambridge University Press, 2009, 579 pages
* Oded Goldreich, Computational Complexity: A Conceptual Perspective, Cambridge University Press, 2008, 606 pages
« Une tentative définie avec Arora et Barak pour inclure du matériel à 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 « applaudit tout... les auteurs pour leurs contributions exceptionnelles. »

### A machine-independent theory of the complexity of recursive functions

* Manuel Blum, « A Machine-Independent Theory of the Complexity of Recursive Functions », Journal of the ACM, vol. 14, n$^o$ 2,‎ 1967, p. 322–336 (DOI 10.1145/321386.321395, lire en ligne)
Description : Les axiomes de Blum.

### Algebraic methods for interactive proof systems

* C. Lund, L. Fortnow, H. Karloff et N. Nisan, « Algebraic methods for interactive proof systems », Journal of the ACM, vol. 39, n$^o$ 4,‎ 1992, p. 859–868 (DOI 10.1145/146585.146605)
Description : Ce document a montré que PH est contenu dans IP.

### The complexity of theorem proving procedures

* Stephen A. Cook, « The Complexity of Theorem-Proving Procedures », Proceedings of the 3rd Annual ACM Symposium on Theory of Computing,‎ 1971, p. 151–158 (DOI 10.1145/800157.805047, lire en ligne)
Description : Cet article introduit le concept du problème NP-complet et a prouvé que problème SAT est NP-complet. Notez que des idées similaires ont été développés indépendamment un peu plus tard par Leonid Levin.

### Computers and Intractability: A Guide to the Theory of NP-Completeness

* (en) Michael R. Garey et David S. Johnson, Computers and intractability : a guide to the theory of NP-completeness, New York, Freeman, 1979, 338 p. (ISBN 0-7167-1045-5)
Description : L'intérêt principal de ce livre est dû à sa longue liste de plus de 300 problèmes NP-complets. Cette liste est devenue une référence et une définition commune.

### Degree of difficulty of computing a function and a partial ordering of recursive sets

* Michael O. Rabin, « Degree of difficulty of computing a function and a partial ordering of recursive sets », Technical Report No. 2, Jerusalem, Hebrew University,‎ 1960 (lire en ligne)
Description : Ce rapport technique a été la première publication parlant de ce qui a plus tard été renommé la théorie de la complexité.

### How good is the simplex method?

* Victor Klee et George J. Minty
* Victor Klee et George J. Minty, « How good is the simplex algorithm? », dans Shisha Oved, 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, 1972, 159–175 p. (MR 332165)
Description : Construction du « cube de Klee–Minty » dans la dimension D, dont 2$^D$ coins sont étudiés par l'algorithme du simplexe de Dantzig pour l'optimisation linéaire.

### How to construct random functions

* O. Goldreich, S. Goldwasser et S. Micali, « How to construct random functions », Journal of the ACM, vol. 33, n$^o$ 4,‎ 1986, p. 792–807 (DOI 10.1145/6490.6503, lire en ligne)
Description : Ce document montre que l'existence d'une fonction à sens unique conduit à l'aléatoire de calcul.

### IP = PSPACE

* A. Shamir, « IP = PSPACE », Journal of the ACM, vol. 39, n$^o$ 4,‎ 1992, p. 869–877 (DOI 10.1145/146585.146609)
Description : IP est une classe de complexité dont la caractérisation (basé sur les systèmes de preuve interactives) est tout à fait différente des classes de calcul. Dans cet article, Shamir a étendu la technique de l'article précédent de Lund, et al., Pour montrer que PSPACE est contenue dans IP, et donc IP = PSPACE, pour faire en sorte que chaque problème dans une classe de complexité est résoluble dans l'autre.

### Reducibility among combinatorial problems

* R. M. Karp
* In R. E. Miller et J. W. Thatcher, editors, Complexity of Computer Computations, Plenum Press, New York, NY, 1972, p. 85–103
Description : Ce document a montré que 21 problèmes différents sont NP-complet et a montré l'importance de ce concept.

### The Knowledge Complexity of Interactive Proof Systems

* S. Goldwasser, S. Micali et C. Rackoff, « The Knowledge Complexity of Interactive Proof Systems », SIAM J. Comput., vol. 18, n$^o$ 1,‎ 1989, p. 186–208 (DOI 10.1137/0218012, lire en ligne)
Description : Le présent document introduit le concept de connaissance nulle.

### A letter from Gödel to 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'efficacité de théorème universel.

### On the computational complexity of algorithms

* Juris Hartmanis et Richard Stearns, « On the computational complexity of algorithms », Transactions of the American Mathematical Society, n$^o$ 117,‎ 1965, p. 285–306
Description : Ce document a donné à la complexité de calcul son nom et sa semence.

### Theory and applications of trapdoor functions

* A. C. Yao, 23rd Annual Symposium on Foundations of Computer Science (SFCS 1982), 1982, 80–91 p. (DOI 10.1109/SFCS.1982.45), « Theory and application of trapdoor functions »
Description : Cet article a créé un cadre théorique pour les trapdoor functions et décrit certaines de leurs applications, comme en cryptographie. Notez que le concept de trapdoor functions a été amené à de « Nouvelles directions en cryptographie » six ans plus tôt (voir la section V « Problem Interrelationships and Trap Doors. »).

### Computational Complexity

* C.H. Papadimitriou
* Addison-Wesley, 1994, (ISBN 0-201-53082-1)
Description : Une introduction à la théorie de la complexité des calculs, le livre explique la caractérisation du P-SPACE et d'autres résultats.

### Interactive proofs and the hardness of approximating cliques

* U. Feige, S. Goldwasser, L. Lovász, S. Safra et M. Szegedy, « Interactive proofs and the hardness of approximating cliques », Journal of the ACM, vol. 43, n$^o$ 2,‎ 1996, p. 268–292 (DOI 10.1145/226643.226652)

### Probabilistic checking of proofs: a new characterization of NP

* S. Arora et S. Safra, « Probabilistic checking of proofs: A new characterization of NP », Journal of the ACM, vol. 45,‎ 1998, p. 70–122 (DOI 10.1145/273865.273901)

### Proof verification and the hardness of approximation problems

* S. Arora, C. Lund, R. Motwani, M. Sudan et M. Szegedy, « Proof verification and the hardness of approximation problems », Journal of the ACM, vol. 45, n$^o$ 3,‎ 1998, p. 501–555 (DOI 10.1145/278298.278306)
Description : Ces trois documents établi le fait surprenant que certains problèmes NP restent difficiles, même lorsque seule une solution approximative est nécessaire. Voir le théorème PCP.

## Algorithmes
### « A machine program for theorem proving »

* M. Davis, G. Logemann et D. Loveland, « A machine program for theorem-proving », Communications of the ACM, vol. 5, n$^o$ 7,‎ 1962, p. 394–397 (DOI 10.1145/368273.368557, lire en ligne)
Description : L'algorithme DPLL. L'algorithme de base pour les SAT et d'autres problèmes NP-complets.

### « A machine-oriented logic based on the resolution principle »

* J. A. Robinson, « A Machine-Oriented Logic Based on the Resolution Principle », Journal of the ACM, vol. 12,‎ 1965, p. 23–41 (DOI 10.1145/321250.321253)Journal of the ACM 12: 23–41.
Description : Première description de la résolution et de l'unification utilisée dans la démonstration automatique de théorèmes; utilisé dans Prolog.

### « The traveling-salesman problem and minimum spanning trees »

* M. Held et R. M. Karp, « The Traveling-Salesman Problem and Minimum Spanning Trees », Operations Research, vol. 18, n$^o$ 6,‎ 1970, p. 1138–1162 (DOI 10.1287/opre.18.6.1138)
Description : L'utilisation d'un algorithme d'arbre couvrant de poids minimal comme un algorithme d'approximation pour le problème NP-complet du voyageur de commerce. Les algorithmes d'approximation sont devenus une méthode commune pour faire face aux problèmes NP-complets.

### « Probabilistic algorithm for testing primality »

* M. Rabin, « Probabilistic algorithm for testing primality », Journal of Number Theory, vol. 12, n$^o$ 1,‎ 1980, p. 128–138 (DOI 10.1016/0022-314X(80)90084-0)
Description : Le document présente le test de primalité deMiller-Rabin et décrit le programme d'algorithmes probabilistes.

### « Optimization by simulated annealing »

* S. Kirkpatrick, C. D. Gelatt et M. P. Vecchi, « Optimization by Simulated Annealing », Science, vol. 220, n$^o$ 4598,‎ 1983, p. 671–680 (PMID 17813860, DOI 10.1126/science.220.4598.671)
Description : Cet article décrit le recuit simulé qui est maintenant une heuristique très commune pour les problèmes NP-complets.

### The Art of Computer Programming

* Donald Knuth
Description : Cette monographie a trois livres d'algorithmes populaires et un certain nombre de fascicules. Les algorithmes sont écrits en anglais et en langage MIX. Cela rend les algorithmes à la fois compréhensible et précis. Cependant, l'utilisation d'un langage de programmation de bas niveau frustre certains programmeurs plus familiers avec les langages de programmation structurés modernes.

### Algorithms + Data Structures = Programs

* Niklaus Wirth
* Prentice Hall, 1976, (ISBN 0-13-022418-9)
Description : Un livre influent sur les algorithmes et des structures de données.

### The Design and Analysis of Computer Algorithms

* Alfred V. Aho, John E. Hopcroft, et Jeffrey D. Ullman
* Addison-Wesley, 1974, (ISBN 0-201-00029-6)
Description : L'un des textes de référence portant sur les algorithmes durant la période 1975-1985.

### How to Solve It By Computer

* R. G. Dromey, How to Solve it by Computer, Prentice-Hall International, 1982, 442 p. (ISBN 978-0-13-434001-2)
Description : Explication du Pourquoi des algorithmes et des structures de données. Explication du Processus de Création, de la Ligne de Raisonnement, et des Facteurs de Conception derrière des solutions innovantes.

### Algorithms

* Robert Sedgewick
* Addison-Wesley, 1983, (ISBN 0-201-06672-6)
Description : Un texte très populaire sur des algorithmes à la fin des années 1980.

### Introduction to Algorithms

* 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 l'enseignement des algorithmes basiques. La 1re édition a été publié en 1990, la 2e édition en 2001, et le 3e en 2009.

## Théorie algorithmique de l'information
### « On Tables of Random Numbers »

* Andrei N. Kolmogorov, « On Tables of Random Numbers », Sankhyā Ser. A., vol. 25,‎ 1963, p. 369–375 (MR 178484).
* Andrei N. Kolmogorov, « On Tables of Random Numbers », Theoretical Computer Science, vol. 207, n$^o$ 2,‎ 1963, p. 387–395 (DOI 10.1016/S0304-3975(98)00075-9, MR 1643414)
Description : Projet d'une approche de calcul de la probabilité.

### « A formal theory of inductive inference »

* Ray Solomonoff
* Information and Control, vol. 7, p. 1–22 and 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 si la complexité de Kolmogorov est nommé d'après Andrey Kolmogorov, cette idée revient à Ray Solomonoff. Andrey Kolmogorov a beaucoup contribué dans ce domaine, mais avec des articles ultérieurs.

### « Algorithmic information theory »

* Gregory Chaitin, « Algorithmic information theory », IBM Journal of Research and Development, IBM, vol. 21, n$^o$ 4,‎ 1977, p. 350–359 (DOI 10.1147/rd.214.0350, lire en ligne)
Description : Une introduction à la théorie algorithmique de l'information par l'une des personnes importantes de ce domaine.

## Théorie de l'information
### « A mathematical theory of communication »

* C.E. Shannon, « A mathematical theory of communication », Bell System Technical Journal, vol. 27,‎ 1948, p. 379–423, 623–656 (lire en ligne)
Description : Ce document a créé le domaine de la théorie de l'information.

### « Error detecting and error correcting codes »

* Richard Hamming, « Error detecting and error correcting codes », Bell System Technical Journal, vol. 29,‎ 1950, p. 147–160 (DOI 10.1002/j.1538-7305.1950.tb00463.x, lire en ligne)
Description : Dans cet article, Hamming a introduit l'idée d'un code de correction d’erreur. Il a créé le code de Hamming et la distance de Hamming.

### « A method for the construction of minimum redundancy codes »

* D. Huffman, « A Method for the Construction of Minimum-Redundancy Codes », Proceedings of the IRE, vol. 40, n$^o$ 9,‎ 1952, p. 1098–1101 (DOI 10.1109/JRPROC.1952.273898, lire en ligne)
Description : Le codage de Huffman.

### « A universal algorithm for sequential data compression »

* J. Ziv et A. Lempel, « A universal algorithm for sequential data compression », IEEE Transactions on Information Theory, vol. 23, n$^o$ 3,‎ 1977, p. 337–343 (DOI 10.1109/TIT.1977.1055714, lire en ligne [archive du 4 décembre 2003])
Description : L'algorithme de compression LZ77.

### Elements of Information Theory

* Thomas M. Cover, Joy A. Thomas, Elements of Information Theory, Wiley-Interscience, 2006 (ISBN 978-0-471-24195-9) [détail des éditions]
Description : Une introduction populaire à la théorie de l'information.

## Vérification formelle
### An Axiomatic Basis for Computer Programming

* C. A. R. Hoare, « An axiomatic basis for computer programming », Communications of the ACM, vol. 12, n$^o$ 10,‎ octobre 1969, p. 576–580 (DOI 10.1145/363235.363259, lire en ligne)
Description : L'article de Tony Hoare décrit un ensemble de règles d'inférence (à savoir la preuve formelle) pour un langage de programmation comme Algol.

### Guarded Commands, Nondeterminacy and Formal Derivation of Programs

* E. W. Dijkstra, « Guarded commands, nondeterminacy and formal derivation of programs », Communications of the ACM, vol. 18, n$^o$ 8,‎ 1975, p. 453–457 (DOI 10.1145/360933.360975, lire en ligne)
Description : Ce document propose que, au lieu de vérifier formellement un programme après qu'il a été écrit (c.-à-post facto), les programmes et leurs preuves formelles devraient être développées main dans la main, une méthode connue sous le nom raffinement (ou dérivation) de programme.

### Proving Assertions about Parallel Programs

* Edward A. Ashcroft
* J. Comput. Syst. Sci. 10(1): 110-135 (1975)
Description : Cet article a présenté les preuves d'invariance des programmes concurrents.

### An Axiomatic Proof Technique for Parallel Programs I

* Susan S. Owicki, David Gries
* Acta Inf. 6: 319-340 (1976)
Description : Dans ce document, l'approche axiomatique parallèle de vérification de programmes est présenté.

### Denotational Semantics

* Joe Stoy
* 1977
Description : Premier livre portant sur l'approche mathématique (ou fonctionnelle) de la sémantique formelle des langages de programmation (contrairement aux approches opérationnelles et algébriques).

### The Temporal Logic of Programs

* A. Pnueli, 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), IEEE, 1977, 46–57 p. (DOI 10.1109/SFCS.1977.32), « The temporal logic of programs »
Description : L'utilisation de la logique temporelle a été proposée comme méthode de vérification formelle.

### Characterizing correctness properties of parallel programs using fixpoints (1980)

* E. Allen Emerson, Edmund M. Clarke
Description : Le modèle de vérification a été présenté comme une procédure afin de vérifier l'exactitude des programmes concurrents.

### The Science of Programming

* David Gries
* 1981
Description : Ce document montre comment construire des programmes qui fonctionnent correctement (sans bugs, autres que des erreurs de frappe).

### Communicating Sequential Processes (1985)

* C.A.R. Hoare
* 1985
Description : Ce livre est actuellement la troisième référence la plus citée en l'informatique.

### Linear logic (1987)

* J.-Y Girard, « Linear Logic », Theoretical Computer Science, London Mathematical Society, vol. 50, n$^o$ 1,‎ 1987, p. 1–102 (DOI 10.1016/0304-3975(87)90045-4, lire en ligne)
Description : la logique linéaire de Girard était une percée dans la conception de système dactylographique pour le calcul séquentiel et simultané.

### A Calculus of Mobile Processes (1989)

* R. Milner, J. Parrow, D. Walker
* 1989
* Version en ligne: Partie 1 et Partie 2
Description : ce document a introduit le Pi-Calcul, une généralisation du CCS. Le calcul est extrêmement simple et est devenu le paradigme dominant dans l'étude théorique des langages de programmation, les systèmes de frappe et des logiques de programme.

### The Z Notation: A Reference Manual

* J. M. Spivey, The Z Notation : A Reference Manual, Prentice Hall International, 1992, 2e éd., 158 p. (ISBN 0-13-978529-9, lire en ligne)
Description : Un manuel de référence résumant la notation Z formelle.

### a Practical Theory of Programming

* Eric Hehner
* Springer, 1993, édition en ligne ici
Description : la version mise à jour de la programmation prédicative. La base de L'UTP de C.A.R. Hoare. Les méthodes formelles les plus simples et les plus complètes.