Mathematical Logic Webinar

The Yoneda Reduction of Polymorphic Types

(joint work with Paolo Pistone)

Transmissão através de Videoconferência

Por Luca Tranchini (University of Tubingen).

In this talk I will present a family of type isomorphisms in System F (i.e. second-order propositional intuitionistic logic) whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under notions of identity of proofs (or programs) stronger than the one induced by βη-equivalence, like those induced by parametricity and dinaturality. We show that the Yoneda type isomorphisms yield a rewriting over types (i.e. formulas), that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We establish some sufficient conditions under which quantifiers can be fully eliminated from a polymorphic type, and we show some application of these conditions to count the inhabitants of a type and to study proof/program equivalence in some fragments of System F.

This is a joint session with SAL (CMA/FCT-UNL).


Zoom | ID da reunião: 890 8479 3299 - senha de acesso: 409604 

16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Fotografia de árvores sem folhas e de bancos de jardim

Estudantes de pós-graduação em Matemática da Faculdade de Ciências da ULisboa falam, de forma descontraída e informal, sobre o seu trabalho.

Seminário Doutoral II (Doutoramento em Biologia), por Ana Sofia Lopes.

Fotografia de sinal identificativo de vinha

Apresentação de candidaturas até 28 de fevereiro.

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 Bruno Santos (Stockholm University, Sweden).

Seminário de Pós-graduação (Doutoramento em Biologia), por Diogo Roque.

Conferência do Centro Interuniversitário de História das Ciências e da Tecnologia, por Luís Campos Ribeiro (CIUHCT, Ciências ULisboa).

Iconografia representando um casal masculino/feminino e diversas áreas científicas

A maior feira de Mestrados e Pós-Graduações, agora também no Algarve.

Seminário do Laboratório de Instrumentação e Física Experimental de Partículas, por Carlota Andrés  (LIP).

Hi-Phi Seminar, por Ana Simões (CIUHCT/Ciências) e Ana Matilde Sousa (CIEBA/FBAUL).

Mathematical Logic Seminar, por Maria Osório Costa (CMAFcIO, Faculdade de Ciências da Universidade de Lisboa).

Título/data/local do evento, logótipo do projeto e fotografia da oradora

Seminário TWIN2PIPSA, por Sophie Jackson (Yusuf Hamied Department of Chemistry, University of Cambridge).

Título do evento, 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.

Theory of Computing Seminar, por Mateusz Skomra (LAAS/CNRS).

Seminário Conjunto CFCUL / Rede Ibérica de Filosofia das Ciências, por Saúl Pérez-González (Universidad de Valencia).

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

Colóquio de Matemática, por José Francisco Rodrigues (DM-Ciências ULisboa).

Pormenor de robô

Nesta sessão, serão descritos os funcionamentos dos vários mestrados, as suas estruturas curriculares, e os horizontes profissionais que oferecem.

CIUHCT Distinguished Lecture, por María M. Portuondo (Johns Hopkins University).

Título/data/local do evento e logótipos dos organizadores

O Departamento de Matemática e o Núcleo de Estudantes de Matemática e Matemática Aplicada associam-se às celebrações do Dia Internacional da Matemática.

Título/data do curso

Curso Avançado CEAUL / Gades Solutions.

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 Gustavo Soutinho (Faculdade de Economia da Universidade do Porto - FEP e Instituto Superior de Saúde Pública da Universidade do Porto - ISPUP).

Logótipo do Dia Internacional da Matemática, sobre um fundo branco

Atividades a decorrer em Ciências ULisboa nos dias 13 e 14 de março.

Seminário de Formação Avançada em Jardins, Paisagens e Ambiente, por Pier Luigi Pireddu (CIUHCT - ULisboa).

Seminário Helena Avelar de Astronomia e Astrologia Antiga, por Luís Tirapicos (Universidade de Lisboa).

Mão humana a interagir com um ecrã virtual

Novos prazos de submissão de candidaturas a projetos IC&DT e PeX.

Páginas