Use este identificador para citar ou linkar para este item:
http://www.monografias.ufop.br/handle/35400000/2738| Título: | Semântica denotacional para o lambda cálculo computacional em Agda. |
| Autor(es): | Amaro, Maycon José Jorge |
| Orientador(es): | Ribeiro, Rodrigo Geraldo |
| Membros da banca: | Ribeiro, Rodrigo Geraldo Coelho, Dayanne Gouveia Feitosa, Samuel da Silva |
| Palavras-chave: | Linguagem de programação - semântica Linguagem de programação - lambda cálculo Conjuntos - teoria dos tipos |
| Data do documento: | 2020 |
| Referência: | 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. |
| Resumo: | 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. |
| Resumo em outra língua: | 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 nas coleções: | Ciência da Computação |
Arquivos associados a este item:
| Arquivo | Descrição | Tamanho | Formato | |
|---|---|---|---|---|
| MONOGRAFIA_SemanticaDenotacionalLambda.pdf | 454,3 kB | Adobe PDF | Visualizar/Abrir |
Este item está licenciado sob uma Licença Creative Commons
