{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:18Z","timestamp":1761611238036},"reference-count":11,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":5424,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1994,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present here a generalization of A-translation to a class of pure type systems. We apply this translation to give a direct proof of the existence of a looping combinator in a large class of inconsistent type systems, a class which includes type systems with a type of all types. This is the first non-automated solution to this problem.<\/jats:p>","DOI":"10.1017\/s0956796800000952","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T16:13:10Z","timestamp":1226074390000},"page":"77-88","source":"Crossref","is-referenced-by-count":25,"title":["A-translation and looping combinators in pure type systems"],"prefix":"10.1017","volume":"4","author":[{"given":"Thierry","family":"Coquand","sequence":"first","affiliation":[]},{"given":"Hugo","family":"Herbelin","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800000952_ref011","unstructured":"Paulin C. (1989) Extraction de programmes dans le Calcul des Constructions. Th\u00e9se de doctorat de l'universit\u00e9Paris 7."},{"key":"S0956796800000952_ref010","unstructured":"Murthy C. (1990) Extracting Constructive Content From Classical Proofs. PhD Thesis, Cornell University."},{"key":"S0956796800000952_ref008","doi-asserted-by":"publisher","DOI":"10.2307\/2274322"},{"key":"S0956796800000952_ref006","unstructured":"Howe D. J. (1987) The computational behaviour of Girard's paradox. In Proceedings Second Symposium of Logic in Computer Science, (Ithaca, NY),(IEEE Press), 205\u2013214."},{"key":"S0956796800000952_ref005","unstructured":"Girard J. Y. (1972) Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur. Th\u00e9se de doctorat d'\u00e9tat d'universit\u00e9 Paris 7."},{"key":"S0956796800000952_ref002","volume-title":"Proceedings 9th International Congress of Logic, Methodology and Philosophy of Science","author":"Coquand","year":"1991"},{"key":"S0956796800000952_ref009","unstructured":"Meyer A. R. and Reinhold M. B. (1986) \u201ctype\u201d is not a type. In Conference record Thirteenth Annual ACM Symposium on Principles of Programming Languages,ACM SIGACT, SIGPLAN, 287\u2013295."},{"key":"S0956796800000952_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0103100"},{"key":"S0956796800000952_ref001","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","article-title":"Introduction to Generalized Type System","volume":"1","author":"Barendregt","year":"1991","journal-title":"J. Functional Programming"},{"key":"S0956796800000952_ref007","volume-title":"From Frege to G\u00f6del: a source book in mathematical logic, 1879\u20131931","author":"Kolmogorov","year":"1967"},{"key":"S0956796800000952_ref004","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","article-title":"Modular proof of strong normalisation for the calculus of constructions","volume":"1","author":"Geuvers","year":"1991","journal-title":"J. Functional Programming"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800000952","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,10]],"date-time":"2020-05-10T00:10:05Z","timestamp":1589069405000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800000952\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,1]]},"references-count":11,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1994,1]]}},"alternative-id":["S0956796800000952"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800000952","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,1]]}}}