{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:32Z","timestamp":1753889792219,"version":"3.41.2"},"reference-count":22,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T00:00:00Z","timestamp":1128470400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We consider the untyped lambda calculus with constructors and recursively defined constants. We construct a domain-theoretic model such that any term not denoting bottom is strongly normalising provided all its `stratified approximations' are. From this we derive a general normalisation theorem for applied typed lambda-calculi: If all constants have a total value, then all typeable terms are strongly normalising. We apply this result to extensions of G\\\"odel's system T and system F extended by various forms of bar recursion for which strong normalisation was hitherto unknown.<\/jats:p>","DOI":"10.2168\/lmcs-1(2:3)2005","type":"journal-article","created":{"date-parts":[[2006,11,23]],"date-time":"2006-11-23T09:21:08Z","timestamp":1164273668000},"source":"Crossref","is-referenced-by-count":5,"title":["Strong normalisation for applied lambda calculi"],"prefix":"10.46298","volume":"Volume 1, Issue 2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7677-3582","authenticated-orcid":false,"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2005,10,5]]},"reference":[{"key":"10.2168\/LMCS-1(2:3)2005_AbramskyJung94","doi-asserted-by":"crossref","unstructured":"S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors,Handbook of Logic in Computer Science, volume 3, pages 1-168. Clarendon Press, 1994.","DOI":"10.1093\/oso\/9780198537625.003.0001"},{"key":"10.2168\/LMCS-1(2:3)2005_Altenkirch93b","unstructured":"T. Altenkirch.Constructions, Inductive Types and Strong Normalization. PhD thesis, The University of Edinburgh, Department of Computer Science, Edinburgh, 1993."},{"key":"10.2168\/LMCS-1(2:3)2005_Barendregt92","unstructured":"H. Barendregt. Lambda calculi with types. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors,Handbook of Logic in Computer Science, volume 2, pages 117-309. Clarendon Press, Oxford, 1992."},{"key":"10.2168\/LMCS-1(2:3)2005_Berardi98","doi-asserted-by":"publisher","DOI":"10.2307\/2586854"},{"key":"10.2168\/LMCS-1(2:3)2005_Berger04","doi-asserted-by":"crossref","unstructured":"U. Berger. A computational interpretation of open induction. In F. Titsworth, editor,Proceedings of the Ninetenth Annual IEEE Symposium on Logic in Computer Science, pages 326-334. IEEE Computer Society, 2004.","DOI":"10.1109\/LICS.2004.1319627"},{"key":"10.2168\/LMCS-1(2:3)2005_Berger0x","first-page":"175","volume":"25","author":"U. Berger","year":"1985","journal-title":"Strong normalization of barrecursive terms without using infinite terms. \\newblock Archive for Mathematical Logic"},{"key":"10.2168\/LMCS-1(2:3)2005_BlanquiJouannaudOkada99","doi-asserted-by":"crossref","unstructured":"F. Blanqui, J-P. Jouannaud, and M. Okada. The calculus of algebraic constructions. In P. Narendran and M. Rusinowitch, editors,Proceedings of RTA'99, number 1631 in LNCS, pages 301-316. Springer Verlag, Berlin, Heidelberg, New York, 1999.","DOI":"10.1007\/3-540-48685-2_25"},{"key":"10.2168\/LMCS-1(2:3)2005_BergerOliva0x","doi-asserted-by":"crossref","unstructured":"U. Berger and P. Oliva. Modified bar recursion and classical dependent choice. InLogic Colloquium 2001. Springer, 2005.","DOI":"10.1201\/9781439865736-3"},{"key":"10.2168\/LMCS-1(2:3)2005_Cook93","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90044-E"},{"key":"10.2168\/LMCS-1(2:3)2005_Constable86","unstructured":"R.L. Constable et al.Implementing Mathematics with the NuprlProof Development System. Prentice-Hall, New Jersey, 1986."},{"key":"10.2168\/LMCS-1(2:3)2005_Girard71","doi-asserted-by":"crossref","unstructured":"J-Y. Girard. Une extension de l'interpr\u00e9tation de G\u00f6del \u00e0 l'analyse, et son application \u00e0 l'\u00e9limination des coupures dans l'analyse et la th\u00e9orie des types. In J.E. Fenstad, editor,Proceedings of the Second {Scandinavian Logic Symposium}, pages 63-92. North-Holland, Amsterdam, 1971.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"10.2168\/LMCS-1(2:3)2005_Griffor93","doi-asserted-by":"crossref","unstructured":"E. Griffor, I. Lindstr\u00f6m, and V. Stoltenberg-Hansen.Mathematical theory of domains. Cambridge University Press, 1993.","DOI":"10.1017\/CBO9781139166386"},{"key":"10.2168\/LMCS-1(2:3)2005_Godel58","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"10.2168\/LMCS-1(2:3)2005_Nash-Williams63","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100003844"},{"key":"10.2168\/LMCS-1(2:3)2005_Plotkin77","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","volume":"5","author":"G.D. Plotkin","year":"1977","journal-title":"Theore\\-ti\\-cal Computer Science"},{"key":"10.2168\/LMCS-1(2:3)2005_Paulin-Mohring93","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116"},{"key":"10.2168\/LMCS-1(2:3)2005_Spector62","doi-asserted-by":"crossref","unstructured":"C. Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In F. D. E. Dekker, editor,Recursive Function Theory: Proc. Symposia in Pure Mathematics, volume 5, pages 1-27. American Mathematical Society, Providence, Rhode Island, 1962.","DOI":"10.1090\/pspum\/005\/0154801"},{"key":"10.2168\/LMCS-1(2:3)2005_Tait71","doi-asserted-by":"crossref","unstructured":"W.W. Tait. Normal form theorem for barrecursive functions of finite type. In J.E. Fenstad, editor,Proceedings of the Second {Scandinavian Logic Symposium}, pages 353-367. North-Holland, Amsterdam, 1971.","DOI":"10.1016\/S0049-237X(08)70853-X"},{"key":"10.2168\/LMCS-1(2:3)2005_Tait75","doi-asserted-by":"crossref","unstructured":"W.W. Tait. A realizability interpretation of the theory of species. In R. Parikh, editor,Logic Colloquium Boston 1971\/72, volume 453 ofLecture Notes in Mathematics, pages 240-251. Springer Verlag, Berlin, Heidelberg, New York, 1975.","DOI":"10.1007\/BFb0064875"},{"key":"10.2168\/LMCS-1(2:3)2005_Troelstra73","doi-asserted-by":"crossref","unstructured":"A.S. Troelstra.Metamathematical Investigation of Intuitionistic {Arithmetic and Analysis}, volume 344 ofLecture Notes in Mathematics. Springer, 1973.","DOI":"10.1007\/BFb0066739"},{"key":"10.2168\/LMCS-1(2:3)2005_PolSchwichtenberg95","doi-asserted-by":"crossref","unstructured":"J. van de Pol and H. Schwichtenberg. Strict functionals for termination proofs. In M. Dezani-Ciancaglini and G. Plotkin, editors,Typed Lambda Calculi and Applications, volume 902 ofLNCS, pages 350-364. Springer Verlag, Berlin, Heidelberg, New York, 1995.","DOI":"10.1007\/BFb0014064"},{"key":"10.2168\/LMCS-1(2:3)2005_Vogel76","doi-asserted-by":"publisher","DOI":"10.1007\/BF02007260"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2267\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2267\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,8]],"date-time":"2024-02-08T12:40:32Z","timestamp":1707396032000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2267"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10,5]]},"references-count":22,"URL":"https:\/\/doi.org\/10.2168\/lmcs-1(2:3)2005","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0507007","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0507007","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2005,10,5]]},"article-number":"2267"}}