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

The course provides essential skills and knowledge that enable the participants to develop climate change adaptation strategies.

Título "Ciências, onde andas tu?", sobre um mapa

Esta é a pergunta que estamos a fazer a alumni de Ciências ULisboa. A resposta interessa-vos?

Seminário Permanente de Filosofia das Ciências, por Dimitris Bolis (CFCUL/GI2, Projeto INTERSELF).

Pormenor da Exposição "Formas & Fórmulas" (Ciências, out2016-mar2017)

Nesta sessão, serão descritos a nova estrutura do Programa Doutoral em Matemática, os cursos oferecidos em 2022/23 e alguns temas de tese propostos, entre outras informações.

Colóquio de Matemática, por Léonard Monsaingeon (Ciências ULisboa - GFM).

Título e data do evento, acompanhados de representações de espécies animais/vegetais e dos logótipos dos organizadores

No dia 26 de maio, a comunidade de Ciências, em conjunto com especialistas de diferentes grupos taxonómicos, inventaria e regista toda a biodiversidade que consiga observar.

The main purpose of this course is to present new recent developments in integrated nested Laplace approximation (INLA) that is a method for approximate Bayesian inference.

Um ciclo de entrevistas com o objetivo de conhecer melhor os docentes do Departamento de Matemática de Ciências ULisboa. Gracinda Gomes é a entrevistada.

Fotografia de elétrico e diversas informações sobre o evento

Evento no âmbito do Ciclo de Conferências "Conversas à 6.ª", promovido pela redeMOV da Universidade de Lisboa.

Logótipo da iniciativa e prazo de candidatura

Candidaturas de 16 a 27 de maio de 2022.

Imagem ilustrativa do evento e várias informações (título, orador, data)

Formação de Comunicação em Ciência(s), por Luís Morgado (Science Communication Office ITQB NOVA).

Ação de formação para docentes, por Sofia Sá.

The objective of this course is to provide participants with basic knowledge on a) the fundamental aspects of experimental design and b) workflows, platforms and tools to increase reproducibility at all scientific levels.

Fotografias do Estuário do Tejo

Concurso de fotografia no âmbito do projeto "MigraWebs: Migradores como modeladores ecológicos sazonais das comunidades e funções ecossistémicas de áreas costeiras temperadas e tropicais", com candidaturas de 18 de abril a 31 de maio de 2022.

Fotografia de bando de aves

O National Geographic Summit está finalmente de volta!

Título e data do evento, sobre uma fotografia de um elétrico

The course aims to provide a better understanding of how to use and customize NIMBLE's statistical algorithms.

Ação de formação para docentes, por Sofia Sá.

Pormenor de vida marinha

Seminários doutorais no âmbito do Doutoramento em Biologia de Ciências ULisboa.

Fotografia de documentos antigos

As perspetivas epistemológicas acerca do arquivo, entendido enquanto realidade mas também como metáfora, sofreram transformações assinaláveis nos últimos anos.

Título do evento e indicação dos oradores

Encontro de Comunicação de Ciência(s), por Diogo Veríssimo (Universidade de Oxford), Maria Vicente (Plataforma de Ciência Aberta) e Milene Matos (BioLiving; Município de Lousada).

Geometry Seminar, por Daniel Barlet (Institut Elie Cartan, Géométrie, Université de Lorraine, Nancy).

Luís Saraiva (Ciências ULisboa) é o coordenador nacional do Seminário Nacional de História da Matemática.

This is a mostly practical course offering an overview on different community ecology and macroecological methods and software. These will include all steps of a research project, from the optimal sampling of communities to process inference from large-scale patterns of taxon, phylogenetic and functional diversity.

Banner do evento

A Summer School dedicated to enhance skills on blue entrepreneurship, held just before the Lisbon United Nations Ocean Conference 2022.

Fotografia de documentos antigos

As perspetivas epistemológicas acerca do arquivo, entendido enquanto realidade mas também como metáfora, sofreram transformações assinaláveis nos últimos anos.

Páginas