Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/85093
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.advisor | Espírito Santo, José | por |
dc.contributor.author | Mendes, Filipa Simões | por |
dc.date.accessioned | 2023-06-20T08:37:26Z | - |
dc.date.available | 2023-06-20T08:37:26Z | - |
dc.date.issued | 2023-01-11 | - |
dc.date.submitted | 2022-10 | - |
dc.identifier.uri | https://hdl.handle.net/1822/85093 | - |
dc.description | Dissertação de mestrado em Matemática e Computação | por |
dc.description.abstract | Plotkin apresentou em 1975 a primeira proposta para o cálculo-lambda call-by-value, um sistema formal que modela uma linguagem de programação call-by-value, e vários outros sistemas têm sidos pro postos desde então. No entanto, este sistema é incompleto para a semântica CPS (continuation-passing style), ou seja, existem termos com a mesma semântica que não podem ser provados iguais no cálculo de Plotkin. Nesta dissertação estudamos a extensão de Sabry-Felleisen, o cálculo computacional de Moggi e o cálculo-𝜆𝑄 de Dyckhoff-Lengrand, três sistemas formais com origens diferentes, que são uma resposta ao problema da incompletude do cálculo de Plotkin relativamente à semântica CPS. Provamos que existe uma correspondência equacional entre a extensão de Sabry-Felleisen e o cálculo computacional. Propomos uma simplificação do cálculo-𝜆𝑄 e identificamos o núcleo correspondente. Por fim, provamos que existe uma correspondência equacional entre o núcleo do cálculo-𝜆𝑄 simplificado e o núcleo do cálculo computacional. | por |
dc.description.abstract | In 1975 Plotkin presented the very first call-by-value lambda-calculus, a formal system that models a call-by-value programming language. Since then, many other systems has been presented. Nevertheless, this system turned out to be incomplete for the CPS (continuation-passing-style) semantics. In other words, there are terms with the same semantic that are not proved equal in Plotkin’s lambda-calculus. In this dissertation, we study Sabry-Felleisen’s extension of Plotkin’s calculus, Moggi’s computational lambda-calculus and Dyckhoff-Lengrand’s 𝜆𝑄-calculus, three formal systems with different origins, that are an answer to Plotkin’s incompleteness problem with respect to CPS semantics. We prove that there is an equational correspondence between Sabry-Felleisen’s extension and the computational calculus. We present a simplified 𝜆𝑄-calculus and we identify its kernel. Finally, we prove that there is an equational correspondence between the kernel of the simplified 𝜆𝑄-calculus and the kernel of the computational lambda-calculus. | por |
dc.language.iso | por | por |
dc.rights | openAccess | por |
dc.rights.uri | http://creativecommons.org/licenses/by-nc/4.0/ | por |
dc.subject | Cálculo-lambda | por |
dc.subject | Call-by-value | por |
dc.subject | Call-by-name | por |
dc.subject | Continuation-passing-style | por |
dc.subject | Linguagens de programação funcionais | por |
dc.subject | Cálculo de sequentes | por |
dc.subject | Lógica intuicionista | por |
dc.subject | Lambda-calculus | por |
dc.subject | Funcional programming languages | por |
dc.subject | Sequent calculus | por |
dc.subject | Intuicionistic logic | por |
dc.title | Variações sobre o cálculo-lambda call-by-value | por |
dc.title.alternative | Variations about the call-by-value lambda-calculus | por |
dc.type | masterThesis | eng |
dc.identifier.tid | 203267001 | por |
thesis.degree.grantor | Universidade do Minho | por |
sdum.degree.grade | 19 valores | por |
sdum.uoei | Escola de Ciências | por |
dc.subject.fos | Ciências Naturais::Matemáticas | por |
Aparece nas coleções: | BUM - Dissertações de Mestrado DMAT - Dissertações de Mestrado |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Filipa Simoes Mendes.pdf | Dissertação de Mestrado | 436,82 kB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons