To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

A formalized proof of str… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

A formalized proof of strong normalization for guarded recursive types

Conference paper
Authors Andreas Abel
Andrea Vezzosi
Published in Lecture Notes in Computer Science: 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 Singapore, 17-19 November 2014
Volume 8858
Pages 140-158
ISBN 978-3-319-12735-4
ISSN 0302-9743
Publication year 2014
Published at Department of Computer Science and Engineering (GU)
Pages 140-158
Language en
Subject categories Computer and Information Science


We consider a simplified version of Nakano’s guarded fixed-point types in a representation by infinite type expressions, defined coinductively. Smallstep 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.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?