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
Ciclo de Palestras do GAPsi "Como comunicar de forma mais eficaz?"

Entre 31 de outubro e 28 de novembro, o GAPsi vai organizar um ciclo de palestras, disponibilizando várias palestras com o objetivo de promover o desenvolvimento pessoal e de competências transversais ao nível da gestão do tempo, gestão da ansi

Aperfeiçoar a Relatividade de Einstein para explicar fenómenos extremos e mistérios do Universo, e conhecer o passado e as pessoas do museu de história natural da Escola Politécnica, serão os dois temas em conversa na sessão de novembro do PubhD de Lisboa.

Por Marco Aurélio Sanfins (DE-IME, Universidade Federal Fluminense).

Por Patricia Faísca (DF-FCUL).

60 Minutos de Ciência "Geoconservação em meio urbano: o que se fez e não se fez"

Dedicada ao património geológico e à sua conservação em meio urbano, recebemos o Professor Doutor Galopim de Carvalho, entusiasta divulgador das geociências e antigo diretor do MUHNAC-ULisboa, em mais uma sessão de 60 Minutos de Ci

Candidaturas abertas para Estágios Tecnológicos no CERN, ESA, ESO e EMBL

A FCT abriu os concursos para a atribuição de 20 bolsas destinadas à realização de estágios tecnológicos em quatro organizações científicas internacionais das quais Portugal é membro, nomeadamente a Organização

Por Tatsuya Miura (Max Planck Institute for Mathematics in the Sciences, Leipzig).

Por Jagoba Malumbres-Olarte (Post-Doc Researcher, cE3c group Island Biodiversity, Biogeography & Conservation).

The ICGI’2018 - International Conference on Graphics and Interaction will take place between 15 and 16 November 2018 at the Faculty of Sciences of the University of Lisbon, in Portugal, a joint organization between the Large-Scale Informatics Systems

Por Carlos Oliveira (Grupo de Física Matemática, Universidade de Lisboa).

Da vida e do futuro: comunicar ciência aos jovens em Portugal (sécs. XIX-XX)

Em Portugal, que visões do futuro e da vida foram transmitidas aos mais jovens quando se lhes falou de ciência? Que projetos de sociedade se esconderam nas representações de ciência que lhes foram apresentadas? Quem comunicou ciência aos mais jovens?

Projeto Empresarial 2019

Está aberto o período de pré-inscrições para a UC Projeto Empresarial, a ter lugar no 2.º semestre (Licenciaturas, Mestrados e Mestrados Integrados).

O MARE - Centro de Ciências do Mar e do Ambiente tem o prazer de convidar professores e educadores a conhecerem o seu programa educativo “O MARE vai à escola” 2018/2019, com atividades disponíveis para todos os graus de escolaridade.

Marte 2030 - Ciclo de conversas com os pés assentes em Marte

Por Rui Agostinho (IA/Faculdade de Ciências da Universidade de Lisboa) e Pedro Fevereiro (DBV/Faculdade de Ciências da Universidade de Lisboa e ITQB-NOVA).

Estágios Internacionais da IAESTE em 2019

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

A IAESTE oferece esta possibilidade - realizar um estágio remunerado numa empresa / centro de investigação, em ambiente de trabalho.

Por Cristina Sernadas (Instituto Superior Técnico, Universidade de Lisboa).

No âmbito do protocolo de cooperação estabelecido entre o Plano Nacional de Leitura (PNL2027) e o CEAUL - Centro de Estatística e Aplicações da Universidade de Lisboa em abril passado, irá realizar-se em breve a primeira sessão de divulgação sobre

1.º Encontro "A Universidade de Lisboa e o Património"

Sob a égide do Ano Europeu do Património Cultural, a Universidade de Lisboa não pode deixar de se associar às comemorações que se desenrolam por toda a Europa.

Por Afonso Pais de Sousa (Siemens Mobility).

Viticultura sustentável, um mito ou uma realidade emergente?

Por Fernando Ferreira (DM - FCUL).

“Se Gauss fosse vivo seria um hacker” (Peter Sarnak, Princeton).

Jorge Miguel Campilho Fragoso defende a dissertação "Estudo de equações e sistemas de equações elípticos não lineares com expoente crítico em IR2".

Constantino Pereira Caetano defende a dissertação "An application of extreme value theory in medical sciences".

Páginas