Por favor, use este identificador para citar o enlazar este ítem:
http://www.monografias.ufop.br/handle/35400000/2738| Título : | Semântica denotacional para o lambda cálculo computacional em Agda. |
| Autor : | Amaro, Maycon José Jorge |
| metadata.dc.contributor.advisor: | Ribeiro, Rodrigo Geraldo |
| metadata.dc.contributor.referee: | Ribeiro, Rodrigo Geraldo Coelho, Dayanne Gouveia Feitosa, Samuel da Silva |
| Palabras clave : | Linguagem de programação - semântica Linguagem de programação - lambda cálculo Conjuntos - teoria dos tipos |
| Fecha de publicación : | 2020 |
| Citación : | AMARO, Maycon José Jorge. Semântica denotacional para o lambda cálculo computacional em Agda. 2020. 26 f. Monografia (Graduação em Ciência da Computação) - Instituto de Ciências Exatas e Biológicas, Universidade Federal de Ouro Preto, Ouro Preto, 2020. |
| Resumen : | Novos recursos para linguagens de programação precisam de uma base teórica sólida antes de serem implementados, e frequentemente são modelados através de um sistema menor—os λ-cálculos—capaz de capturar a essência das linguagens e separá-las dos syntatic sugars. A semântica denotacional desses sistemas é extremamente útil para o racícionio sobre programas e suas propriedades. Este trabalho formaliza, em Agda, o modelo padrão de uma semântica denotacional para o λ-cálculo computacional, que estende o λ-cálculo tipado simples com um operador modal usado para definir computações envolvendo diferentes efeitos colaterais. |
| metadata.dc.description.abstracten: | New features for programming languages require solid foundations before implementation. These features are often modeled by smaller systems—the λ-calculi—that capture the language’s core and separate them from the syntatic sugars. The denotational semantics of those systems are a very helpful tool in reasoning about programs and their properties. This work formalizes, in Agda, the standard model for the computational λ-calculus, a system that extends the simply typed λ-calculus with a modal operator used to define computations involving different side effects. |
| URI : | http://www.monografias.ufop.br/handle/35400000/2738 |
| Aparece en las colecciones: | Ciência da Computação |
Ficheros en este ítem:
| Fichero | Descripción | Tamaño | Formato | |
|---|---|---|---|---|
| MONOGRAFIA_SemanticaDenotacionalLambda.pdf | 454,3 kB | Adobe PDF | Visualizar/Abrir |
Este ítem está sujeto a una licencia Creative Commons Licencia Creative Commons
