20 de maio às 15h00
Programa Doutoral | Ciência de Computadores
Provas | A Quantitative Study of Higher-Order Computations with Effects
Estudante | Jorge Miguel Soares Ramos
Data: 20 de maio
Hora: 15h00
Local: Sala FC6 029
Presidente:
António Mário da Silva Marcos Florido
Professor Catedrático
Departamento de Ciência de Computadores, Faculdade de Ciências da Universidade do Porto
Arguentes:
Ugo Dal Lago
Full Professor
Dipartimento di Informatica - Scienza e Ingegneria, University of Bologna (Itália)
Danel Ahman
Associate Professor
Institute of Computer Science, University of Tartu (Estónia)
Vogais:
Sabine Babette Broda
Professora Associada
Departamento de Ciência de Computadores, Faculdade de Ciências da Universidade do Porto
Delia Kesner (Co-orientadora)
Full Professor
UFR d'Informatique, Université Paris Cité (França)
Resumo:
Os tipos de interseção não-idempotentes emergiram como um poderoso enquadramento lógico para fornecer semânticas quantitativas exatas de programas de ordem superior, permitindo que as derivações de tipagem captem informação precisa sobre o uso de recursos, como o comprimento da avaliação. Embora estas técnicas estejam atualmente bem compreendidas para o λ-cálculo puro, a sua extensão a funcionalidades linguísticas mais ricas que envolvem controlo e efeitos computacionais continua a ser um problema desafiante.
Esta tese desenvolve sistemas de tipos de interseção não-idempotentes para extensões do λ cálculo que incorporam mecanismos de pattern matching e efeitos computacionais, com o objetivo de fornecer semânticas de custo exatas, dirigidas pela sintaxe e fundamentadas na semântica operacional. As contribuições organizam-se em torno de dois eixos principais.
A primeira parte da tese estuda o pattern matching como uma extensão fundamental do λ cálculo. Com base em análises quantitativas prévias de cálculos com pattern matching, desenvolve mos sistemas de tipos de interseção não-idempotentes refinados e generalizados que preservam uma correspondência exata entre as derivações de tipagem e o comprimento da avaliação. É dada particular atenção ao tratamento de computações bloqueadas (stuck computations). Explorando a codificação clássica de exceções através de pattern matching, estendemos esta análise ao controlo excecional, mostrando que a propagação e o tratamento de exceções admitem semânticas quantitativas exatas, apesar de constituírem um efeito computacional não algébrico.
A segunda parte da tese aborda operações e efeitos algébricos. Concentramo-nos em teorias algébricas que admitem comodelos não triviais, os quais fornecem uma base coalgébrica para a definição de semânticas operacionais de granularidade fina através de sistemas de transição baseados em comodelos. Para cálculos com estado global, definimos tais semânticas operacionais e desenvolvemossistemasdetiposdeinterseçãonão-idempotentesquecontabilizamcomprecisão tanto os passos computacionais como os passos associados a efeitos. Em seguida, generalizamos esta abordagem modelando o estado como um mapeamento de localizações para pilhas infinitas, obtendo um enquadramento quantitativo uniforme capaz de capturar uma vasta classe de efeitos algébricos, incluindo estado global, input/output interativo e não-determinismo finito.
Ao longo datese, o λ!-cálculo desempenha um papel unificador, subsumindo as estratégias de avaliação call-by-name e call-by-value, ao mesmo tempo que preserva a granularidade operacional necessária para um raciocínio quantitativo exato. No seu conjunto, este trabalho alarga significativamente o âmbito dos tipos de interseção não-idempotentes, demonstrando a sua aplicabilidade a linguagens com pattern matching, exceções e efeitos algébricos, e fornecendo uma descrição operacional e quantitativa unificada da computação sensível a recursos.