Dual Calculus with Inductive and Coinductive Types

Professor Makoto Tatsuta (National Institute of Informatics, Japan)

LOGIC AND COMPUTATION SEMINAR

DATE: 2012-02-28
TIME: 15:30:00 - 16:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.

ABSTRACT:
This talk gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this talk presents its involution for the new system and proves that it preserves both typing and reduction. The duality between inductive types and coinductive types is shown by the existence of the involution that maps an inductive type and a coinductive type to each other. The strong normalization in this system is also proved. First, strong normalization in second-order Dual Calculus is shown by translating it into second-order symmetric lambda calculus. Next, strong normalization in Dual Calculus with inductive and coinductive types is proved by translating it into second-order Dual Calculus. This is a joint work with Daisuke Kimura.

BIO:
Bachelors in Law in 1983 and Science in 1985, Master's in Science in 1987, and PhD in 1993 all in University of Tokyo. An assistant professor and an associate professor at Tohoku University from 1989 to 1996. An associate professor at Kyoto University from 1996 to 2001. A professor at National Institute of Informatics since 2001. Interested in theoretical computer science and mathematical logic, in particular, type theory and constructive logic.