Talks@DI/LaSIGE

Typed Definitional Interpretation of a Communication-Based Concurrent Language

Sala 6.3.38, FCUL, Lisboa

Por Peter Thiemann.

Abstract: Dependently-typed definitional interpreters offer a convenient way to define a language together with its type system such that type soundness of the language is guaranteed by the typing of the interpreter. This approach has been pursued extensively for functional languages. Recent work has addressed imperative languages with first-class references and objects.
Session types have emerged as a powerful paradigm for structuring communication-based programs. Type soundness proofs for language with session types are tedious and technically involved. It is rare to see mechanized soundness proofs for these systems.
We show that typed definitional interpretation is applicable to a multi-threaded functional language with communication primitives governed by session types by implementing a suitably typed interpreter in Agda. This implementation also provides a fully mechanized and executable soundness proof for the underlying session-typed calculus.  

Short Bio: Peter Thiemann is a full professor of computer science at the University of Freiburg, Germany. His area of research is programming languages with an emphasis on functional programming, message-passing concurrency, and types. He has authored and co-authored more than 100 papers in this area. He served as a reviewer, pc member, pc chair, and general chair for various conferences including the flagship conference in this area, the ACM SIGPLAN International Conference on Functional Programming. He is an editor of the Journal of Functional Programming.  

14h00
Departamento de Informática / LaSIGE - Laboratório de Sistemas Informáticos de Grande Escala
Imagem estilizada do continente europeu, associada ao logótipo "European Strategy Update"

Uma reflexão centrada na recente atualização da Estratégia Europeia para a Física de Partículas pelo Conselho do CERN.

Logótipo UNITE! Dialogue Meeting, sobre uma imagem estilizada do globo

De 29 de setembro a 1 de outubro, irá decorrer a 2.ª UNITE! Dialogue Meeting, organizado pela Universidade de Lisboa. O evento será realizado em formato digital.

O principal objetivo desta iniciativa centra-se em atrair fotógrafos profissionais e amadores a submeter trabalhos de excelência produzidos em Portugal e nos países africanos de língua oficial portuguesa (PALOP) e fomentar práticas de observação, conhecimento e registo através

De onde vêm todos os compostos que te permitem estar a ver esta mensagem ou notícia no teu smartphone ou computador? Será possível montá-lo sem toda uma cadeia de impactes sociais e económicos?

Título e data do evento, acompanhados do logótipo do cE3c e de uma fotografia de um morcego

O evento realiza-se online, via Zoom, nas tardes dos dias 1 e 2 de outubro de 2020.

Formação sobre gestão da ansiedade - inscrições a decorrer!

As sessões são online e realizam-se nos dias 01, 22 e 29 de outubro, 05 e 12 de novembro.

Fotografia de Alunos de Ciências

A sessão de boas-vindas irá decorrer na sexta-feira, dia 09 de outubro, no Grande Auditório da Faculdade, localizado no edifício C3, piso 2. Contará com a presença de Luís Carriço, Diretor da Faculdade de Ciências da Universidade de Lisboa.

De onde vêm todos os compostos que te permitem estar a ver esta mensagem ou notícia no teu smartphone ou computador? Será possível montá-lo sem toda uma cadeia de impactes sociais e económicos?

O cE3c - Centro de Ecologia, Evolução e Alterações Ambientais está mais uma vez a organizar o Seminário cE3c I, que irá decorrer no 1.º semestre do ano letivo 2020/2021 na Faculdade de Ciências.

Ciências ULisboa associa-se ao maior evento mundial sobre inovação para a sustentabilidade - “The Planetiers World Gathering” - que terá lugar no Altice Arena entre 21 e 23 de outubro de 2020, sob os auspícios da

Fotografia de caminhantes numa montanha

Suspensão motivada pela aplicação do plano de contingência da Faculdade de Ciências da Universidade de Lisboa, na sequência das orientações da Direção-Geral de Saúde e das recomendações por parte da Reitoria da Universidade de Lisboa, relativamente ao novo Coronavírus (COVID

De onde vêm todos os compostos que te permitem estar a ver esta mensagem ou notícia no teu smartphone ou computador? Será possível montá-lo sem toda uma cadeia de impactes sociais e económicos?

Fotografia de ilha no Oceano Pacífico

A Direção-Geral de Política do Mar, na qualidade de operador do Programa Crescimento Azul do Mecanismo Financeiro do Espaço Económico Europeu 2014/2021 (EEA Grants), lançou recentemente o

Leitura e escrita são a base fundacional de todas as literacias e a condição primeira para o juízo compreensivo e crítico, o enriquecimento cultural, a formação estética e a memória individual e coletiva das sociedades.

Logótipo da IAESTE, sobre uma fotografia da cidade de Edimburgo

Interessado em realizar um estágio extracurricular a nível internacional?

Imagem ilustrativa do prémio (fotografia de rosto de um jovem, metade humana e metade "computorizada", acompanhada do título da iniciativa e do slogan "Um Milhão para a Inovação"

Novo prazo de candidatura a decorrer até ao dia 31 de outubro de 2020.

IN3+  | Um Milhão para a Inovação.

Objectives: Evolutionary theory provides a framework for understanding all living systems.

Overview: Currently, climate changes or alterations are known to be reflected on the stable isotope ratios of Hydrogen, Nitrogen, Carbon, Oxygen and Sulphur present in atmospheric gas forms, fresh or ocean water, as well as in plants and animals and organi

Objectives: To introduce participants to the details of communicating science to non-specialized audiences, including, but not exclusive to, public and private stakeholders, students and teachers, and media professionals.

De onde vêm todos os compostos que te permitem estar a ver esta mensagem ou notícia no teu smartphone ou computador? Será possível montá-lo sem toda uma cadeia de impactes sociais e económicos?

Objectives: Natural history museums are privileged spaces for seminal research on different subjects of biological sciences such as biodiversity, evolution, ecology, biogeography and taxonomy.

De onde vêm todos os compostos que te permitem estar a ver esta mensagem ou notícia no teu smartphone ou computador? Será possível montá-lo sem toda uma cadeia de impactes sociais e económicos?

Objectives: Provide students with basic workflows, platforms and tools to increase reproducibility at all scientific levels.

Objectives: Under the general framework of Global Change Ecology, the goal of this course is to provide the participants with the most recent and practical knowledge on the use of Functional Diversity.

Objectives: The objective of this course is to introduce participants to the details of communication and writing scientific publications. The main emphasis is on the most common form, the “primary scientific paper”, but other forms will be covered.

Páginas