{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,12]],"date-time":"2024-06-12T10:10:14Z","timestamp":1718187014973},"reference-count":32,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2015,11,9]],"date-time":"2015-11-09T00:00:00Z","timestamp":1447027200000},"content-version":"unspecified","delay-in-days":312,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2015]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce a new formulation of pure type systems (PTSs) with explicit substitution and de Bruijn indices and formally prove some of its meta-theory. Using techniques based on Normalisation by Evaluation, we prove that untyped conversion can be typed for predicative PTSs. Although this equivalence was settled by Siles and Herbelin for the conventional presentation of PTSs, we strongly conjecture that our proof method can also be applied to PTSs with \u03b7.<\/jats:p>","DOI":"10.1017\/s0956796815000210","type":"journal-article","created":{"date-parts":[[2015,11,9]],"date-time":"2015-11-09T10:06:30Z","timestamp":1447063590000},"source":"Crossref","is-referenced-by-count":1,"title":["Pure type systems with explicit substitutions"],"prefix":"10.1017","volume":"25","author":[{"given":"DANIEL","family":"FRIDLENDER","sequence":"first","affiliation":[]},{"given":"MIGUEL","family":"PAGANO","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,11,9]]},"reference":[{"key":"S0956796815000210_ref32","unstructured":"Streicher T. (1989) Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions. Ph.D. thesis, Universit\u00e4t Passau, Passau, West Germany."},{"key":"S0956796815000210_ref31","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000044"},{"key":"S0956796815000210_ref30","first-page":"21","volume-title":"Lics","author":"Siles","year":"2010"},{"key":"S0956796815000210_ref29","unstructured":"Siles V. (2010) Investigation on the Typing of Equality in Type Systems. Ph.D. thesis, \u00c9cole Polytechnique."},{"key":"S0956796815000210_ref28","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003261"},{"key":"S0956796815000210_ref27","first-page":"240","volume-title":"Types","author":"Miquel","year":"2002"},{"key":"S0956796815000210_ref26","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"Luo","year":"1994"},{"key":"S0956796815000210_ref22","unstructured":"Geuvers H. (1993) Logics and Type Systems. Ph.D. thesis, Katholieke Universiteit Nijmegen."},{"key":"S0956796815000210_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38946-7_12"},{"key":"S0956796815000210_ref20","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"S0956796815000210_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"S0956796815000210_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_7"},{"key":"S0956796815000210_ref16","doi-asserted-by":"publisher","DOI":"10.1145\/226643.226675"},{"key":"S0956796815000210_ref15","unstructured":"Coq, Development Team. (2004) The Coq Proof Assistant Reference Manual. Version 8.0."},{"key":"S0956796815000210_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097785"},{"key":"S0956796815000210_ref9","first-page":"64","volume-title":"Cade","author":"Asperti","year":"2011"},{"key":"S0956796815000210_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000325X"},{"key":"S0956796815000210_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007278"},{"key":"S0956796815000210_ref5","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:4)2011"},{"key":"S0956796815000210_ref3","first-page":"3","volume-title":"Lics. Wroc\u0142aw","author":"Abel","year":"2007"},{"key":"S0956796815000210_ref6","first-page":"1","volume-title":"Domain Theory","author":"Abramsky","year":"1994"},{"key":"S0956796815000210_ref10","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt","year":"1992"},{"key":"S0956796815000210_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004726"},{"key":"S0956796815000210_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00166-2"},{"key":"S0956796815000210_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003750"},{"key":"S0956796815000210_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90105-9"},{"key":"S0956796815000210_ref1","doi-asserted-by":"crossref","unstructured":"Abadi M. , Cardelli L. , Curien P.-L. , & L\u00e9vy J. J. (1990) Explicit substitutions. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL '90: San Francisco, California, USA, January 1990. ACM, pp. 31\u201346.","DOI":"10.1145\/96709.96712"},{"key":"S0956796815000210_ref23","doi-asserted-by":"crossref","unstructured":"Geuvers H. , & Werner B. (1994) On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study. In Proceedings Symposium on Logic in Computer Science, 1994. LICS '94, Paris, France, July 4\u20137, 1994. pp. 320\u2013329.","DOI":"10.1109\/LICS.1994.316057"},{"key":"S0956796815000210_ref4","first-page":"29","volume-title":"Proceedings of the 9th International Conference on Mathematics of Program Construction, MPC 2008","author":"Abel","year":"2008"},{"key":"S0956796815000210_ref7","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005770"},{"key":"S0956796815000210_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_17"},{"key":"S0956796815000210_ref17","first-page":"209","volume-title":"Mfcs","author":"Curien","year":"1992"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796815000210","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,12]],"date-time":"2024-06-12T09:31:52Z","timestamp":1718184712000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796815000210\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":32,"alternative-id":["S0956796815000210"],"URL":"https:\/\/doi.org\/10.1017\/s0956796815000210","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"article-number":"e19"}}