De Wikipedia, la enciclopedia libre
  (Redirigido desde On Computable Numbers )
Saltar a navegación Saltar a búsqueda

Esta es una lista de publicaciones importantes en informática teórica , organizadas por campo.

Algunas razones por las que una publicación en particular podría considerarse importante:

  • Creador de tema : una publicación que creó un tema nuevo
  • Breakthrough : una publicación que cambió significativamente el conocimiento científico.
  • Influencia : una publicación que ha influido significativamente en el mundo o ha tenido un impacto masivo en la enseñanza de la informática teórica.

Computabilidad [ editar ]

Computabilidad de Cutland : Introducción a la teoría de funciones recursivas (Cambridge) [ editar ]

  • Cutland, Nigel J. (1980). Computabilidad: Introducción a la teoría de funciones recursivas . Prensa de la Universidad de Cambridge . ISBN 978-0-521-29465-2.

La revisión de este primer texto por Carl Smith de Purdue University (en la Society for Industrial and Applied Mathematics Reviews ), [1] informa que este es un texto con una "combinación apropiada de intuición y rigor ... en la exposición de pruebas" que presenta "los resultados fundamentales de la teoría de la recursividad clásica [RT] ... en un estilo ... accesible a estudiantes universitarios con una formación matemática mínima". Si bien afirma que "sería un excelente texto introductorio para un curso introductorio en [RT] para estudiantes de matemáticas", sugiere que un "instructor debe estar preparado para aumentar sustancialmente el material ..." cuando se usa con estudiantes de ciencias de la computación (dado escasez de material sobre aplicaciones de RT en esta área). [1]

Decidibilidad de las teorías de segundo orden y los autómatas en árboles infinitos [ editar ]

  • Michael O. Rabin
  • Transacciones de la American Mathematical Society , vol. 141, págs. 1-35, 1969

Descripción: El artículo presentaba el árbol autómata , una extensión de los autómatas . El árbol autómata tuvo numerosas aplicaciones para pruebas de corrección de programas .

Autómatas finitos y sus problemas de decisión [ editar ]

  • Michael O. Rabin y Dana S. Scott
  • IBM Journal of Research and Development , vol. 3, págs. 114-125, 1959
  • Versión en línea

Descripción: Tratamiento matemático de autómatas , prueba de propiedades del núcleo y definición de autómata finito no determinista .

Introducción a la teoría, los lenguajes y la computación de los autómatas [ editar ]

Artículo principal: Introducción a la teoría, los lenguajes y la computación de los autómatas
  • John E. Hopcroft , Jeffrey D. Ullman y Rajeev Motwani
  • Addison-Wesley , 2001, ISBN 0-201-02988-X 

Descripción: Un libro de texto popular.

Sobre ciertas propiedades formales de las gramáticas [ editar ]

  • Chomsky, N. (1959). "Sobre ciertas propiedades formales de las gramáticas" . Información y control . 2 (2): 137-167. doi : 10.1016 / S0019-9958 (59) 90362-6 .

Descripción: Este artículo presentó lo que ahora se conoce como la jerarquía de Chomsky , una jerarquía de contención de clases de gramáticas formales que generan lenguajes formales .

Sobre números computables, con una aplicación al Entscheidungsproblem [ editar ]

  • Alan Turing
  • Actas de la London Mathematical Society , Serie 2 , vol. 42, págs. 230-265, 1937, doi : 10.1112 / plms / s2-42.1.230 .
    La errata apareció en el vol. 43, págs. 544-546, 1938, doi : 10.1112 / plms / s2-43.6.544 .
  • Versión HTML , versión PDF

Descripción: Este artículo marca los límites de la informática. Definió la Máquina de Turing , un modelo para todos los cálculos. Por otro lado, demostró la indecidibilidad del problema de la detención y el Entscheidungsproblem y, al hacerlo, encontró los límites del cálculo posible.

Rekursive Funktionen [ editar ]

  • Péter, Rózsa (1951). Funktionen Rekursive . Prensa académica. ISBN 9780125526500.

El primer libro de texto sobre teoría de funciones recursivas . El libro pasó por muchas ediciones y le valió a Péter el Premio Kossuth del gobierno húngaro . [2] Las reseñas de Raphael M. Robinson y Stephen Kleene elogiaron el libro por proporcionar una introducción elemental eficaz para los estudiantes. [3]

Representación de eventos en redes nerviosas y autómatas finitos [ editar ]

  • SC Kleene
  • Memorando de investigación RM-704 del Proyecto Rand de la Fuerza Aérea de EE. UU. , 1951
  • Versión en línea
  • republicado en: Shannon, Claude ; McCarthy, John , eds. (1956). Estudios de autómatas . OCLC 564148 . 

Descripción: este artículo introdujo autómatas finitos , expresiones regulares y lenguajes regulares , y estableció su conexión.

Teoría de la complejidad computacional [ editar ]

Arora y Barak de complejidad computacional y de Goldreich complejidad computacional (ambos de Cambridge) [ editar ]

  • Sanjeev Arora y Boaz Barak, "Computational Complexity: A Modern Approach", Cambridge University Press, 2009, 579 páginas, tapa dura
  • Oded Goldreich, "Computational Complexity: A Conceptual Perspective, Cambridge University Press, 2008, 606 páginas, tapa dura

Además de la estimable prensa que presenta estos textos recientes, Daniel Apon de la Universidad de Arkansas los revisa muy positivamente en SIGACT News de ACM [4], quien los identifica como "libros de texto para un curso de teoría de la complejidad, dirigido a graduados tempranos ... o ... estudiantes universitarios avanzados ... [con] numerosas y únicas fortalezas y muy pocas debilidades ", y afirma que ambos son:

"textos excelentes que cubren a fondo tanto la amplitud como la profundidad de la teoría de la complejidad computacional ... [por] autores ... cada uno [que] son ​​gigantes en la teoría de la computación [donde cada uno será] ... un texto de referencia excepcional para expertos en el campo ... [y que] ... teóricos, investigadores e instructores de cualquier escuela de pensamiento encontrarán útil cualquiera de los dos libros ".

El revisor señala que hay "un intento definitivo en [Arora y Barak] de incluir material muy actualizado, mientras que Goldreich se centra más en desarrollar una base contextual e histórica para cada concepto presentado", y que "aplaude [s ] a todos ... autores por sus destacadas contribuciones ". [4]

Una teoría independiente de la máquina de la complejidad de las funciones recursivas [ editar ]

  • Blum, Manuel (1967). "Una teoría independiente de la máquina de la complejidad de las funciones recursivas" (PDF) . Revista de la ACM . 14 (2): 322–336. doi : 10.1145 / 321386.321395 . S2CID  15710280 .

Descripción: Los axiomas de Blum .

Métodos algebraicos para sistemas de prueba interactivos [ editar ]

  • Lund, C .; Fortnow, L .; Karloff, H .; Nisan, N. (1992). "Métodos algebraicos para sistemas de prueba interactivos". Revista de la ACM . 39 (4): 859–868. CiteSeerX  10.1.1.41.9477 . doi : 10.1145 / 146585.146605 . S2CID  207170996 .

Descripción: Este documento mostró que PH está contenido en IP .

La complejidad de los procedimientos de demostración de teoremas [ editar ]

  • Cook, Stephen A. (1971). "La complejidad de los procedimientos de demostración de teoremas" (PDF) . Actas del 3er Simposio Anual de ACM sobre Teoría de la Computación : 151-158. CiteSeerX  10.1.1.406.395 . doi : 10.1145 / 800157.805047 . S2CID  7573663 .

Descripción: Este artículo introdujo el concepto de NP-Completeness y demostró que el problema de satisfacibilidad booleano (SAT) es NP-Complete . Tenga en cuenta que Leonid Levin desarrolló ideas similares de forma independiente un poco más tarde en "Levin, Universal Search Problems. Problemy Peredachi Informatsii 9 (3): 265-266, 1973".

Computadoras e intratabilidad: una guía para la teoría de NP-Completeness [ editar ]

  • Garey, Michael R .; Johnson, David S. (1979). Computadoras e intratabilidad: una guía para la teoría de NP-Completeness . Nueva York: Freeman. ISBN 978-0-7167-1045-5.

Descripción: La principal importancia de este libro se debe a su extensa lista de más de 300 problemas NP-Complete . Esta lista se convirtió en una referencia y una definición comunes. Aunque el libro se publicó pocos años después de que se definiera el concepto, se encontró una lista tan extensa.

Grado de dificultad para calcular una función y un orden parcial de conjuntos recursivos [ editar ]

  • Rabin, Michael O. (1960). "Grado de dificultad para calcular una función y un ordenamiento parcial de conjuntos recursivos" (PDF) . Informe técnico No. 2 . Jerusalén: Universidad Hebrea.

Descripción: Este informe técnico fue la primera publicación que habla de lo que más tarde pasó a llamarse complejidad computacional [5]

¿Qué tan bueno es el método simplex? [ editar ]

  • Victor Klee y George J. Minty
  • Klee, Victor ; Minty, George J. (1972). "¿Qué tan bueno es el algoritmo simplex?". En Shisha, Oved (ed.). Desigualdades III (Actas del Tercer Simposio sobre Desigualdades celebrado en la Universidad de California, Los Ángeles, California, del 1 al 9 de septiembre de 1969, dedicado a la memoria de Theodore S. Motzkin) . Nueva York-Londres: Academic Press. págs. 159-175. Señor  0332165 .

Descripción: Construyó el "cubo de Klee-Minty" en la dimensión  D , cuyas esquinas 2 D son visitadas por el algoritmo simplex de Dantzig para la optimización lineal .

Cómo construir funciones aleatorias [ editar ]

  • Goldreich, O .; Goldwasser, S .; Micali, S. (1986). "Cómo construir funciones aleatorias" (PDF) . Revista de la ACM . 33 (4): 792–807. doi : 10.1145 / 6490.6503 . S2CID  17064126 .

Descripción: Este artículo mostró que la existencia de funciones unidireccionales conduce a la aleatoriedad computacional .

IP = PSPACE [ editar ]

  • Shamir, A. (1992). "IP = PSPACE". Revista de la ACM . 39 (4): 869–877. doi : 10.1145 / 146585.146609 . S2CID  315182 .

Descripción: IP es una clase de complejidad cuya caracterización (basada en sistemas de prueba interactivos ) es bastante diferente de las clases computacionales habituales limitadas en tiempo / espacio. En este artículo, Shamir amplió la técnica del artículo anterior de Lund, et al., Para mostrar que PSPACE está contenido en IP y, por lo tanto, IP = PSPACE, de modo que cada problema de una clase de complejidad se puede resolver en la otra.

Reducibilidad entre problemas combinatorios [ editar ]

Artículo principal: 21 problemas NP-completos de Karp
  • RM Karp
  • En RE Miller y JW Thatcher, editores, Complexity of Computer Computations , Plenum Press, Nueva York, NY, 1972, págs. 85-103

Descripción: Este artículo mostró que 21 problemas diferentes son NP-Complete y mostró la importancia del concepto.

La complejidad del conocimiento de los sistemas de prueba interactivos [ editar ]

  • Goldwasser, S .; Micali, S .; Rackoff, C. (1989). "La complejidad del conocimiento de los sistemas de prueba interactivos" (PDF) . SIAM J. Comput. 18 (1): 186–208. doi : 10.1137 / 0218012 .

Descripción: Este artículo introdujo el concepto de conocimiento cero . [6]

Una carta de Gödel a von Neumann [ editar ]

  • Kurt Gödel
  • Una carta de Gödel a John von Neumann , 20 de marzo de 1956
  • Versión en línea

Descripción: Gödel analiza la idea de un demostrador de teoremas universal eficiente.

Sobre la complejidad computacional de los algoritmos [ editar ]

  • Hartmanis, Juris ; Stearns, Richard (1965). "Sobre la complejidad computacional de los algoritmos" . Transacciones de la American Mathematical Society . 117 : 285-306. doi : 10.1090 / s0002-9947-1965-0170805-7 .

Descripción: Este artículo le dio a la complejidad computacional su nombre y semilla.

Caminos, árboles y flores [ editar ]

  • Edmonds, J. (1965). "Caminos, árboles y flores". Revista canadiense de matemáticas . 17 : 449–467. doi : 10.4153 / CJM-1965-045-4 .

Descripción: Existe un algoritmo de tiempo polinomial para encontrar una coincidencia máxima en un gráfico que no es bipartito y otro paso hacia la idea de complejidad computacional . Para obtener más información, consulte [2] .

Teoría y aplicaciones de las funciones de la trampilla [ editar ]

  • Yao, AC (1982). "Teoría y aplicación de las funciones de la trampilla". 23º Simposio Anual sobre Fundamentos de las Ciencias de la Computación (SFCS 1982) . págs. 80–91. doi : 10.1109 / SFCS.1982.45 .

Descripción: Este artículo crea un marco teórico para las funciones de la trampilla y describe algunas de sus aplicaciones, como en la criptografía . Tenga en cuenta que el concepto de funciones de trampilla se presentó en "Nuevas direcciones en criptografía" seis años antes (consulte la sección V "Interrelaciones de problemas y trampillas").

Complejidad computacional [ editar ]

  • CH Papadimitriou
  • Addison-Wesley , 1994, ISBN 0-201-53082-1 

Descripción: Una introducción a la teoría de la complejidad computacional , el libro explica la caracterización de P-SPACE por parte de su autor y otros resultados.

Pruebas interactivas y la dureza de aproximarse a camarillas [ editar ]

  • Feige, U .; Goldwasser, S .; Lovász, L .; Safra, S .; Szegedy, M. (1996). "Pruebas interactivas y la dureza de aproximación de camarillas" . Revista de la ACM . 43 (2): 268-292. doi : 10.1145 / 226643.226652 .

Comprobación probabilística de pruebas: una nueva caracterización de NP [ editar ]

  • Arora, S .; Safra, S. (1998). "Comprobación probabilística de pruebas: una nueva caracterización de NP". Revista de la ACM . 45 : 70-122. doi : 10.1145 / 273865.273901 . S2CID  751563 .

Verificación de la prueba y la dureza de los problemas de aproximación [ editar ]

  • Arora, S .; Lund, C .; Motwani, R .; Sudán, M .; Szegedy, M. (1998). "Comprobación de pruebas y dureza de problemas de aproximación". Revista de la ACM . 45 (3): 501–555. CiteSeerX  10.1.1.145.4652 . doi : 10.1145 / 278298.278306 . S2CID  8561542 .

Descripción: Estos tres artículos establecieron el sorprendente hecho de que ciertos problemas en NP siguen siendo difíciles incluso cuando solo se requiere una solución aproximada. Consulte el teorema de PCP .

La dificultad computacional intrínseca de las funciones [ editar ]

  • Cobham, Alan (1964). "La dificultad computacional intrínseca de las funciones" (PDF) . Actas del Congreso Internacional de Lógica, Metodología y Filosofía de la Ciencia de 1964 : 24–30.

Descripción: Primera definición de la clase de complejidad P. Uno de los artículos fundacionales de la teoría de la complejidad.

Algoritmos [ editar ]

Ver también: Lista de algoritmos

"Un programa de máquina para demostrar teoremas" [ editar ]

  • Davis, M .; Logemann, G .; Loveland, D. (1962). "Un programa de máquina para la demostración de teoremas" (PDF) . Comunicaciones de la ACM . 5 (7): 394–397. doi : 10.1145 / 368273.368557 . hdl : 2027 / mdp.39015095248095 . S2CID  15866917 .

Descripción: El algoritmo DPLL . El algoritmo básico para SAT y otros problemas NP-Complete .

"Una lógica orientada a la máquina basada en el principio de resolución" [ editar ]

  • Robinson, JA (1965). "Una lógica orientada a la máquina basada en el principio de resolución". Revista de la ACM . 12 : 23–41. doi : 10.1145 / 321250.321253 . S2CID  14389185 .

Descripción: Primera descripción de resolución y unificación utilizada en la demostración automatizada de teoremas ; utilizado en Prolog y programación lógica .

"El problema del viajante de comercio y los árboles de expansión mínimos" [ editar ]

  • Held, M .; Karp, RM (1970). "El problema del viajante-vendedor y árboles de expansión mínima". Investigación operativa . 18 (6): 1138-1162. doi : 10.1287 / opre.18.6.1138 .

Descripción: El uso de un algoritmo para el árbol de expansión mínimo como un algoritmo de aproximación para el problema del viajante NP-Complete . Los algoritmos de aproximación se convirtieron en un método común para hacer frente a problemas NP-Complete.

"Un algoritmo polinomial en programación lineal" [ editar ]

  • LG Khachiyan
  • Matemáticas soviéticas - Doklady , vol. 20, págs. 191-194, 1979

Descripción: Durante mucho tiempo, no hubo un algoritmo de tiempo polinomial comprobable para el problema de programación lineal . Khachiyan fue el primero en proporcionar un algoritmo polinomial (y no solo lo suficientemente rápido la mayor parte del tiempo como los algoritmos anteriores). Más tarde, Narendra Karmarkar presentó un algoritmo más rápido en: Narendra Karmarkar, "Un nuevo algoritmo de tiempo polinomial para programación lineal", Combinatorica , vol 4, no. 4, pág. 373–395, 1984.

"Algoritmo probabilístico para probar la primalidad" [ editar ]

  • Rabin, M. (1980). "Algoritmo probabilístico para probar la primalidad". Revista de teoría de números . 12 (1): 128-138. doi : 10.1016 / 0022-314X (80) 90084-0 .

Descripción: El artículo presentó la prueba de primalidad Miller-Rabin y describió el programa de algoritmos aleatorios .

"Optimización mediante recocido simulado" [ editar ]

  • Kirkpatrick, S .; Gelatt, CD; Vecchi, MP (1983). "Optimización por recocido simulado". Ciencia . 220 (4598): 671–680. Código Bibliográfico : 1983Sci ... 220..671K . CiteSeerX  10.1.1.123.7607 . doi : 10.1126 / science.220.4598.671 . PMID  17813860 . S2CID  205939 .

Descripción: Este artículo describió el recocido simulado, que ahora es una heurística muy común para los problemas NP-Complete .

El arte de la programación informática [ editar ]

Artículo principal: El arte de la programación informática
  • Donald Knuth

Descripción: esta monografía tiene cuatro volúmenes que cubren algoritmos populares. Los algoritmos están escritos tanto en inglés como en lenguaje ensamblador MIX (o lenguaje ensamblador MMIX en fascículos más recientes). Esto hace que los algoritmos sean tanto comprensibles como precisos. Sin embargo, el uso de un lenguaje de programación de bajo nivel frustra a algunos programadores más familiarizados con los lenguajes de programación estructurados modernos .

Algoritmos + Estructuras de datos = Programas [ editar ]

Artículo principal: Algoritmos + Estructuras de datos = Programas
  • Niklaus Wirth
  • Prentice Hall, 1976, ISBN 0-13-022418-9 

Descripción: Un libro temprano e influyente sobre algoritmos y estructuras de datos, con implementaciones en Pascal.

El diseño y análisis de algoritmos informáticos [ editar ]

  • Alfred V. Aho , John E. Hopcroft y Jeffrey D. Ullman
  • Addison-Wesley, 1974, ISBN 0-201-00029-6 

Descripción: Uno de los textos estándar sobre algoritmos para el período de aproximadamente 1975-1985.

Cómo resolverlo por computadora [ editar ]

  • Dromey, RG (1982). Cómo resolverlo por computadora . Prentice-Hall International. ISBN 978-0-13-434001-2.

Descripción: Explica el por qué de los algoritmos y estructuras de datos. Explica el proceso creativo , la línea de razonamiento , los factores de diseño detrás de las soluciones innovadoras.

Algoritmos [ editar ]

  • Robert Sedgewick
  • Addison-Wesley, 1983, ISBN 0-201-06672-6 

Descripción: Un texto muy popular sobre algoritmos a fines de la década de 1980. Era más accesible y legible (pero más elemental) que Aho, Hopcroft y Ullman. Hay ediciones más recientes.

Introducción a los algoritmos [ editar ]

Artículo principal: Introducción a los algoritmos
  • Thomas H. Cormen , Charles E. Leiserson , Ronald L. Rivest y Clifford Stein
  • Tercera edición, MIT Press, 2009, ISBN 978-0-262-03384-8 . 

Descripción: Este libro de texto se ha vuelto tan popular que es casi el estándar de facto para enseñar algoritmos básicos. La primera edición (con los tres primeros autores) se publicó en 1990, la segunda edición en 2001 y la tercera en 2009.

Teoría algorítmica de la información [ editar ]

"En tablas de números aleatorios" [ editar ]

  • Kolmogorov, Andrei N. (1963). "En tablas de números aleatorios". Sankhyā Ser. Una . 25 : 369–375. Señor  0178484 .
  • Kolmogorov, Andrei N. (1963). "En tablas de números aleatorios". Informática Teórica . 207 (2): 387–395. doi : 10.1016 / S0304-3975 (98) 00075-9 . Señor  1643414 .

Descripción: Propuesta de un enfoque computacional y combinatorio de la probabilidad.

"Una teoría formal de la inferencia inductiva" [ editar ]

  • Ray Solomonoff
  • Información y Control , vol. 7, págs. 1–22 y 224–254, 1964
  • Copia en línea: parte I , parte II

Descripción: Este fue el comienzo de la teoría algorítmica de la información y la complejidad de Kolmogorov . Tenga en cuenta que aunque la complejidad de Kolmogorov lleva el nombre de Andrey Kolmogorov , dijo que las semillas de esa idea se deben a Ray Solomonoff . Andrey Kolmogorov contribuyó mucho a esta área, pero en artículos posteriores.

"Teoría algorítmica de la información" [ editar ]

  • Chaitin, Gregory (1977). "Teoría algorítmica de la información" (PDF) . IBM Journal of Research and Development . 21 (4): 350–359. CiteSeerX  10.1.1.48.3094 . doi : 10.1147 / rd.214.0350 . Archivado desde el original (PDF) el 30 de mayo de 2009.

Descripción: Una introducción a la teoría de la información algorítmica por una de las personas importantes en el área.

Teoría de la información [ editar ]

"Una teoría matemática de la comunicación" [ editar ]

  • Shannon, CE (1948). "Una teoría matemática de la comunicación" . Revista técnica de Bell System . 27 (3): 379–423, 623–656. doi : 10.1002 / j.1538-7305.1948.tb01338.x . hdl : 10338.dmlcz / 101429 .

Descripción: Este artículo creó el campo de la teoría de la información .

"Error al detectar y corregir los códigos" [ editar ]

  • Hamming, Richard (1950). "Códigos de detección y corrección de errores" . Revista técnica de Bell System . 29 (2): 147–160. doi : 10.1002 / j.1538-7305.1950.tb00463.x . hdl : 10945/46756 .

Descripción: En este artículo, Hamming introdujo la idea del código de corrección de errores . Creó el código Hamming y la distancia Hamming y desarrolló métodos para pruebas de optimización del código.

"Un método para la construcción de códigos mínimos de redundancia" [ editar ]

  • Huffman, D. (1952). "Un método para la construcción de códigos de redundancia mínima" (PDF) . Actas de la IRE . 40 (9): 1098-1101. doi : 10.1109 / JRPROC.1952.273898 .

Descripción: La codificación de Huffman .

"Un algoritmo universal para la compresión secuencial de datos" [ editar ]

  • Ziv, J .; Lempel, A. (1977). "Un algoritmo universal para la compresión secuencial de datos" . Transacciones IEEE sobre teoría de la información . 23 (3): 337–343. CiteSeerX  10.1.1.118.8921 . doi : 10.1109 / TIT.1977.1055714 . hdl : 10338.dmlcz / 142947 . Archivado desde el original el 4 de diciembre de 2003.

Descripción: El algoritmo de compresión LZ77 .

Elementos de la teoría de la información [ editar ]

  • T. Cubierta ; J. Thomas (1991). Elementos de la teoría de la información . págs.  38–42 . ISBN 978-0-471-06259-2.

Descripción: Una introducción popular a la teoría de la información.

Verificación formal [ editar ]

Asignar significado a los programas [ editar ]

  • Floyd, Robert (1967). "Asignar significado a los programas". Aspectos matemáticos de la informática (PDF) . Actas de simposios en matemáticas aplicadas. 19 . págs. 19–32. doi : 10.1090 / psapm / 019/0235771 . ISBN 9780821813195.

Descripción: El artículo histórico de Robert Floyd, Asignación de significados a los programas, presenta el método de afirmaciones inductivas y describe cómo se puede demostrar que un programa anotado con afirmaciones de primer orden satisface una especificación previa y posterior a la condición; el artículo también presenta los conceptos de invariante de bucle y condición de verificación.

Una base axiomática para la programación informática [ editar ]

  • Hoare, CAR (octubre de 1969). "Una base axiomática para la programación informática" (PDF) . Comunicaciones de la ACM . 12 (10): 576–580. doi : 10.1145 / 363235.363259 . S2CID  207726175 . Archivado desde el original (PDF) el 4 de marzo de 2016.

Descripción: El artículo de Tony Hoare An Axiomatic Basis for Computer Programming describe un conjunto de reglas de inferencia (es decir, prueba formal) para fragmentos de un lenguaje de programación tipo Algol descrito en términos de (lo que ahora se llama) Hoare-triples.

Comandos vigilados, no determinación y derivación formal de programas [ editar ]

  • Dijkstra, EW (1975). "Comandos vigilados, no determinación y derivación formal de programas" . Comunicaciones de la ACM . 18 (8): 453–457. doi : 10.1145 / 360933.360975 . S2CID  1679242 .

Descripción: El artículo de Edsger Dijkstra Guarded Commands, Nondeterminacy and Formal Derivation of Programs (ampliado por su libro de texto de nivel de posgrado de 1976 A Discipline of Programming) propone que, en lugar de verificar formalmente un programa después de que ha sido escrito (es decir, post facto), los programas y sus demostraciones formales deben desarrollarse mano a mano (utilizando transformadores de predicado para refinar progresivamente las condiciones previas más débiles), un método conocido como refinamiento (o derivación) de programa (o formal), o algunas veces "corrección por construcción".

Demostrar afirmaciones sobre programas paralelos [ editar ]

  • Edward A. Ashcroft
  • J. Comput. Syst. Sci. 10 (1): 110-135 (1975) doi : 10.1016 / s0022-0000 (75) 80018-3

Descripción: El artículo que introdujo pruebas de invariancia de programas concurrentes.

Una técnica de prueba axiomática para programas paralelos I [ editar ]

  • Susan S. Owicki , David Gries
  • Acta Inform. 6: 319-340 (1976)

Descripción: En este artículo, junto con el artículo del mismo autor "Verificación de propiedades de programas paralelos: un enfoque axiomático. Commun. ACM 19 (5): 279-285 (1976)", se presentó el enfoque axiomático para la verificación de programas paralelos.

Una disciplina de programación [ editar ]

  • Edsger W. Dijkstra
  • 1976

Descripción: El clásico libro de texto de nivel de posgrado de Edsger Dijkstra A Discipline of Programming extiende su artículo anterior Guarded Commands, Nondeterminacy and Formal Derivation of Programs y establece firmemente el principio de derivar formalmente los programas (y sus pruebas) a partir de su especificación.

Semántica denotacional [ editar ]

  • Joe Stoy
  • 1977

Descripción: La semántica denotativa de Joe Stoy es la primera exposición (a nivel de posgrado) en forma de libro del enfoque matemático (o funcional) de la semántica formal de los lenguajes de programación (en contraste con los enfoques operacional y algebraico).

La lógica temporal de los programas [ editar ]

  • Pnueli, A. (1977). "La lógica temporal de los programas". 18º Simposio Anual sobre Fundamentos de la Ciencia de la Computación (SFCS 1977) . IEEE. págs. 46–57. doi : 10.1109 / SFCS.1977.32 . S2CID  117103037 .

Descripción: Se sugirió el uso de la lógica temporal como método de verificación formal.

Caracterización de las propiedades de corrección de programas paralelos utilizando puntos de referencia (1980) [ editar ]

  • E. Allen Emerson , Edmund M. Clarke
  • En Proc. Séptimo Coloquio Internacional sobre Lenguajes y Programación de Autómatas, páginas 169–181, 1980

Descripción: La verificación de modelos se introdujo como un procedimiento para verificar la corrección de programas concurrentes.

Comunicación de procesos secuenciales (1978) [ editar ]

  • COCHE Hoare
  • 1978

Descripción: El documento de procesos secuenciales comunicativos (CSP) de Tony Hoare (original) introduce la idea de procesos concurrentes (es decir, programas) que no comparten variables, sino que cooperan únicamente mediante el intercambio de mensajes sincrónicos.

Un cálculo de sistemas de comunicación [ editar ]

  • Robin Milner
  • 1980

Descripción: El artículo A Calculus of Communicating Systems (CCS) de Robin Milner describe un álgebra de procesos que permite razonar formalmente sobre sistemas de procesos concurrentes, algo que no ha sido posible para modelos anteriores de concurrencia (semáforos, secciones críticas, CSP original).

Desarrollo de software: un enfoque riguroso [ editar ]

  • Cliff Jones
  • 1980

Descripción: El libro de texto de Cliff Jones Desarrollo de software: un enfoque riguroso es la primera exposición completa del Método de desarrollo de Viena (VDM), que había evolucionado (principalmente) en el laboratorio de investigación de IBM en Viena durante la década anterior y que combina la idea de programa refinamiento según Dijkstra con el refinamiento de datos (o reificación) mediante el cual los tipos de datos abstractos definidos algebraicamente se transforman formalmente en representaciones progresivamente más "concretas".

La ciencia de la programación [ editar ]

  • David Gries
  • 1981

Descripción: El libro de texto de David Gries La ciencia de la programación describe el método de precondición más débil de Dijkstra para la derivación de programas formales, excepto de una manera mucho más accesible que la anterior Disciplina de programación de Dijkstra .

Muestra cómo construir programas que funcionen correctamente (sin errores, aparte de los errores tipográficos). Lo hace mostrando cómo usar expresiones de predicado de condición previa y posterior y técnicas de prueba de programas para guiar la forma en que se crean los programas.

Los ejemplos del libro son todos a pequeña escala y claramente académicos (a diferencia del mundo real). Enfatizan algoritmos básicos, como ordenar y fusionar, y manipulación de cadenas. Se incluyen subrutinas (funciones), pero no se abordan los entornos de programación funcional y orientados a objetos.

Comunicación de procesos secuenciales (1985) [ editar ]

  • COCHE Hoare
  • 1985

Descripción: El libro de texto Communicating Sequential Processes (CSP) de Tony Hoare (actualmente la tercera referencia en ciencias de la computación más citada de todos los tiempos) presenta un modelo CSP actualizado en el que los procesos cooperantes ni siquiera tienen variables de programa y que, como CCS, permite que los sistemas de procesos funcionen. ser razonado formalmente.

Lógica lineal (1987) [ editar ]

  • Girard, J.-Y (1987). "Lógica lineal" (PDF) . Informática Teórica . 50 (1): 1–102. doi : 10.1016 / 0304-3975 (87) 90045-4 . Archivado desde el original (PDF) el 29 de noviembre de 2006.

Descripción: La lógica lineal de Girard fue un gran avance en el diseño de sistemas de mecanografía para computación secuencial y concurrente, especialmente para sistemas de mecanografía conscientes de los recursos.

Un cálculo de procesos móviles (1989) [ editar ]

  • R. Milner , J. Parrow, D. Walker
  • 1989
  • Versión en línea: Parte 1 y Parte 2

Descripción: Este artículo presenta el Pi-Calculus , una generalización de CCS que permite la movilidad de procesos. El cálculo es extremadamente simple y se ha convertido en el paradigma dominante en el estudio teórico de lenguajes de programación, sistemas de mecanografía y lógicas de programas.

La notación Z: un manual de referencia [ editar ]

  • Spivey, JM (1992). La notación Z: un manual de referencia (2ª ed.). Prentice Hall International. ISBN 978-0-13-978529-0. Archivado desde el original el 20 de junio de 2016 . Consultado el 24 de agosto de 2009 .

Descripción: El libro de texto clásico de Mike Spivey The Z Notation: A Reference Manual resume la notación Z del lenguaje de especificación formal que, aunque se originó por Jean-Raymond Abrial, había evolucionado (principalmente) en la Universidad de Oxford durante la década anterior.

Comunicación y simultaneidad [ editar ]

  • Robin Milner
  • Prentice-Hall Internacional, 1989

Descripción: El libro de texto Communication and Concurrency de Robin Milner es una exposición más accesible, aunque técnicamente avanzada, de su trabajo anterior de CCS.

una teoría práctica de la programación [ editar ]

  • Eric Hehner
  • Springer, 1993, edición actual en línea aquí

Descripción: la versión actualizada de la programación Predicativa . La base de la UTP de CAR Hoare . Los métodos formales más simples y completos.

Referencias [ editar ]

  1. ↑ a b Smith, Carl H. (1982). "Computabilidad: una introducción a la teoría de funciones recursivas (NJ Cutland)". Revisión SIAM . 24 : 98. doi : 10.1137 / 1024029 .
  2. ^ "Rózsa Péter: fundador de la teoría de la función recursiva" . Mujeres en la ciencia: una selección de 16 colaboradores . Centro de supercomputación de San Diego. 1997 . Consultado el 23 de agosto de 2017 .
  3. ^ "Reseñas de los libros de Rózsa Péter" . www-history.mcs.st-andrews.ac.uk . Consultado el 29 de agosto de 2017 .
  4. ^ a b Daniel Apon, 2010, "Revisión conjunta de la complejidad computacional: una perspectiva conceptual de Oded Goldreich… y la complejidad computacional: un enfoque moderno de Sanjeev Arora y Boaz Barak…" ACM SIGACT News, vol. 41 (4), diciembre de 2010, págs. 12 a 15, véase [1] , consultado el 1 de febrero de 2015.
  5. ^ Shasha, Dennis , "Una entrevista con Michael O. Rabin" , Comunicaciones de la ACM , vol. 53 No. 2, páginas 37–42, febrero de 2010.
  6. ^ SIGACT 2011
  • Grupo de interés especial de ACM sobre algoritmos y teoría de la computación (2011). "Premios: Premio Gödel" . Archivado desde el original el 22 de abril de 2018 . Consultado el 8 de octubre de 2011 .