Please use this identifier to cite or link to this item:
http://www.monografias.ufop.br/handle/35400000/2738| Title: | Semântica denotacional para o lambda cálculo computacional em Agda. |
| Authors: | 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 |
| Keywords: | Linguagem de programação - semântica Linguagem de programação - lambda cálculo Conjuntos - teoria dos tipos |
| Issue Date: | 2020 |
| Citation: | 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. |
| Abstract: | 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 |
| Appears in Collections: | Ciência da Computação |
Files in This Item:
| File | Description | Size | Format | |
|---|---|---|---|---|
| MONOGRAFIA_SemanticaDenotacionalLambda.pdf | 454,3 kB | Adobe PDF | View/Open |
This item is licensed under a Creative Commons License
