Seminário de Lógica Matemática

Modal embeddings and calling paradigms

Sala 6.2.33, FCUL, Lisboa

Por José Carlos Espírito Santo (Centro de Matemática, Universidade do Minho).

Abstract: We study the computational interpretation of the two standard embeddings, usually named after Girard and Gödel, of intuitionistic logic into modal logic IS4, and show that the embeddings are translations between calling paradigms of functional programming. To this effect, the common target system of the embeddings can be taken to be the arguably simplest fragment of IS4, here recast as a very simple lambda-calculus equipped with an indeterminate lax monoidal comonad. As the source system we take respectively the call-by-name (cbn) and the call-by-value (cbv) lambda-calculus with simple types. Unlike cps translations, which translate cbn and cbv into each other, the modal embeddings unify cbn and cbv as call-by-box (cbb), a new paradigm identified in the target fragment of IS4. The technical justification of such unification is the standardization theorem for cbb, from which we extract the standardization theorems for cbn and cbv as corollaries, with the help of the properties of the modal embeddings. These results are both stronger and more abstract than those known of embeddings into linear logic.

(Joint work with Luís Pinto and Tarmo Uustalu)

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional

Seminário de Lógica Matemática, por Borja Sierra Miranda (University of Bern).

Seminário Doutoral I (Doutoramento em Biologia), por Sara Bento.

Roundtable by the 2nd year MSc students.

Seminário em Biologia Humana e Ambiente, por João Brandão (National Institute of Health Dr. Ricardo Jorge - INSA / Researcher at the Centre for Environmental and Marine Studies - CESAM_FCUL).

Seminário do Centro de Estatística e Aplicações da Universidade de Lisboa e do Centro de Matemática Computacional e Estocástica, por Miguel Pereira (Cogitars, UK).

Geometry and Physics Seminar, por Pedro M. Silva (CMAFcIO).

Título do evento, logótipos da ULisboa/DGES e fotografia de peças de xadrez

Sentes-te perdido/a em relação ao teu futuro académico/profissional? Ainda não sabes qual a melhor área a seguir ou como definir a tua carreira? Este workshop é para ti!

Logótipos de Ciências ULisboa/GAPsi e calendarização das palestras

Uma conversa sobre ti, alguém amigo ou apenas acerca de ansiedade.

Logótipo do concurso

As candidaturas à 21.ª edição decorrem até 06 de dezembro.

Data Science Seminar, por Ana Filipa Rodrigues (LASIGE).

Título da iniciativa, logótipos das entidades envolvidas e fotografias de dois jovens

Voa alto com o teu talento no Talent Bootcamp em CIÊNCIAS.

Título/data/local do evento e fotografia de cantor

Concerto pelo Duo de canto e piano, no âmbito da Temporada Darcos, e que integra o programa Música na Universidade de Lisboa.

Logótipo do evento, sobre um fundo cor-de-rosa

Marcam presença neste concerto a Orquestra Sinfónica Juvenil, o Coro da Universidade de Lisboa (CUL) e o Coro do Instituto Gregoriano de Lisboa, com Direção de Christopher Bochmann.

Seminário Doutoral III (Doutoramento em Biologia), por Susana Martins.

Título do programa, fotografia de dois jovens e logótipo da Rede Alumni CIÊNCIAS

As candidaturas estão abertas até dia 09 de dezembro.

Título/data/local do evento e fotografia de autocarro

Evento no âmbito do Ciclo de Conferências "Conversas à Terça", promovido pela redeMOV da Universidade de Lisboa.

Seminário do Centro de Estatística e Aplicações da Universidade de Lisboa e do Centro de Matemática Computacional e Estocástica, por Joaquin Cavieres (University of Gӧttingen, Germany).

Fotografia do Professor Pedro Miranda

Lição de Jubilação "Wind and water: on-going research on climate processes".

Uma iniciativa dedicada a sensibilizar toda a sociedade, em especial os jovens, para os desafios climáticos que enfrentamos e para o papel crucial que podem desempenhar na construção de um futuro sustentável. 

Título/data/local do evento e fotografia de António Sampaio da Nóvoa

A sessão será presidida por Sua Excelência O Presidente da República, Marcelo Rebelo de Sousa.

Conversas sobre a geologia rica e fascinante do Parque Natural Sintra-Cascais, com a participação de vários docentes de CIÊNCIAS.

Título "5th edition ULisses", sobre fotografia do mar

Apresentação de candidaturas até 15 de dezembro.

Um dia para aprender sobre produção caseira de cogumelos, da teoria à prática! Cada participante leva consigo um kit de cogumelos produzido nesta tarde e ainda todo o conhecimento para o fazer novamente de forma autónoma!

titulo e data do evento

TWIN2PIPSA Seminar, por Ana Vila Verde (University of Duisburg-Essen).

Páginas