Sala 6.2.33, FCUL, Lisboa
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.
16h00
CMAFcIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
