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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Agda Wiki. Chalmers and Gothenburg University, 2.4 edn. (2014), http://wiki.portal.chalmers.se/agda
Abel, A.: Normalization for the simply-typed lambda-calculus in Twelf. In: Logical Frameworks and Metalanguages (LFM 2004). Electronic Notes in Theoretical Computer Science, vol. 199C, pp. 3–16. Elsevier (2008)
Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: Programming infinite structures by observations. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, January 23-25, pp. 27–38. ACM Press (2013)
Abel, A., Vezzosi, A.: A formalized proof of strong normalization for guarded recursive types (long version and Agda sources) (August 2014), http://www.cse.chalmers.se/~abela/publications.html#aplas14
Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now! In: Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, pp. 57–68. ACM Press (2007)
Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 453–468. Springer, Heidelberg (1999)
Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: Proc. of the 18th ACM SIGPLAN Int. Conf. on Functional Programming, ICFP 2013, pp. 197–208. ACM Press (2013)
Benton, N., Hur, C.K., Kennedy, A., McBride, C.: Strongly typed term representations in Coq. Journal of Automated Reasoning 49(2), 141–159 (2012)
Birkedal, L., Møgelberg, R.E.: Intensional type theory with guarded recursive types qua fixed points on universes. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, pp. 213–222. IEEE Computer Society Press (2013)
Dybjer, P.: Inductive families. Formal Aspects of Computing 6(4), 440–465 (1994)
Joachimski, F., Matthes, R.: Short proofs of normalization. Archive of Mathematical Logic 42(1), 59–87 (2003)
Krishnaswami, N.R., Benton, N.: A semantic model for graphical user interfaces. In: Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, pp. 45–57. ACM Press (2011a)
Krishnaswami, N.R., Benton, N.: Ultrametric semantics of reactive programs. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, Toronto, Ontario, Canada, June 21-24, pp. 257–266. IEEE Computer Society Press (2011b)
McBride, C.: Type-preserving renaming and substitution, unpublished draft (2006), http://strictlypositive.org/ren-sub.pdf
McBride, C.: Let’s see how things unfold: Reconciling the infinite with the intensional (Extended abstract). In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 113–126. Springer, Heidelberg (2009)
McBride, C.: Outrageous but meaningful coincidences: Dependent type-safe syntax and evaluation. In: Proceedings of the ACM SIGPLAN Workshop on Generic Programming, WGP 2010, Baltimore, MD, USA, September 27-29, pp. 1–12. ACM Press (2010)
Nakano, H.: A modality for recursion. In: Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS 2000), Santa Barbara, California, USA, June 26-29, pp. 255–266. IEEE Computer Society Press (2000)
van Raamsdonk, F., Severi, P., Sørensen, M.H., Xi, H.: Perpetual reductions in lambda calculus. Information and Computation 149(2), 173–225 (1999)
Tait, W.W.: Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic 32(2), 198–212 (1967)
Univalent Foundations: Homotopy type theory: Univalent foundations of mathematics. Tech. rep. Institute for Advanced Study (2013), http://homotopytypetheory.org/book/
Xi, H., Chen, C., Chen, G.: Guarded recursive datatype constructors. In: Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages, New Orleans, pp. 224–235 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Abel, A., Vezzosi, A. (2014). A Formalized Proof of Strong Normalization for Guarded Recursive Types. In: Garrigue, J. (eds) Programming Languages and Systems. APLAS 2014. Lecture Notes in Computer Science, vol 8858. Springer, Cham. https://doi.org/10.1007/978-3-319-12736-1_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-12736-1_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-12735-4
Online ISBN: 978-3-319-12736-1
eBook Packages: Computer ScienceComputer Science (R0)