RSS Meetup

Propositions-as-Types and Shared State

Sala 6.3.27, Ciências ULisboa
Título, data, orador e localização do evento

Por Pedro Rocha (NOVA LINCS, FCT/NOVA).

Modern software construction depends on imperative state, state sharing, and concurrency. Still, safely programming with state, aliasing and concurrency has always been considered a significant challenge. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. In this work, we develop a principled integration of shared mutable state into a propositions-as-types linear logic interpretation of a session-based concurrent programming language. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs. This is joint work with Luís Caires.

Bio: Pedro is a final-year PhD student, supervised by Luís Caires, in Computer Science at the NOVA School of Science and Technology / NOVA LINCS. Pedro got his Master in Electrical and Computer Engineering from Faculty of Engineering of University of Porto (FEUP). He won the prize Asea Brown Boveri, granted to the student with the highest rank dissertation of FEUP, and merit scholarships attributed during the years 2010-2012, granted to the top 12 students of the University of Porto. Before enrolling in the PhD program he worked for 2 years with Synopsys as an R&D engineer.

14h00
LASIGE
Astronauta, banhado pela luz solar, no meio de uma floresta

Candidaturas até 30 de julho - um evento único, que reunirá estudantes de mestrado e doutoramento com investigadores e líderes da indústria de toda a Europa para uma experiência inesquecível.

Lupa e caneta sobre página com texto e gráfico

O curso visa dar formação inicial a estudantes de pós-graduação sobre o processo de escrita, submissão e publicação de trabalhos científicos, focando principalmente a publicação de artigos científicos em revistas internacionais com revisão por pares.

Iconografia relacionada com a temática do curso

O curso fornece uma exploração aprofundada de isótopos estáveis como uma ferramenta valiosa em Ecologia, usando assinaturas isotópicas para rastrear processos ecológicos e revelando insights sobre o ciclo de nutrientes e água, interações de espécies e condições ambientais em diversos ecossistemas e comunidades.

Composição de três imagens relativas à área da deteção remota

2.ª edição do curso, com candidaturas até 18 de outubro.

O evento pretende reunir investigadores que trabalhem sobre temas ligados à indústria e sobre património técnico e industrial, para uma reflexão prospetiva sobre o património industrial e atuais vias de colaboração no seu estudo, salvaguarda e preservação.

Computador portátil a projetar imagem de sequência biológica

O curso visa a aquisição de conhecimentos sobre as ferramentas bioinformáticas disponíveis para efetuar análises de sequências de DNA e proteínas, bem como a autonomia e espírito crítico na utilização dessas ferramentas. Procura igualmente desenvolver competências na utilização de software de bioinformática disponível gratuitamente na Internet e na interpretação do significado biológico dos resultados.

Bola de cristal colocada no solo

O curso tem como objetivo apresentar aos participantes um estado da arte atualizado sobre a diversidade da biota do solo e os papéis funcionais desempenhados pelos organismos do solo nos principais processos ecológicos.

A conferência visa reunir os principais especialistas no domínio da Imagiologia Médica por Micro-ondas (MMWI) e incluirá palestras, apresentações e pósteres de resumos revistos por pares e artigos de conferências, bem como workshops em áreas satélite de investigação com interesse para a investigação em MMWI.

Páginas