Copenhagen Programming Language Seminar


Definability of type constructors and logical connectives

Pawel Urzyczyn
Warsaw University

Monday, January 23, 11:15-12:00
DIKU, Universitetsparken 1, room N034


Certain operations are definable in type-free lambda-calculus, and polymorphic lambda-calculus, but not in simple types. Similarly, some logical constructions are possible in classical logic and higher-order, but not propositional, intuitionistic logic. These facts are often related via the Curry-Howard isomorphism. This talk will collect some observations concerning definablity of logical connectives and data types in various logics and lambda-calculi.

Scientific host: Fritz Henglein. Administrative host: Camilla Jensen. All are welcome. The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL. COPLAS is sponsored by FIRST Graduate School. To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.itu.dk with the word 'subscribe' as subject or in the body. For more information about COPLAS, see http://www.coplas.org.

Valid HTML 4.01 Transitional