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
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!

Seminário do Laboratório de Instrumentação e Física Experimental de Partículas, por António Gomes (LIP).

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á!

Aumente o envolvimento e a colaboração dos alunos com uma solução de ensino e aprendizagem completa dentro do Moodle através do FeedbackFruits.

Título "Quem são as mulheres do LIP na experiência ATLAS do CERN? - um encontro de gerações"

Um encontro que homenageia as várias gerações de mulheres do grupo do LIP que participam na experiência ATLAS, no colisionador LHC do CERN. Este evento celebra décadas de liderança e contributos femininos num dos maiores projetos científicos do mundo.

Título/data/local do evento e logótipos das entidades organizadoras

Inscrições até 07 de fevereiro.

Título/data/local do evento e fotografia de cruzamento bastante movimentado

Conferência da redeMOV, por Ana Rita Martins (IST-ULisboa).

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.

Sessão comemorativa, a realizar na ocasião da colocação do retrato do Professor João Guerreiro no Grande Auditório, bem como de um póster a ele relativo no átrio do edifício C3.

Seminários por Daniel Sequeira e Emily Croasdale.

António Cruz Serra

A cerimónia decorre no Pavilhão de Portugal, pelas 17h00.

Logótipo do projeto

Formação no âmbito da 22.ª edição do projeto "Observar e Aprender", com inscrições até 10 de fevereiro.

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.

Fotografia de João Paulo Dias

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

Fotografia de Carlos Paredes

Concerto no âmbito do programa Música na Universidade de Lisboa.

Composição do logótipo da ULisboa e de representação do rosto humano à base de relógios

Consegue comunicar eficazmente a sua investigação de doutoramento em 3 minutos?

Título do curso, sobre uma fotografia do Large Hadron Collider

The objective of the course is to introduce the physics, analysis methods and results on the physics areas covered by the LHC experiments.

A reunião, aberta a toda a comunidade estudantil, tem como objetivo esclarecer os mecanismos processuais de formalização de todas as realidades associativas existentes, a potencial criação de novas e a implementação e funcionamento futuros do FAC

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/data/local do evento e fotografia de vegetais

Workshop hands-on, dirigido a todos os estudantes da ULisboa.

Pormenor de pessoa sentada a ler um livro

Maiores de 50 anos - Candidaturas até 14 de fevereiro.

Se queres saber mais informações sobre os cursos de CIÊNCIAS, não deixes de participar!

Título "Bolsas Alumni Solidárias" e fotografia de grupo de alunos

As candidaturas decorrem de 03 a 28 de fevereiro.

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.

Páginas