{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T04:10:09Z","timestamp":1746418209006,"version":"3.40.4"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319127354"},{"type":"electronic","value":"9783319127361"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-12736-1_8","type":"book-chapter","created":{"date-parts":[[2014,10,13]],"date-time":"2014-10-13T14:53:24Z","timestamp":1413212004000},"page":"140-158","source":"Crossref","is-referenced-by-count":6,"title":["A Formalized Proof of Strong Normalization for Guarded Recursive Types"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Vezzosi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Agda Wiki. Chalmers and Gothenburg University, 2.4 edn. (2014), http:\/\/wiki.portal.chalmers.se\/agda"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"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.\u00a0199C, pp. 3\u201316. Elsevier (2008)","DOI":"10.1016\/j.entcs.2007.11.009"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"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\u201338. ACM Press (2013)","DOI":"10.1145\/2480359.2429075"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"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","DOI":"10.1007\/978-3-319-12736-1_8"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"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\u201368. ACM Press (2007)","DOI":"10.1145\/1292597.1292608"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/3-540-48168-0_32","volume-title":"Computer Science Logic","author":"T. Altenkirch","year":"1999","unstructured":"Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 453\u2013468. Springer, Heidelberg (1999)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"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\u2013208. ACM Press (2013)","DOI":"10.1145\/2544174.2500597"},{"issue":"2","key":"8_CR8","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/s10817-011-9219-0","volume":"49","author":"N. Benton","year":"2012","unstructured":"Benton, N., Hur, C.K., Kennedy, A., McBride, C.: Strongly typed term representations in Coq. Journal of Automated Reasoning\u00a049(2), 141\u2013159 (2012)","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Birkedal, L., M\u00f8gelberg, 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\u2013222. IEEE Computer Society Press (2013)","DOI":"10.1109\/LICS.2013.27"},{"issue":"4","key":"8_CR10","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/BF01211308","volume":"6","author":"P. Dybjer","year":"1994","unstructured":"Dybjer, P.: Inductive families. Formal Aspects of Computing\u00a06(4), 440\u2013465 (1994)","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"8_CR11","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/s00153-002-0156-9","volume":"42","author":"F. Joachimski","year":"2003","unstructured":"Joachimski, F., Matthes, R.: Short proofs of normalization. Archive of Mathematical Logic\u00a042(1), 59\u201387 (2003)","journal-title":"Archive of Mathematical Logic"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"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\u201357. ACM Press (2011a)","DOI":"10.1145\/2034773.2034782"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"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\u2013266. IEEE Computer Society Press (2011b)","DOI":"10.1109\/LICS.2011.38"},{"key":"8_CR14","unstructured":"McBride, C.: Type-preserving renaming and substitution, unpublished draft (2006), http:\/\/strictlypositive.org\/ren-sub.pdf"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-642-03741-2_9","volume-title":"Algebra and Coalgebra in Computer Science","author":"C. McBride","year":"2009","unstructured":"McBride, C.: Let\u2019s see how things unfold: Reconciling the infinite with the intensional (Extended abstract). In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 113\u2013126. Springer, Heidelberg (2009)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"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\u201312. ACM Press (2010)","DOI":"10.1145\/1863495.1863497"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"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\u2013266. IEEE Computer Society Press (2000)","DOI":"10.1109\/LICS.2000.855774"},{"issue":"2","key":"8_CR18","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1006\/inco.1998.2750","volume":"149","author":"F. Raamsdonk van","year":"1999","unstructured":"van Raamsdonk, F., Severi, P., S\u00f8rensen, M.H., Xi, H.: Perpetual reductions in lambda calculus. Information and Computation\u00a0149(2), 173\u2013225 (1999)","journal-title":"Information and Computation"},{"issue":"2","key":"8_CR19","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","volume":"32","author":"W.W. Tait","year":"1967","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic\u00a032(2), 198\u2013212 (1967)","journal-title":"The Journal of Symbolic Logic"},{"key":"8_CR20","unstructured":"Univalent Foundations: Homotopy type theory: Univalent foundations of mathematics. Tech. rep. Institute for Advanced Study (2013), http:\/\/homotopytypetheory.org\/book\/"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"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\u2013235 (2003)","DOI":"10.1145\/640128.604150"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-12736-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T03:47:35Z","timestamp":1746416855000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-12736-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319127354","9783319127361"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-12736-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}