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

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

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

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

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

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

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

Description : Les axiomes de Blum .

Méthodes algébriques pour les systèmes de preuve interactifs

Description : Cet article a montré que PH est contenu dans IP .

La complexité des procédures de preuve de théorème

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

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

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

Description : Cet article a montré que l'existence de fonctions à sens unique conduit à un calcul aléatoire .

IP = PSPACE

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

Description : Cet article a introduit le concept de connaissance zéro .

Une lettre de Gödel à von Neumann

Description : Gödel discute de l'idée d'un prouveur de théorème universel efficace.

Sur la complexité calculatoire des algorithmes

Description : Cet article a donné son nom et son germe à la complexité informatique .

Chemins, arbres et fleurs

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

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

Vérification probabiliste des preuves : une nouvelle caractérisation de NP

Vérification de la preuve et la dureté des problèmes d'approximation

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

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"

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"

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"

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"

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é"

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é"

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

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

Description : L'un des textes standard sur les algorithmes pour la période d'environ 1975-1985.

Comment le résoudre par ordinateur

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

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

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 »

Description : Proposition d'une approche computationnelle et combinatoire des probabilités.

"Une théorie formelle de l'inférence inductive"

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"

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"

Description : Cet article a créé le domaine de la théorie de l' information .

"Codes de détection et de correction d'erreurs"

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"

Description : Le codage Huffman .

"Un algorithme universel pour la compression de données séquentielles"

Description : L' algorithme de compression LZ77 .

Éléments de théorie de l'information

Description : Une introduction populaire à la théorie de l'information.

Vérification formelle

Attribuer un sens aux programmes

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

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

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

Description : L'article qui a introduit les preuves d'invariance des programmes concurrents.

Une technique de preuve axiomatique pour les programmes parallèles I

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

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

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

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)

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)

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

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

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

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)

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)

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

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

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

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 .