Projeto e prototipação de uma variação do cálculo-lambda com tipos de sessão

Abstract

Os tipos de sessão são uma extensão de linguagens de programação que permite verificar, em nível de sistema de tipos, se uma comunicação por troca de mensagens entre pro cessos concorrentes respeita um determinado protocolo. São inspirados na lógica linear e surgiram no contexto do cálculo-π (um cálculo de processos), sendo posteriormente incor porados em variantes do cálculo-λ. Recentemente, tipos de sessão estão sendo integrados em linguagens de programação convencionais como Java, Haskell e outras. O objetivo deste trabalho é explorar a teoria de tipos de sessão e sua aplicação à programa ção através do projeto, especificação formal e prototipação de uma variante do cálculo-λ estendida com tipos de sessão e operações para programação concorrente. Através desse cálculo, serão apresentados exemplos de uso e idiomas aplicáveis a linguagens de progra mação que tenham tais extensões.

Session types are a programming language extension that allows to check, at type system level, if a message-passing communication between concurrent processes conforms to some given protocol. They take inspiration from linear logic and have emerged in the context of π-calculus (a process calculus), being later embedded in variants of λ-calculus. Recently, session types are being integrated in mainstream programming languages such as Java, Haskell and others. This work aims to explore the theory of session types and their application to program ming through the design, formal specification and prototyping of a variant of λ-calculus extended with session types and operations for concurrent programming. Using this cal culus, this work will present examples of use and idioms applicable to programming lan guages that have such extensions