Strong normalization for guarded types

Andreas Abel

Dept. of Computer Science and Engineering
Chalmers University of Technology

Thursday, 18 December 2014, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Abstract: We consider a simplified version of Nakano's guarded fixed-point types in a representation by infinite type expressions, defined coinductively. Small-step reduction is parametrized by a natural number "depth" that expresses under how many guards we may step during evaluation. We prove that reduction is strongly normalizing for any depth. The proof involves a typed inductive notion of strong normalization and a Kripke model of types in two dimensions: depth and typing context. Our results have been formalized in Agda and serve as a case study of reasoning about a language with coinductive type expressions.

(Joint work with Andrea Vezzosi, published in APLAS '14.)

ERDF
Tarmo Uustalu
Last update 15 December 2014