Copenhagen Programming Language Seminar

Type Inference for Bimorphic Recursion

Makoto Tatsuta
National Institute of Informatics, Tokyo, Japan

Date/time: August 27, 2010 / 14:15 - 15:00
Location: DIKU, Universitetsparken 1, Meeting room A+B

Bimorphic recursion is restricted polymorphic recursion such
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

Scientific host: 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 prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org