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
Logótipos Ciências ULisboa e C-Academy, títulos dos cursos

Um programa de formação avançada em Cibersegurança para a administração pública e o setor privado desenvolvido pelo Centro Nacional de Cibersegurança, no âmbito do Plano de Recuperação e Resiliência.

Logótipos Ciências ULisboa e C-Academy, títulos dos cursos

Um programa de formação avançada em Cibersegurança para a administração pública e o setor privado desenvolvido pelo Centro Nacional de Cibersegurança, no âmbito do Plano de Recuperação e Resiliência.

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.

Imagem do evento

Extended enrolement date until July 12th.

Logótipo do Workshop

A participação na 3.ª edição do Workshop é gratuita, mediante inscrição prévia.

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.