Seminário de Lógica Matemática

On the unification of functional interpretations

Sala 6.2.33, FCUL, Lisboa

Por Bruno Dinis (FCUL e CMAFcIO, Universidade de Lisboa).

Abstract: Since Godel published his functional (“Dialectica") interpretation in 1958, various other functional interpretations have been proposed. These include Kreisel's modified realizability, the Diller-Nahm variant of the Dialectica interpretation, Stein's family of interpretations, and more recently, the bounded functional interpretation, the bounded modified realizability, and "Herbrandized" versions of modified realizability and the Dialectica. It is then natural to ask how are these different interpretations related to each other and what is the common structure behind all of them. These questions were addressed by Paulo Oliva and various co-authors in the "unification programme". Starting with a unification of interpretations of intuitionistic logic, which was followed by various analysis of functional interpretations within the finer setting of linear logic, a proposal on how functional interpretations could actually be combined in so-called hybrid functional interpretations, and the inclusion of truth variants in the unification. This unification programme has so far been unable to capture the two more recent families of functional interpretations, namely the bounded functional interpretations, and the Herbrandized functional interpretations.

In this talk I will present a more general framework for unifying functional interpretations, based on two families of parameters, one for interpreting the contraction axiom, and another for interpreting typed quantifications, which allow to include in the unification the more recent bounded and Herbrandized functional interpretations. I will start by presenting this parametrised interpretation in the setting of affine logic. Then, via the two well-known Girard translations from intuitionistic logic into affine logic, one obtains two parametrised interpretations of intuitionistic logic. I will explain how all of the functional interpretations mentioned above can be recovered by suitable choices of these two parameters and how this framework can be used to discover some new interpretations.

(This is joint work with Paulo Oliva).

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Título "European Strategy Discussion" e mapa estilizado da Europa

O encontro visa promover o diálogo entre investigadores e consolidar ideias para a contribuição nacional - uma oportunidade única para alinhar as prioridades científicas de Portugal com a estratégia europeia, discutir os desafios da área e reforçar a colaboração entre investigadores.

Seminário de Lógica Matemática, por Luís Pereira (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 Milan Stehlík (Institute of Statistics, Universidad de Valparaíso, Valparaíso, Chile).

Representação antiga da cidade de Lisboa

Evoluir Juntos para Co-Criar o Futuro de Lisboa e Inspirar Portugal.

Sessão com a participação de membros de CIÊNCIAS.

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

Concerto pelo Coro de Câmara da Universidade de Lisboa (CCUL) da Associação Coral da Universidade de Lisboa (ACUL), e que integra a iniciativa Música na Universidade de Lisboa.

O evento, que conta com a participação do CIUHCT, terá a participação, entre outros, do matemático e historiador da matemática Professor Robin Wilson (Reino Unido) e do criador do primeiro museu de ciência dedicado inteiramente à matemática, Professor Albrecht Beutelspacher (Alemanha).

Minicurso por Pedro M. Silva (Pós-doc - CEMS.UL).

Dois estudantes em frente a um computador

Uma iniciativa integrada no Projeto de Promoção de Sucesso e Redução de Abandono no Ensino Superior, com inscrições até 25 de janeiro.

Logótipo da ULisboa, título/data/local do evento e fotografia de professora e estudantes numa biblioteca

Workshop no âmbito do Programa de Promoção da Saúde Mental e do Bem-Estar na ULisboa.

Título/data/local do evento e fotografia de Vítor Cardoso

Prémio atribuído a Vítor Cardoso, Professor Catedrático no Departamento de Física do Instituto Superior Técnico da Universidade de Lisboa e Diretor do Centro de Gravidade do Instituto Niels Bohr da Universidade de Copenhaga, Dinamarca.

Título do curso e logótipo do CEAUL

Aprenda a organizar e analisar dados com foco na obtenção de soluções orientadas para a resolução de problemas.

Data/título do evento/frase "(Re)começa agora. É a tua vez!", sobre fotografia de balões de ar quente

(Re)começa agora. É a tua vez!

Com o Inverno já a deixar a sua marca nos ramos nus das árvores, é tempo também de as ajudarmos a crescer na Primavera que se seguirá!

Logótipos CIÊNCIAS/CEAUL, indicação do título/data/orador e representação do cérebro humano

Participants will be introduced to using R in real life situations. From the start, this hands-on practical workshop will focus on following good programming and data analysis practices. 

Ação de formação para docentes e investigadores de CIÊNCIAS.

Fotografia de João Paulo Dias

A Celebration of his 80th Birthday - registration until 24 January.

Título e datas de candidaturas aos prémios, sobre uma imagem abstrata

Candidaturas abertas até 14 de fevereiro - em 2025, serão atribuídos 26 Prémios e 52 Menções Honrosas.

Banner do Dia do DEGGE 2025.

Um evento dedicado às três áreas de estudo do Dia do Departamento de Engenharia Geográfica, Geofísica e Energia: Engenharia da Energia e Ambiente; Meteorologia, Oceanografia e Geofísica; Engenharia Geoespacial.

Título "Bolsas de Doutoramento Unite! ULisboa", logótipos das entidades promotoras e fotografia de jovem investigadora a utilizar um laptop na esplanada de um café

O 4.º concurso decorre até 28 de fevereiro.

Composição de imagens relativas à área das ciências forenses

O curso visa disponibilizar aos profissionais com formação universitária inicial ao nível da licenciatura os conhecimentos básicos e a informação necessária ao eventual futuro ingresso e exercício de funções em áreas Médico-Legais e Forenses - candidaturas até 05 de fevereiro.

Reitoria da ULisboa

O ato eleitoral decorrerá nos dias 31 de março e 01 de abril de 2025.

O maior evento de empregabilidade de CIÊNCIAS, a decorrer nos dias 08 e 09 de abril.

A leading venue for presenting and discussing the latest research, industrial practice and innovations in dependable and secure computing.

Um concurso de programação dirigido aos alunos do ensino secundário (11.º e 12.º anos), que visa promover a prática e o gosto pela programação.

Páginas