{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:03:52Z","timestamp":1759147432502},"reference-count":18,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2016,3,10]],"date-time":"2016-03-10T00:00:00Z","timestamp":1457568000000},"content-version":"unspecified","delay-in-days":69,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2016]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper proposes a new typed lambda-encoding for inductive types which, for Peano numerals, has the expected time complexities for basic operations like addition and multiplication, has a constant-time predecessor function, and requires only quadratic space to encode a numeral. This improves on the exponential space required by the Parigot encoding. Like the Parigot encoding, the new encoding is typable in System F-omega plus positive-recursive type definitions, a total type theory. The new encoding is compared with previous ones through a significant case study: mergesort using Braun trees. The practical runtime efficiency of the new encoding, and the Church and Parigot encodings, are compared by two translations, one to Racket and one to Haskell, on a small suite of benchmarks.<\/jats:p>","DOI":"10.1017\/s0956796816000034","type":"journal-article","created":{"date-parts":[[2016,3,10]],"date-time":"2016-03-10T09:31:44Z","timestamp":1457602304000},"source":"Crossref","is-referenced-by-count":7,"title":["Efficiency of lambda-encodings in total type theory"],"prefix":"10.1017","volume":"26","author":[{"given":"AARON","family":"STUMP","sequence":"first","affiliation":[]},{"given":"PENG","family":"FU","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2016,3,10]]},"reference":[{"key":"S0956796816000034_ref4","volume-title":"The Calculi of Lambda Conversion","author":"Church","year":"1941"},{"key":"S0956796816000034_ref8","unstructured":"Fu P. & Stump A. (2014) Self types for dependently typed lambda encodings. In Proceedings of 25th International Conference on Rewriting Techniques and Applications (RTA) joint with the 12th International Conference on Typed Lambda Calculi and Applications (TLCA), Dowek G. (ed), Lecture Notes in Computer Science, vol. 8560, Springer, pp. 224\u2013239."},{"key":"S0956796816000034_ref15","volume-title":"European Symposium On Programming (ESOP)","author":"Parigot","year":"1988"},{"key":"S0956796816000034_ref1","unstructured":"Abel A. & Matthes R. (2004) Fixed points of type constructors and primitive recursion. In Proceedings of 18th International Workshop Computer Science Logic (CSL), Marcinkowski J. & Tarlecki A. (eds), pp. 190\u2013204."},{"key":"S0956796816000034_ref18","unstructured":"The Coq development team. (2014) The Coq proof assistant reference manual. LogiCal Project. Version 8.4."},{"key":"S0956796816000034_ref17","unstructured":"Philip W. (1990) Recursive types for free! Available at http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/free-rectypes\/free-rectypes.txt."},{"key":"S0956796816000034_ref13","unstructured":"Norrell U. & the Agda Development Team. (2014) The Agda Wiki."},{"key":"S0956796816000034_ref12","volume-title":"Perspectives of System Informatics","author":"Mogensen","year":"2001"},{"key":"S0956796816000034_ref10","volume-title":"The Implementation of Functional Programming Languages","author":"Jones","year":"1987"},{"key":"S0956796816000034_ref6","volume-title":"Semantics Engineering with PLT Redex","author":"Felleisen","year":"2009"},{"key":"S0956796816000034_ref9","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005313"},{"key":"S0956796816000034_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002876"},{"key":"S0956796816000034_ref2","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1985"},{"key":"S0956796816000034_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"S0956796816000034_ref11","doi-asserted-by":"crossref","unstructured":"Koopman P. , Plasmeijer R & Jansen J. M. (2014) Church encoding of data types considered harmful for implementations. In Proceedings of 26th Symposium on Implementation and Application of Functional Languages (IFL), Plasmeijer R. & Tobin-Hochstadt S. (eds), Presented version.","DOI":"10.1145\/2746325.2746330"},{"key":"S0956796816000034_ref7","unstructured":"Flatt M. & PLT. (2010) Reference: Racket. Technical Report PLT-TR-2010-1. PLT Design Inc. http:\/\/racket-lang.org\/tr1\/."},{"key":"S0956796816000034_ref16","first-page":"309","volume-title":"Proceedings of 3rd Workshop on Computer Science Logic (CSL)","author":"Parigot","year":"1989"},{"key":"S0956796816000034_ref5","volume-title":"Combinatory Logic","author":"Curry","year":"1972"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000034","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T23:51:04Z","timestamp":1559951464000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000034\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"references-count":18,"alternative-id":["S0956796816000034"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000034","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"article-number":"e3"}}