En informática , la semántica denotacional (inicialmente conocida como semántica matemática o semántica de Scott-Strachey ) es un enfoque para formalizar los significados de los lenguajes de programación mediante la construcción de objetos matemáticos (llamados denotaciones ) que describen los significados de las expresiones de dichos lenguajes. Otros enfoques que proporcionan semántica formal de los lenguajes de programación incluyen la semántica axiomática y la semántica operacional .
En términos generales, la semántica denotacional se ocupa de encontrar objetos matemáticos llamados dominios que representan lo que hacen los programas. Por ejemplo, los programas (o frases de programas) podrían representarse mediante funciones parciales [ 1 ] [ 2 ] o mediante juegos [ 3 ] entre el entorno y el sistema.
Un principio importante de la semántica denotacional es que la semántica debe ser compositiva : la denotación de una frase de programa debe construirse a partir de las denotaciones de sus subfrases .
Desarrollo histórico
La semántica denotacional se originó en el trabajo de Christopher Strachey y Dana Scott, publicado a principios de la década de 1970. [ 1 ] [ 2 ] Tal como la desarrollaron originalmente Strachey y Scott, la semántica denotacional proporcionaba el significado de un programa informático como una función que mapeaba la entrada en la salida. [ 2 ] Para dar significado a los programas definidos recursivamente , Scott propuso trabajar con funciones continuas entre dominios , específicamente órdenes parciales completas . Como se describe a continuación, el trabajo ha continuado investigando la semántica denotacional apropiada para aspectos de los lenguajes de programación tales como la secuencialidad, la concurrencia , el no determinismo y el estado local .
Se ha desarrollado una semántica denotacional para lenguajes de programación modernos que utilizan capacidades como la concurrencia y las excepciones , por ejemplo, Concurrent ML , [ 4 ] CSP , [ 5 ] y Haskell . [ 6 ] La semántica de estos lenguajes es compositiva, ya que el significado de una frase depende de los significados de sus subfrases. Por ejemplo, el significado de la expresión aplicativaf(E1,E2) se define en términos de la semántica de sus subfrases f, E1 y E2. En un lenguaje de programación moderno, E1 y E2 pueden evaluarse concurrentemente y la ejecución de una de ellas puede afectar a la otra al interactuar a través de objetos compartidos , lo que hace que sus significados se definan en términos de la otra. Además, E1 o E2 pueden lanzar una excepción que podría terminar la ejecución de la otra. Las secciones siguientes describen casos especiales de la semántica de estos lenguajes de programación modernos.
Significados de los programas recursivos
La semántica denotacional se atribuye a una frase de programa como una función de un entorno (que contiene los valores actuales de sus variables libres) a su denotación. Por ejemplo, la frase n*mproduce una denotación cuando se le proporciona un entorno que tiene enlaces para sus dos variables libres: ny m. Si en el entorno ntiene el valor 3 y mtiene el valor 5, entonces la denotación es 15. [ 2 ]
Una función puede representarse como un conjunto de pares ordenados de argumentos y sus correspondientes valores de resultado. Por ejemplo, el conjunto {(0,1), (4,3)} denota una función cuyo resultado es 1 para el argumento 0, 3 para el argumento 4 y no está definido en los demás casos.
Consideremos, por ejemplo, la función factorial , que podría definirse recursivamente como:
int factorial ( int n ) { if ( n == 0 ) return 1 ; else return n * factorial ( n - 1 ); }Para dar sentido a esta definición recursiva, la denotación se construye como el límite de aproximaciones, donde cada aproximación limita el número de llamadas a factorial. Al principio, comenzamos sin llamadas, por lo tanto, no hay nada definido. En la siguiente aproximación, podemos agregar el par ordenado (0,1), porque esto no requiere volver a llamar a factorial. De manera similar, podemos agregar (1,1), (2,2), etc., agregando un par en cada aproximación sucesiva porque calcular factorial(n) requiere n+1 llamadas. En el límite obtenemos una función total deadefinido en todas partes dentro de su dominio.
Formalmente, modelamos cada aproximación como una función parcial.. Nuestra aproximación consiste entonces en aplicar repetidamente una función que implementa "hacer una función factorial parcial más definida", es decir, comenzando con la función vacía (conjunto vacío). F podría definirse en el código de la siguiente manera (usando Map<int,int>para ):
int factorial_nonrecursive ( Map < int , int > factorial_less_defined , int n ) { if ( n == 0 ) then return 1 ; else if ( fprev = lookup ( factorial_less_defined , n -1 )) then return n * fprev ; else return NOT_DEFINED ; }Map < int , int > F ( Map < int , int > factorial_less_defined ) { Map < int , int > new_factorial = Map . empty (); for ( int n in all < int > ()) { if ( f = factorial_nonrecursive ( factorial_less_defined , n ) != NOT_DEFINED ) new_factorial . put ( n , f ); } return new_factorial ; }Entonces podemos introducir la notación F n para indicar que F se aplica n veces .
- F 0 ({}) es la función parcial totalmente indefinida, representada como el conjunto {};
- F 1 ({}) es la función parcial representada como el conjunto {(0,1)}: está definida en 0, es 1 y no está definida en ningún otro lugar;
- F 5 ({}) es la función parcial representada como el conjunto {(0,1), (1,1), (2,2), (3,6), (4,24)}: está definida para los argumentos 0,1,2,3,4.
Este proceso iterativo construye una secuencia de funciones parciales a partir deaLas funciones parciales forman un orden parcial completo en cadena usando ⊆ como ordenación. Además, este proceso iterativo de mejores aproximaciones de la función factorial forma una aplicación expansiva (también llamada progresiva) porque cadausando ⊆ como ordenación. Por lo tanto, según un teorema de punto fijo (específicamente el teorema de Bourbaki-Witt ), existe un punto fijo para este proceso iterativo.
En este caso, el punto fijo es el límite superior mínimo de esta cadena, que es la factorialfunción completa, la cual puede expresarse como la unión
El punto fijo que encontramos es el punto fijo más pequeño de F , porque nuestra iteración comenzó con el elemento más pequeño del dominio (el conjunto vacío). Para demostrar esto, necesitamos un teorema de punto fijo más complejo, como el teorema de Knaster-Tarski .
Semántica denotacional de programas no deterministas
El concepto de dominios de potencia se ha desarrollado para dar una semántica denotacional a los programas secuenciales no deterministas. Escribiendo P para un constructor de dominio de potencia, el dominio P ( D ) es el dominio de los cálculos no deterministas del tipo denotado por D .
Existen dificultades con la equidad y la no limitación en los modelos de no determinismo basados en la teoría de dominios. [ 7 ]
Semántica denotacional de la concurrencia
Muchos investigadores han argumentado que los modelos teóricos de dominio presentados anteriormente no son suficientes para el caso más general de computación concurrente . Por esta razón, se han introducido varios modelos nuevos . A principios de la década de 1980, se comenzó a utilizar el estilo de la semántica denotacional para dar semántica a los lenguajes concurrentes. Ejemplos de ello son el trabajo de Will Clinger con el modelo de actor ; el trabajo de Glynn Winskel con estructuras de eventos y redes de Petri ; [ 8 ] y el trabajo de Francez, Hoare, Lehmann y de Roever (1979) sobre semántica de trazas para CSP. [ 9 ] Todas estas líneas de investigación siguen en estudio (véase, por ejemplo, los diversos modelos denotacionales para CSP [ 5 ] ).
Recientemente, Winskel y otros han propuesto la categoría de profunctores como una teoría de dominio para la concurrencia. [ 10 ] [ 11 ]
Semántica denotacional del estado
Los estados (como un montón) y las características imperativas simples se pueden modelar directamente en la semántica denotacional descrita anteriormente. La idea clave es considerar un comando como una función parcial en algún dominio de estados. El significado de " x:=3" es entonces la función que lleva un estado al estado con 3asignado a x. El operador de secuenciación " ;" se denota por la composición de funciones. Luego se utilizan construcciones de punto fijo para dar una semántica a construcciones de bucle, como " while".
Las cosas se complican al modelar programas con variables locales. Un enfoque consiste en dejar de trabajar con dominios y, en su lugar, interpretar los tipos como functores de alguna categoría de mundos a una categoría de dominios. Los programas se denotan entonces mediante funciones continuas naturales entre estos functores. [ 12 ] [ 13 ]
Denotaciones de tipos de datos
Muchos lenguajes de programación permiten a los usuarios definir tipos de datos recursivos . Por ejemplo, el tipo de listas de números se puede especificar mediante
lista de tipos de datos = Cons de nat * lista | VacíoEsta sección trata únicamente de estructuras de datos funcionales que no pueden modificarse. Los lenguajes de programación imperativos convencionales suelen permitir que los elementos de una lista recursiva de este tipo se modifiquen.
Por otro ejemplo: el tipo de denotaciones del cálculo lambda sin tipo es
tipo de datos D = D de ( D → D )El problema de resolver ecuaciones de dominio se centra en encontrar dominios que modelen este tipo de datos. Un enfoque, en términos generales, consiste en considerar el conjunto de todos los dominios como un dominio en sí mismo y, a partir de ahí, resolver la definición recursiva.
Los tipos de datos polimórficos son tipos de datos que se definen con un parámetro. Por ejemplo, el tipo de α lists se define mediante
Lista de tipo de datos α = Cons de α * lista α | VacíaLas listas de números naturales, entonces, son de tipo nat list, mientras que las listas de cadenas son de string list.
Algunos investigadores han desarrollado modelos de polimorfismo basados en la teoría de dominios. Otros investigadores también han modelado el polimorfismo paramétrico dentro de las teorías constructivas de conjuntos.
Un área de investigación reciente ha involucrado la semántica denotacional para lenguajes de programación basados en objetos y clases. [ 14 ]
Semántica denotacional para programas de complejidad restringida
Tras el desarrollo de lenguajes de programación basados en lógica lineal , se han dotado de semántica denotacional a lenguajes para uso lineal (véase, por ejemplo, redes de prueba , espacios de coherencia ) y también complejidad temporal polinomial. [ 15 ]
Semántica denotacional de la secuencialidad
El problema de la abstracción total para el lenguaje de programación secuencial PCF fue, durante mucho tiempo, una gran incógnita en la semántica denotacional. La dificultad de PCF radica en su naturaleza eminentemente secuencial. Por ejemplo, no existe una forma de definir la función `parallel-or` en PCF. Por esta razón, el enfoque que utiliza dominios, como se mencionó anteriormente, produce una semántica denotacional que no es completamente abstracta.
Esta cuestión abierta se resolvió en gran medida en la década de 1990 con el desarrollo de la semántica de juegos y también con técnicas que involucran relaciones lógicas . [ 16 ] Para más detalles, consulte la página sobre PCF.
La semántica denotacional como traducción de fuente a fuente
A menudo resulta útil traducir un lenguaje de programación a otro. Por ejemplo, un lenguaje de programación concurrente podría traducirse a un cálculo de procesos ; un lenguaje de programación de alto nivel podría traducirse a código de bytes. (De hecho, la semántica denotacional convencional puede considerarse como la interpretación de los lenguajes de programación al lenguaje interno de la categoría de dominios).
En este contexto, las nociones de la semántica denotacional, como la abstracción completa, ayudan a satisfacer las preocupaciones de seguridad. [ 17 ] [ 18 ]
Abstracción
A menudo se considera importante vincular la semántica denotacional con la semántica operacional . Esto es especialmente importante cuando la semántica denotacional es más matemática y abstracta, y la semántica operacional es más concreta o cercana a las intuiciones computacionales. Las siguientes propiedades de la semántica denotacional suelen ser de interés.
- Independencia sintáctica : Las denotaciones de los programas no deben involucrar la sintaxis del lenguaje fuente.
- Adecuación (o solidez) : Todos los programas observablemente distintos tienen denotaciones distintas;
- Abstracción total : Todos los programas observacionalmente equivalentes tienen denotaciones iguales.
En la semántica tradicional, la adecuación y la abstracción total pueden entenderse, a grandes rasgos, como el requisito de que «la equivalencia operacional coincida con la igualdad denotacional». En la semántica denotacional de modelos más intensionales, como el modelo de actores y los cálculos de procesos , existen diferentes nociones de equivalencia dentro de cada modelo, por lo que los conceptos de adecuación y abstracción total son objeto de debate y más difíciles de definir. Asimismo, la estructura matemática de la semántica operacional y la denotacional puede llegar a ser muy similar.
Otras propiedades deseables que podríamos desear mantener entre la semántica operacional y la denotacional son:
- Constructivismo : El constructivismo se ocupa de si se puede demostrar la existencia de los elementos de un dominio mediante métodos constructivos.
- Independencia de la semántica denotacional y operacional : La semántica denotacional debe formalizarse mediante estructuras matemáticas independientes de la semántica operacional del lenguaje de programación; sin embargo, los conceptos subyacentes pueden estar estrechamente relacionados. Véase la sección sobre composicionalidad más adelante.
- Completitud o definibilidad total : Cada morfismo del modelo semántico debe ser la denotación de un programa. [ 19 ]
Composicionalidad
Un aspecto importante de la semántica denotacional de los lenguajes de programación es la composicionalidad, mediante la cual la denotación de un programa se construye a partir de las denotaciones de sus partes. Por ejemplo, consideremos la expresión "7 + 4". La composicionalidad en este caso consiste en proporcionar un significado a "7 + 4" en términos de los significados de "7", "4" y "+".
Una semántica denotacional básica en la teoría de dominios es composicional porque se da de la siguiente manera. Comenzamos considerando fragmentos de programas, es decir, programas con variables libres. Un contexto de tipado asigna un tipo a cada variable libre. Por ejemplo, en la expresión ( x + y ) podría considerarse en un contexto de tipado ( x : nat, y : nat). Ahora damos una semántica denotacional a los fragmentos de programas, utilizando el siguiente esquema.
- Comenzamos describiendo el significado de los tipos de nuestro lenguaje: el significado de cada tipo debe ser un dominio. Escribimos 〚τ〛 para el dominio que denota el tipo τ. Por ejemplo, el significado del tipo
natdebe ser el dominio de los números naturales: 〚nat〛=⊥ . - Del significado de los tipos derivamos un significado para los contextos de tipado. Establecemos 〚x 1 :τ 1 ,..., x n :τ n〛 = 〚 τ 1〛× ... ×〚τ n〛. Por ejemplo, 〚x :
nat, y :nat〛=⊥ ×⊥ . Como caso especial, el significado del contexto de tipado vacío, sin variables, es el dominio con un elemento, denotado 1. - Finalmente, debemos dar un significado a cada fragmento de programa en contexto de tipado. Supongamos que P es un fragmento de programa de tipo σ, en contexto de tipado Γ, a menudo escrito Γ⊢ P :σ. Entonces, el significado de este programa en contexto de tipado debe ser una función continua 〚Γ⊢ P :σ〛:〚Γ〛→〚σ〛. Por ejemplo, 〚⊢7:
nat〛:1→⊥ es la función "7" constante, mientras que 〚x :nat, y :nat⊢ x + y :nat〛:⊥ ×⊥ →⊥ es la función que suma dos números.
Ahora bien, el significado de la expresión compuesta (7+4) se determina componiendo las tres funciones 〚⊢7: nat〛:1→⊥ , 〚⊢4: nat〛:1→⊥ , y 〚x : nat, y : nat⊢ x + y : nat〛:⊥ ×⊥ →⊥ .
De hecho, este es un esquema general para la semántica denotacional compositiva. No hay nada específico sobre dominios y funciones continuas aquí. Se puede trabajar con una categoría diferente . Por ejemplo, en la semántica de juegos, la categoría de juegos tiene juegos como objetos y estrategias como morfismos: podemos interpretar tipos como juegos y programas como estrategias. Para un lenguaje simple sin recursión general, podemos usar la categoría de conjuntos y funciones . Para un lenguaje con efectos secundarios, podemos trabajar en la categoría de Kleisli para una mónada. Para un lenguaje con estado, podemos trabajar en una categoría de functores . Milner ha defendido el modelado de la ubicación y la interacción trabajando en una categoría con interfaces como objetos y bigrafos como morfismos. [ 20 ]
Semántica versus implementación
Según Dana Scott (1980): [ 21 ]
- No es necesario que la semántica determine una implementación, pero sí debe proporcionar criterios para demostrar que una implementación es correcta.
Según Clinger (1981): [ 22 ] : 79
- Por lo general, la semántica formal de un lenguaje de programación secuencial convencional puede interpretarse como una implementación (ineficiente) del lenguaje. Sin embargo, la semántica formal no siempre tiene por qué proporcionar dicha implementación, y creer que debe hacerlo genera confusión respecto a la semántica formal de los lenguajes concurrentes. Esta confusión se hace dolorosamente evidente cuando se afirma que la presencia de no determinismo ilimitado en la semántica de un lenguaje de programación implica que dicho lenguaje no puede implementarse.
Conexiones con otras áreas de la informática
Algunos trabajos en semántica denotacional han interpretado los tipos como dominios en el sentido de la teoría de dominios, que puede considerarse una rama de la teoría de modelos , lo que genera conexiones con la teoría de tipos y la teoría de categorías . Dentro de la informática, existen conexiones con la interpretación abstracta , la verificación de programas y la comprobación de modelos .
Referencias
- 1 2 Dana S. Scott. Esquema de una teoría matemática de la computación . Monografía técnica PRG-2, Laboratorio de Computación de la Universidad de Oxford, Oxford, Inglaterra, noviembre de 1970.
- 1 2 3 4 Dana Scott y Christopher Strachey . Hacia una semántica matemática para lenguajes de programación . Monografía técnica del Grupo de Investigación en Programación de Oxford. PRG-6. 1971.
- ↑ Jan Jürjens. J. Juegos en la semántica de los lenguajes de programación: una introducción elemental. Synthese 133, 131–158 (2002). https://doi.org/10.1023/A:1020883810034
- ↑ John Reppy, "Aprendizaje automático concurrente: diseño, aplicación y semántica", en Springer-Verlag, Lecture Notes in Computer Science , vol. 693, 1993.
- 1 2 A. W. Roscoe . "La teoría y la práctica de la concurrencia". Prentice-Hall. Edición revisada de 2005.
- ↑ Simon Peyton Jones , Alastair Reid, Fergus Henderson, Tony Hoare y Simon Marlow. " Una semántica para excepciones imprecisas ". Conferencia sobre diseño e implementación de lenguajes de programación. 1999.
- ↑ Levy, Paul Blain (2007). "Amb rompe la buena agudeza, Ground Amb no" . Electron. Notes Theor. Comput. Sci . 173 : 221–239 . doi : 10.1016/j.entcs.2007.02.036 .
- ↑ Semántica de la estructura de eventos para CCS y lenguajes relacionados . Informe de investigación de DAIMI, Universidad de Aarhus, 67 págs., abril de 1983.
- ↑ Nissim Francez , CAR Hoare , Daniel Lehmann y Willem-Paul de Roever . " Semántica del no determinismo, la concurrencia y la comunicación ", Journal of Computer and System Sciences . Diciembre de 1979.
- ↑ Cattani, Gian Luca; Winskel, Glynn (2005). "Profunctors, open maps and bisimulation". Mathematical Structures in Computer Science . 15 (3): 553– 614. CiteSeerX 10.1.1.111.6243 . doi : 10.1017/S0960129505004718 . S2CID 16356708 .
- ↑ Nygaard, Mikkel; Winskel, Glynn (2004). "Teoría de dominios para la concurrencia" . Theor. Comput. Sci . 316 ( 1–3 ): 153–190 . doi : 10.1016/j.tcs.2004.01.029 .
- ↑ Peter W. O'Hearn , John Power, Robert D. Tennent , Makoto Takeyama. Control sintáctico de la interferencia: una revisión. Electron. Notes Theor. Comput. Sci. 1. 1995.
- ↑ Frank J. Oles. Un enfoque de teoría de categorías a la semántica de la programación . Tesis doctoral, Universidad de Syracuse , Nueva York, EE. UU. 1982.
- ↑ Reus, Bernhard; Streicher, Thomas (2004). "Semántica y lógica de los cálculos de objetos" . Theor. Comput. Sci . 316 (1): 191– 213. doi : 10.1016/j.tcs.2004.01.030 .
- ↑ Baillot, P. (2004). "Espacios de coherencia estratificados: una semántica denotacional para la lógica lineal ligera" . Theor. Comput. Sci . 318 ( 1–2 ): 29–55 . doi : 10.1016/j.tcs.2003.10.015 .
- ↑ O'Hearn, PW; Riecke, JG (julio de 1995). "Relaciones lógicas de Kripke y PCF" . Information and Computation . 120 (1): 107– 116. doi : 10.1006/inco.1995.1103 . S2CID 6886529 .
- ↑ Martin Abadi. "Protección en traducciones de lenguajes de programación". Actas de ICALP'98 . LNCS 1443. 1998.
- ↑ Kennedy, Andrew (2006). "Asegurando el modelo de programación .NET" . Theor. Comput. Sci . 364 (3): 311– 7. doi : 10.1016/j.tcs.2006.08.014 .
- ↑ Curien, Pierre-Louis (2007). "Definibilidad y abstracción completa" . Electronic Notes in Theoretical Computer Science . 172 : 301–310 . doi : 10.1016/j.entcs.2007.02.011 .
- ↑ Milner, Robin (2009). El espacio y el movimiento de los agentes comunicantes . Cambridge University Press. ISBN 978-0-521-73833-0.Borrador de 2009. Archivado el 2 de abril de 2012 en Wayback Machine .
- ↑ "¿Qué es la semántica denotacional?", Serie de conferencias distinguidas del Laboratorio de Ciencias de la Computación del MIT, 17 de abril de 1980, citado en Clinger (1981).
- ↑ Clinger, William D. (mayo de 1981). Fundamentos de la semántica de actores (tesis doctoral). Instituto Tecnológico de Massachusetts. hdl : 1721.1/6935 . AITR-633.
Lecturas adicionales
- Libros de texto
- Milne, RE; Strachey, C. (1976). Una teoría de la semántica de los lenguajes de programación . ISBN 978-1-5041-2833-9.
- Gordon, MJC (2012) [1979]. La descripción denotacional de los lenguajes de programación: una introducción . Springer. ISBN 978-1-4612-6228-2.
- Stoy, Joseph E. (1977). Semántica denotacional: El enfoque de Scott-Strachey para la semántica de los lenguajes de programación . MIT Press. ISBN 978-0-262-19147-0.(Un libro de texto clásico, aunque algo anticuado).
- Schmidt, David A. (1986). Semántica denotacional: una metodología para el desarrollo del lenguaje . Allyn & Bacon. ISBN 978-0-205-10450-5.
- Actualmente agotado; versión electrónica gratuita disponible: Schmidt, David A. (1997) [1986]. Denotational Semantics: A Methodology for Language Development . Kansas State University.
- Gunter, Carl (1992). Semántica de los lenguajes de programación: estructuras y técnicas . MIT Press. ISBN 978-0-262-07143-7.
- Winskel, Glynn (1993). Semántica formal de los lenguajes de programación . MIT Press. ISBN 978-0-262-73103-4.
- Tennent, RD (1994). «Semántica denotacional». En Abramsky, S.; Gabbay, Dov M.; Maibaum, TSE (eds.). Estructuras semánticas . Manual de lógica en informática. Vol. 3. Oxford University Press. pp. 169–322 . ISBN 978-0-19-853762-5.
- Abramsky, S .; Jung, A. (1994). "Teoría del dominio" (PDF) . Abramsky, Gabbay y Maibaum 1994 .
- Stoltenberg-Hansen, V.; Lindström, I.; Griffor, ER (1994). Teoría matemática de dominios . Cambridge University Press. ISBN 978-0-521-38344-8.
- Apuntes de clase
- Winskel, Glynn. "Semántica Denotacional" (PDF) . Universidad de Cambridge.
- Otras referencias
- Greif, Irene (agosto de 1975). Semántica de los procesos paralelos comunicantes (PDF) (tesis doctoral). Proyecto MAC. Instituto Tecnológico de Massachusetts. ADA016302.
- Plotkin, GD (1976). "Una construcción de dominio de potencia". SIAM J. Comput . 5 (3): 452– 487. CiteSeerX 10.1.1.158.4318 . doi : 10.1137/0205035 .
- Dijkstra, Edsger W. (1976). Una disciplina de programación . Serie Prentice-Hall en computación automática. Englewood Cliffs, NJ ISBN 0-13-215871-XOCLC 1958445 .
{{cite book}}: CS1 mantenimiento: falta el editor de ubicación ( enlace ) - Apto, Krzysztof R .; de Bakker, JW (1976). Ejercicios de semántica denotacional . Afdeling Informática. Ámsterdam: Mathematisch Centrum. OCLC 63400684 .
- De Bakker, JW (1976). "Revisión de los puntos fijos mínimos" . Theoretical Computer Science . 2 (2): 155– 181. doi : 10.1016/0304-3975(76)90031-1 .
- Smyth, Michael B. (1978). "Dominios de poder" . J. Comput. Syst. Sci . 16 : 23–36 . doi : 10.1016/0022-0000(78)90048-X .
- Francez, Nissim; Hoare, CAR; Lehmann, Daniel; de Roever, Willem-Paul (diciembre de 1979). Semántica del no determinismo, la concurrencia y la comunicación . Lecture Notes in Computer Science. Vol. 64. pp. 191–200 . doi : 10.1007/3-540-08921-7_67 . hdl : 1874/15886 . ISBN 978-3-540-08921-6.
{{cite book}}:|work=ignorado ( ayuda ) - Lynch, Nancy ; Fischer, Michael J. (1979). «Sobre la descripción del comportamiento de los sistemas distribuidos» . En Kahn, G. (ed.). Semántica de la computación concurrente: actas del simposio internacional, Évian, Francia, 2-4 de julio de 1979. Springer. ISBN 978-3-540-09511-8.
- Schwartz, Jerald (1979). "Semántica denotacional del paralelismo". Kahn 1979 .
- Wadge, William (1979). "Un tratamiento extensional del bloqueo de flujo de datos". Kahn 1979 .
- Back, Ralph-Johan (1980). «Semántica del no determinismo ilimitado» . En de Bakker, Jaco; van Leeuwen, Jan (eds.). Autómatas, lenguajes y programación . Lecture Notes in Computer Science. Vol. 85. Berlín, Heidelberg: Springer. pp. 51–63 . doi : 10.1007/3-540-10003-2_59 . ISBN 978-3-540-39346-7OCLC 476017025
- Park, David (1980). «Sobre la semántica del paralelismo justo» . En Bjøorner, Dines (ed.). Abstract Software Specifications (PDF) . Lecture Notes in Computer Science. Vol. 86. Berlín, Heidelberg: Springer Berlin Heidelberg. pp. 504–526 . doi : 10.1007/3-540-10007-5_47 . ISBN 978-3-540-10007-2.
- Allison, L. (1986). Una introducción práctica a la semántica denotacional . Cambridge University Press. ISBN 978-0-521-31423-7.
- America, P.; de Bakker, J.; Kok, JN; Rutten, J. (1989). "Semántica denotacional de un lenguaje orientado a objetos paralelo" . Information and Computation . 83 (2): 152– 205. doi : 10.1016/0890-5401(89)90057-6 . S2CID 2405175 .
- Schmidt, David A. (1994). La estructura de los lenguajes de programación tipados . MIT Press. ISBN 978-0-262-69171-0.
Enlaces externos
- Semántica denotacional . Resumen del libro de Lloyd Allison.
- Schreiner, Wolfgang (1995). "Estructura de los lenguajes de programación I: Semántica denotacional" . Apuntes del curso .
- semántica denotacional
- 1970 en informática
- Lógica en informática
- Modelos de computación
- lenguajes de especificación formal
- semántica de lenguajes de programación