Liste over viktige publikasjoner innen teoretisk informatikk

Her er en liste over  viktige publikasjoner  innen  teoretisk informatikk , organisert etter felt.

Noen grunner til at et innlegg kan betraktes som viktig:

Beregnbarhet

Avgjørbarhet av andre ordens teorier og automater på uendelige trær

Beskrivelse: dette dokumentet presenterer treautomaten , en utvidelse av automaten . treautomaten har hatt mange applikasjoner i   formell verifisering .

På beregningsbare tall, med en applikasjon til Entscheidungsproblemet

Beskrivelse: Denne artikkelen setter grensene for databehandling. Han definerte Turing-maskinen , en modell for alle beregninger. På den annen side beviste han at det var ubesluttsomt med dommen og Entscheidungsproblemet, og fant dermed mulige grenser for beregningen. 

Automata og formelle språk

Endelige automater og deres beslutningsproblemer

Beskrivelse: Den matematiske behandlingen av automatene , beviset på grunnleggende egenskaper og definisjonen av ikke-deterministisk endelig automat .

På visse formelle egenskaper ved grammatikk

Beskrivelse: Denne artikkelen introduserer det som nå kalles Chomsky- hierarkiet , et hierarki av formelle grammatikklasser som genererer formelle språk .

Introduksjon til automatteori, språk og beregning

Beskrivelse: En populær lærebok.

Kompleksitetsteori

Computational Complexity  av Arora & Barak og Computational Complexity av Goldreich's (Cambridge)


"Et bestemt forsøk med [Arora og Barak] å ta med oppdatert materiale, mens Goldreich fokuserer mer på å utvikle et kontekstuelt og historisk grunnlag for hvert konsept som presenteres," og han "applauderer alle ... forfattere for deres eksepsjonelle bidrag. ”

En maskinuavhengig teori om kompleksiteten til rekursive funksjoner

Beskrivelse: Aksiomene til Blum .

Algebraiske metoder for interaktive bevis systemer

Beskrivelse: Dette dokumentet har vist at PH er inneholdt i IP .

Kompleksiteten i teoremet som beviser prosedyrer

Beskrivelse: Denne artikkelen introduserer begrepet  NP-komplett problem  og beviste at SAT-problemet er NP-komplett . Merk at lignende ideer ble utviklet uavhengig litt senere av Leonid Levin .

Datamaskiner og trekkbarhet: En guide til teorien om NP-fullstendighet

Beskrivelse: Hovedinteressen til denne boka skyldes den lange listen over over 300 NP-komplette problemer . Denne listen har blitt en vanlig referanse og definisjon. 

Vanskelighetsgrad med å beregne en funksjon og en delvis rekkefølge av rekursive sett

Beskrivelse: Denne tekniske rapporten var den første publikasjonen som diskuterte hva som senere ble omdøpt til Complexity Theory ? '' 'UNIQ - nowiki-00000006-QINU' ''? 2 ? '"` UNIQ - nowiki-00000007-QINU` "'? ..

Hvor god er simpleksmetoden?

Beskrivelse: Konstruksjon av "Klee-Minty-kuben" i dimensjonen  D , 2 D  hjørner er studert av simpleksalgoritmen til Danzig for lineær optimalisering .

Hvordan konstruere tilfeldige funksjoner

Beskrivelse: Dette dokumentet viser at eksistensen av en enveisfunksjon fører til beregnings tilfeldighet.

IP = PSPACE

Beskrivelse:  IP er en kompleksitetsklasse hvis karakterisering (basert på interaktive proof-systemer ) er ganske forskjellig fra beregningsklasser. I denne artikkelen utvidet Shamir teknikken til forrige artikkel av Lund, et al. , For å vise at PSPACE er inneholdt i IP, og derfor IP = PSPACE, for å sikre at hvert problem i en kompleksitetsklasse er løst i det andre.

Reduserbarhet blant kombinatoriske problemer

Beskrivelse: Dette dokumentet har vist at 21 forskjellige problemer er NP-komplette og har vist viktigheten av dette konseptet.

Kunnskapskompleksiteten til interaktive bevis systemer

Beskrivelse: Dette dokumentet introduserer begrepet null kunnskap .

Et brev fra Gödel til von Neumann

Beskrivelse:  Gödel diskuterer ideen om effektivitet i den universelle setningen.

På beregningskompleksiteten til algoritmer

Beskrivelse: Dette dokumentet ga beregningskompleksitet  navn og frø.

Teori og anvendelser av låsefunksjoner

Beskrivelse: Denne artikkelen har laget et teoretisk rammeverk for trapdoorfunksjoner og beskriver noen av deres applikasjoner, for eksempel i  kryptografi . Vær oppmerksom på at konseptet med dørfunksjoner ble brakt til "Nye veiledninger i kryptografi" for seks år siden (se avsnitt V " Problemforhold og felle dører .").

Computational Complexity

Beskrivelse: En introduksjon til teorien om beregningskompleksitet, forklarer boken karakteriseringen av P-SPACE og andre resultater.

Interaktive bevis og hardheten til omtrentlige klikker

Probabilistisk kontroll av bevis: en ny karakterisering av NP

Bevisverifisering og hardheten til tilnærmingsproblemer

Beskrivelse: Disse tre dokumentene viser det overraskende faktum at noen NP-problemer fortsatt er vanskelige, selv når det bare er behov for en grov løsning. Se  PCP-teoremet .

Algoritmer

"Et maskinprogram for bevisning av teorem"

Beskrivelse: DPLL-algoritmen . Den grunnleggende algoritmen for SAT og andre NP-komplette problemer .

"En maskinorientert logikk basert på oppløsningsprinsippet"

Beskrivelse: Første beskrivelse av oppløsningen og foreningen som brukes i det automatiske beviset på setninger ; brukt i  Prolog .

"Reisende selgerproblem og minimum spennende trær"

Beskrivelse: Bruk av en algoritme med et minimumspennende tre som en tilnærmelsesalgoritme for NP-komplett problem med den reisende selgeren . Tilnærmelsesalgoritmer har blitt en vanlig metode for å håndtere NP-komplette problemer.

"Probabilistisk algoritme for testing av primalitet"

Beskrivelse: Dokumentet presenterer Miller-Rabin primality test og beskriver det sannsynlige algoritmeprogrammet .

"Optimalisering ved simulert annealing"

Beskrivelse: Denne artikkelen beskriver simulert annealing som nå er en veldig vanlig heuristikk for NP-komplette problemer .

Kunsten med dataprogrammering

Beskrivelse: Denne monografien har tre populære algoritmebøker og et antall hefter . Algoritmene er skrevet på engelsk og på MIX- språk . Dette gjør algoritmene både forståelige og presise. Ved å bruke et programmeringsspråk på lavt nivå frustrerer imidlertid noen programmerere som er mer kjent med moderne strukturerte programmeringsspråk .

Algoritmer + datastrukturer = programmer

Beskrivelse: En bok påvirker algoritmer og datastrukturer.

Design og analyse av datalgoritmer

Beskrivelse: En av referansetekstene om algoritmer i perioden 1975-1985.

Hvordan løse det med datamaskin

Beskrivelse: Forklaring av hvorfor  algoritmer og datastrukturer. Forklaring til skapelsesprosessen , argumentasjonslinjen og designfaktorene bak innovative løsninger.

Algoritmer

Beskrivelse: En veldig populær tekst om algoritmer på slutten av 1980-tallet.

Introduksjon til algoritmer

Beskrivelse: Denne håndboken har blitt så populær at den nesten er standarden for undervisning i grunnleggende algoritmer. Den 1 st  utgaven ble utgitt i 1990, to th  utgave i 2001, og tre e i 2009.

Algoritmisk informasjonsteori

"På tabeller med tilfeldige tall"

Beskrivelse: Prosjekt av en sannsynlighetsberegningstilnærming.

"En formell teori om induktiv slutning"

Beskrivelse: Dette var starten på Kolmogorovs algoritmiske teori om informasjon og kompleksitet . Merk at mens Kolmogorov-kompleksitet er oppkalt etter Andrey Kolmogorov , går ideen til Ray Solomonoff . Andrey Kolmogorov bidro mye på dette området, men med påfølgende artikler.

"Algoritmisk informasjonsteori"

Beskrivelse: En introduksjon til algoritmisk informasjonsteori av en av de viktige personene i dette feltet.

Informasjonsteori

"En matematisk teori om kommunikasjon"

Beskrivelse: Dette dokumentet opprettet felt for informasjonsteori .

"Feiloppdaging og feilretting av koder"

Beskrivelse: I denne artikkelen introduserte Hamming ideen om en feilrettingskode . Han opprettet Hamming-koden og Hamming-avstanden .

"En metode for konstruksjon av minimumskrav til redundans"

Beskrivelse:  Huffmans koding .

"En universell algoritme for sekvensiell datakomprimering"

Beskrivelse: LZ77- komprimeringsalgoritmen .

Elementer av informasjonsteori

Beskrivelse: En populær introduksjon til informasjonsteori.

Formell bekreftelse

Et aksiomatisk grunnlag for dataprogrammering

Beskrivelse: Tony Hoares artikkel beskriver et sett av regler for slutning (dvs. formell bevis) for et programmeringsspråk som Algol .

Bevoktet kommando, ubestemmelighet og formell avledning av programmer

Beskrivelse: Dette dokumentet foreslår at programmer og deres formelle bevis skal utvikles hånd i hånd, i stedet for å formelt verifisere et program etter at det er skrevet (dvs. post facto), en metode kjent som navneforbedring (eller avledning) av programmet.

Bevise påstander om parallelle programmer

Beskrivelse: Denne artikkelen presenterte bevisene for uforanderlighet i samtidige programmer.

En aksiomatisk bevisteknikk for parallelle programmer I

Beskrivelse: I dette dokumentet presenteres den parallelle aksiomatiske tilnærmingen til programverifisering.

Denotasjonell semantikk

Beskrivelse: Første bok om den matematiske (eller funksjonelle) tilnærmingen til den formelle semantikken til programmeringsspråk (i motsetning til operasjonelle og algebraiske tilnærminger).

Programmets tidsmessige logikk

Beskrivelse: Bruk av tidslogikk er blitt foreslått som en formell verifiseringsmetode.

Karakteriserer korrekthetsegenskapene til parallelle programmer ved hjelp av fixpoints (1980)

Beskrivelse: Verifiseringsmodellen ble presentert som en prosedyre for å verifisere nøyaktigheten til samtidige programmer.

Vitenskapen om programmering

Beskrivelse: Dette dokumentet viser hvordan du bygger programmer som fungerer som de skal (uten feil, bortsett fra skrivefeil).

Kommunisere sekvensielle prosesser (1985)

Beskrivelse: Denne boken er for tiden den tredje mest siterte referansen innen databehandling.

Lineær logikk (1987)

Beskrivelse: Girards lineære logikk var et gjennombrudd i typesystemdesign for sekvensiell og samtidig beregning .

En beregning av mobile prosesser (1989)

Beskrivelse: dette dokumentet introduserte  Pi-Calculus , en generalisering av CCS. Beregning er ekstremt enkel og har blitt det dominerende paradigmet i den teoretiske studien av programmeringsspråk, typesystemer og programlogikk.

Z-notasjonen: En referansehåndbok

Beskrivelse: En referansehåndbok som oppsummerer den formelle Z-notasjonen .

en praktisk teori om programmering

Beskrivelse: Den oppdaterte versjonen av prediktiv programmering . Basen til CAR Hoares UTP . De enkleste og mest komplette formelle metodene.

Relaterte artikler

Referanser

  1. Daniel Apon, 2010, "Joint Review of Computational Complexity: A Conceptual Perspective av Oded Goldreich ... og Computational Complexity: A Modern Approach av Sanjeev Arora og Boaz Barak ...," ACM SIGACT News, Vol. 41 (4), desember 2010, s.  12-15 , se [1] , åpnet 1. februar 2015.
  2. Shasha, Dennis, "Et intervju med Michael O. Rabin" , Communications of the ACM , Vol. 53 nr. 2, side 37-42, februar 2010.
  3. (in) ACM Special Interest Group on Algorithms and Computation Theory, "  Premieres: Gödel Prize  " ,2011(åpnet 7. september 2016 )