Por Sebastián Buedo Fernández (University of Santiago de Compostela).

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

Por Fernando Ferreira (Universidade de Lisboa).

Por Alberto Bressan (Penn State University).

Por André Souto (Universidade de Lisboa).

Por Fernando Ferreira (Universidade de Lisboa).

Por Fátima Silva Leite (Universidade de Coimbra).

Por Clarence Protin (Independent Scholar).

Abstract: Pawel Urzyczyn has shown how to obtain a syntactic proof of the undecidability of type inhabitation for systems $F$ and $F_\omega$ by a reduction involving the codification of a certain undecidable $\forall,\rightarrow$- fragment of intutitionistic predicate calculus and the use of the Curry-Howard isomorphism. We show how this technique can be simplified and used to prove the undecidability of type inhabitation for atomic polymorphism.

Uma conversa com …

José Matos (Ordem dos Biólogos)
Fábio Chalub (Sociedade Portuguesa de Matemática)
Carlos Braumann (Sociedade Portuguesa de Estatística)

Moderação de José Francisco Rodrigues (Ciências ULisboa)

Por Andrei Zviagin (Voronezh State University, Russia).