ROSAEC center Seoul National University

Seminars & Workshops

Speaker:Makoto Tatsuta , NII
When:2012-03-29 15:00
Place:Room 309, Bldg 302, SNU


This talk answers the open problem of finding a type system that characterizes hereditary permutators. First this talk shows that there does not exist such a type system by showing that the set of hereditary permutators is not recursively enumerable. The set of positive primitive recursive functions is used to prove it. Secondly this talk gives a best-possible solution by providing a countably infinite set of types such that a term has every type in the set if and only if the term is a hereditary permutator. By the same technique for the first claim, this talk also shows that a set of normalizing terms in infinite lambda-calculus is not recursively enumerable if it contains some term having a computable infinite path, and shows the set of streams is not recursively enumerable. This work was presented at LICS 2008.

Short bio

2001--present Professor, National Institute of Informatics 1996--2001 Associate Professor, University of Tokyo 1994--1996 Associate Professor, Tohoku University 1989--1994 Research Associate, Tohoku University 1993 Ph.D in Science, University of Tokyo 1987 Master's in Science, University of Tokyo 1985 Bachelor n Science, University of Tokyo 1983 Bachelor in Law, University of Tokyo


© Copyright 2008-2010 ROSAEC Center, Seoul National University