Seminário de Lógica Matemática

Instantiation overflow from the viewpoint of categorical semantics and linear logic

Sala 6.2.33, FCUL, Lisboa

Por Paolo Pistone (Università Roma Tre).

Abstract: Instantiation overflow (IO for short), first investigated by Fernando Ferreira and Gilda Ferreira, is a property of some second order types for which full comprehension for any type can be derived from comprehension restricted to atomic types. In other words, for such an A, one can type, by predicative polymorphism, “expansion terms” which realize instances of impredicative comprehension over A (i.e. the principle ∀XA ⇒A[B/X]). By this property, the usual Russell-Prawitz translation of logical connectives into System F can be "atomized", yielding derivations in System Fat.

We show that the IO property can be investigated and generalized from two related viewpoints. First, from the viewpoint of the categorial semantics of System F, the "atomization" technique corresponds to applying some permutations of rules coming from the usual dinatural interpretation of System F. As a consequence, the Russell-Prawitz translation and the "atomized" translation in Fat are observationally equivalent and, in particular, equal in the well-known class of parametric models of System F. Second, by using linear logic proof net, the IO property can be related to a geometric property of linear types. By exploiting this property we recently obtained a characterization of the simple types enjoying IO, providing a (partial) solution to a problem posed by Gilda Ferreira and Bruno Dinis.

16h00
CMAF-CIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Título do programa, sobre mosaico de fotografias de jovens cientistas

As candidaturas encontram-se encerradas. Obrigada aos quase 80 candidatos/as!

Logótipo do EVM 2024

Por Pedro Duarte (DM Ciências ULisboa, CMAFcIO).

Seminário do Centro de Matemática, Aplicações Fundamentais e Investigação Operacional, por Baptiste Claustre (aluno ENS Lyon, estagiário CMAFcIO).

Fotografia de ilha

Seminários Doutorais no âmbito da disciplina de Projeto de Investigação (Doutoramento em Ciências do Mar).

Logótipo do EVM 2024

Por Maria Manuel Torres (DM Ciências ULisboa e CMAFcIO).

Titulo e data do evento, com imagem de ponte sobre o tejo

Um evento organizado no âmbito da Ação COST EURO-MIC, de cujo Comitê de Gestão Elisabete Silva, líder do Bioactive and Multifunctional Materials Lab do BioISI, faz parte.

Logótipo do EVM 2024

Por: Jorge Buescu (DM Ciências ULisboa e CMAFcIO).

Logótipo do EVM 2024

Por Jean-Baptiste Casteras (DM Ciências ULisboa e CMAFcIO).

Chegou a hora: os participantes do Programa Ser Cientista vão apresentar os projetos que desenvolveram ao longo de uma semana, acompanhados por docentes e investigadores de CIÊNCIAS. E todos podem assistir!

Imagem do evento

Extended enrolement date until July 12th.

Logótipo do evento, sobre um fundo branco

Um evento de reunião da comunidade nacional nas diversas vertentes da informática, com a ambição de ser o fórum de eleição para a divulgação, discussão e reconhecimento de trabalhos científicos.

Are you ready for this year's edition?

Imagem do evento - título, local e data do evento

Investigação Ecológica ao Serviço da Conservação

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