{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:44Z","timestamp":1779836744614,"version":"3.53.1"},"reference-count":25,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2012,3,16]],"date-time":"2012-03-16T00:00:00Z","timestamp":1331856000000},"content-version":"unspecified","delay-in-days":15,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2012,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Pure Type Systems are usually described in two different ways, one that uses an external notion of computation like beta-reduction, and one that relies on a typed judgment of equality, directly in the typing system. For a long time, the question was open to know whether both presentations described the same theory. A first step towards this equivalence has been made by Adams for a particular class of\n                    <jats:italic>Pure Type Systems<\/jats:italic>\n                    (PTS) called functional. Then, his result has been relaxed to all semi-full PTSs in previous work. In this paper, we finally give a positive answer to the general question, and prove that equivalence holds for any Pure Type System.\n                  <\/jats:p>","DOI":"10.1017\/s0956796812000044","type":"journal-article","created":{"date-parts":[[2012,3,16]],"date-time":"2012-03-16T06:38:37Z","timestamp":1331879917000},"page":"153-180","source":"Crossref","is-referenced-by-count":10,"title":["Pure Type System conversion is always typable"],"prefix":"10.1017","volume":"22","author":[{"given":"VINCENT","family":"SILES","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"HUGO","family":"HERBELIN","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2012,3,16]]},"reference":[{"key":"S0956796812000044_ref13","first-page":"385","volume-title":"Proceedings of the Fourth Annual Symposium on Logic in Computer Science","author":"Luo","year":"1989"},{"key":"S0956796812000044_ref24","unstructured":"Werner B. (1994) Une th\u00e9orie des Constructions Inductives. Ph.D. thesis, Universit\u00e9 Paris, France."},{"key":"S0956796812000044_ref19","unstructured":"Siles V. (2010) Formalization of Equivalence Between PTS and PTSe. http:\/\/www.lix.polytechnique.fr\/vsiles\/coq\/PTSATR.html."},{"key":"S0956796812000044_ref22","volume-title":"Een nadere Bewijstheoretische Analyse van GSTTs (Manuscript, in Dutch)","author":"Terlouw","year":"1989"},{"key":"S0956796812000044_ref23","first-page":"19","volume-title":"TYPES","author":"van Benthem Jutting","year":"1993"},{"key":"S0956796812000044_ref16","volume-title":"Programming in Martin-L\u00f6f's Type Theory: An introduction","author":"Nordstrom","year":"1990"},{"key":"S0956796812000044_ref5","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"Barendregt","year":"1992"},{"key":"S0956796812000044_ref18","unstructured":"Pollack R. (1994) The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. Ph.D. thesis, University of Edinburgh, Scotland."},{"key":"S0956796812000044_ref3","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005770"},{"key":"S0956796812000044_ref15","volume-title":"A Generic Normalization Proof for Pure Type Systems. TYPES'96","author":"Melli\u00e8s","year":"1997"},{"key":"S0956796812000044_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"S0956796812000044_ref7","unstructured":"Coq Development Team. (2010) The Coq Proof Assistant Reference Manual. http:\/\/coq.inria.fr\/refman\/."},{"key":"S0956796812000044_ref4","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1017\/S0956796800020025","article-title":"Introduction to generalized type systems","volume":"1","author":"Barendregt","year":"1991","journal-title":"J. Funct. Program."},{"key":"S0956796812000044_ref17","unstructured":"Norell U. (2007 September) Towards a Practical Programming Language Based on Dependent Type Theory. Ph.D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg, Sweden."},{"key":"S0956796812000044_ref14","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796812000044_ref1","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/978-3-642-12251-4_17","volume-title":"Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010), Sendai, Japan, April 19-21, 2010","author":"Abel","year":"2010"},{"key":"S0956796812000044_ref20","volume-title":"Proceedings of the 25th Annual IEEE Symposium on Login in Computer Science (LICS '10), Edinburgh, UK, 11-14 July 2010","author":"Siles","year":"2010"},{"key":"S0956796812000044_ref10","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","article-title":"Modular proof of strong normalization for the calculus of constructions","volume":"1","author":"Geuvers","year":"1991","journal-title":"J. Funct. Program."},{"key":"S0956796812000044_ref25","article-title":"A proof-irrelevant model of CC with predicate induction and judgemental equality","volume":"7","author":"Werner","year":"2011","journal-title":"Logical Methods Comput. Sci."},{"key":"S0956796812000044_ref6","unstructured":"Berardi S. (1990) Type Dependence and Constructive Mathematics. Ph.D. thesis, Mathematical Institute Torino, Italy."},{"key":"S0956796812000044_ref12","doi-asserted-by":"crossref","unstructured":"Goguen H. (1994) A Typed Operational Semantics for Type Theory. Ph.D. thesis, University of Edinburgh, Scotland.","DOI":"10.1007\/BFb0014053"},{"key":"S0956796812000044_ref2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.33"},{"key":"S0956796812000044_ref11","first-page":"320","volume-title":"Logic in Computer Science","author":"Geuvers","year":"1994"},{"key":"S0956796812000044_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"S0956796812000044_ref9","unstructured":"Geuvers H. (1993) Logics and Type Systems. Ph.D. thesis, Katholieke Universiteit Nijmegen, The Netherlands."}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796812000044","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:24Z","timestamp":1779834984000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796812000044\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,3]]}},"alternative-id":["S0956796812000044"],"URL":"https:\/\/doi.org\/10.1017\/s0956796812000044","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,3]]}}}