PhD in Computer Science

Type Inference for Bimorphic Recursion

Academic year 2012/2013

Sommario del corso

• Program
• Notes
• Teaching tools

Program

This talk proposes bimorphic recursion, which is restricted

polymorphic recursion such that every recursive call in the body of a

function definition has the same type.  Bimorphic recursion allows us

to assign two different types to a recursively defined function: one

is for its recursive calls and the other is for its calls outside its

definition.  Bimorphic recursion in this talk can be nested.  This

talk shows bimorphic recursion has principal types and decidable type

inference.  Hence bimorphic recursion gives us flexible typing for

recursion with decidable type inference.  This talk also shows that

its typability becomes undecidable because of nesting of recursions

when one removes the instantiation property from the bimorphic

recursion. This ia a joint work with Ferruccio Damiani and was

presented at Second International Symposium on Games, Automata,

Logics, and Formal Verification (GandALF 2011).

Class schedule

Note

SEMINAR HELD BY:

Prof. Makoto Tatsuta

(National Institute of Informatics)

• Teaching materials
• Exams and finals
• Go to Moodle
• Visit the forums