Copenhagen Programming Language Seminar
that every recursive call in the body of the definition of a function
has the same type. Bimorphic recursion allows us to assign two
different types to a recursively defined function: one is for its
recursive calls in the body of its definition and the other is for its
calls outside its definition. Bimorphic recursion in this paper can
be nested. Bimorphic recursion gives us flexible typing for
recursion. This paper shows bimorphic recursion has principal types
and decidable type inference. This paper also shows its typability
becomes undecidable when one removes the instantiation property from
the bimorphic recursion.
Makoto Tatsuta holds bachelor's degrees in Law (1983) and Science (1985),
a Master's degree in Science (1987), and obtained his PhD in 1993, all
at the University of Tokyo.
He was assistant professor and associate professor at Tohoku
University from 1989 to
1996 and associate professor at Kyoto University from 1996 to 2001.
Since 2001 he is
professor at the National Institute of Informatics.
His interests are mainly in theoretical computer science and
mathematical logic and in
particular in type theory and constructive logic.
Host: Fritz Henglein, DIKU
Fritz Heinglein Administrative host:Renée Korver Michan.
All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to firstname.lastname@example.org with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org