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
Sitemap
To content Read more about how we use cookies on gu.se

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
Links dx.doi.org/10.1007/978-3-319-12736-...
Subject categories Computer and Information Science

Abstract

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
Share:

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?