{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:30:50Z","timestamp":1770273050928,"version":"3.49.0"},"reference-count":56,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2017,5,9]],"date-time":"2017-05-09T00:00:00Z","timestamp":1494288000000},"content-version":"unspecified","delay-in-days":128,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Modern constructive type theory is based on pure dependently typed lambda calculus, augmented with user-defined datatypes. This paper presents an alternative called the Calculus of Dependent Lambda Eliminations, based on pure lambda encodings with no auxiliary datatype system. New typing constructs are defined that enable induction, as well as large eliminations with lambda encodings. These constructs are constructor-constrained recursive types, and a lifting operation to lift simply typed terms to the type level. Using a lattice-theoretic denotational semantics for types, the language is proved logically consistent. The power of CDLE is demonstrated through several examples, which have been checked with a prototype implementation called Cedille.<\/jats:p>","DOI":"10.1017\/s0956796817000053","type":"journal-article","created":{"date-parts":[[2017,5,9]],"date-time":"2017-05-09T08:12:58Z","timestamp":1494317578000},"source":"Crossref","is-referenced-by-count":20,"title":["The calculus of dependent lambda eliminations"],"prefix":"10.1017","volume":"27","author":[{"given":"AARON","family":"STUMP","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,5,9]]},"reference":[{"key":"S0956796817000053_ref38","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\u00f6teborg, Sweden."},{"key":"S0956796817000053_ref54","first-page":"249","volume-title":"Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (ICFP)","author":"Washburn","year":"2003"},{"key":"S0956796817000053_ref22","first-page":"336","volume-title":"Computer Science Logic, 24th International Workshop (CSL)","author":"Ghani","year":"2010"},{"key":"S0956796817000053_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"S0956796817000053_ref51","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90097-7"},{"key":"S0956796817000053_ref20","first-page":"224","volume-title":"Proceedings of 25th International Conference on Rewriting Techniques and Applications (RTA) joint with the 12th International Conference on Typed Lambda Calculi and Applications (TLCA)","author":"Fu","year":"2014"},{"key":"S0956796817000053_ref56","unstructured":"Werner B. (1994) Une Th\u00e9orie des Constructions Inductives. PhD Thesis. Paris VII: Universit\u00e9 Paris-Diderot."},{"key":"S0956796817000053_ref34","unstructured":"Mendler N. (1988) Inductive Definition in Type Theory. PhD Thesis, Cornell University."},{"key":"S0956796817000053_ref52","unstructured":"The Coq development team (2015) The Coq Proof Assistant Reference Manual. LogiCal Project. Version 8.4."},{"key":"S0956796817000053_ref25","first-page":"241","volume-title":"Tapsoft'89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, March 13\u201317, 1989, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Current Issues in Programming Languages (CCIPL)","author":"Harper","year":"1989"},{"key":"S0956796817000053_ref49","doi-asserted-by":"publisher","DOI":"10.1145\/2841316"},{"key":"S0956796817000053_ref12","volume-title":"The Calculi of Lambda Conversion, Annals of Mathematics Studies","author":"Church","year":"1941"},{"key":"S0956796817000053_ref28","first-page":"4:1","volume-title":"Proceedings of 26th Symposium on Implementation and Application of Functional Languages (IFL)","author":"Koopman","year":"2014"},{"key":"S0956796817000053_ref3","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1145\/2578855.2535852","article-title":"A relationally parametric model of dependent type theory","volume":"49","author":"Atkey","year":"2014","journal-title":"Sigplan Not."},{"key":"S0956796817000053_ref39","first-page":"145","volume-title":"European Symposium On Programming (ESOP)","author":"Parigot","year":"1988"},{"key":"S0956796817000053_ref40","first-page":"309","volume-title":"Computer Science Logic (CSL)","author":"Parigot","year":"1989"},{"key":"S0956796817000053_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"S0956796817000053_ref29","doi-asserted-by":"crossref","unstructured":"Kopylov A. (2003) Dependent intersection: A new way of defining records in type theory. In Proceedings of 18th IEEE Symp. Log. Comput. Sci. (LICS), pp. 86\u201395.","DOI":"10.1109\/LICS.2003.1210048"},{"key":"S0956796817000053_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863565"},{"key":"S0956796817000053_ref1","first-page":"190","volume-title":"Proceedings of 18th International Workshop Computer Science Logic (CSL)","author":"Abel","year":"2004"},{"key":"S0956796817000053_ref27","first-page":"83","volume-title":"Twenty-Five Years of Constructive Type Theory","author":"Hofmann","year":"1998"},{"key":"S0956796817000053_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"S0956796817000053_ref55","unstructured":"Werner B. (1992) A normalization proof for an impredicative type system with large elimination over integers. In Proceedings of the 1992 Workshop on Types for Proofs and Programs. Available from http:\/\/www.cse.chalmers.se\/research\/group\/logic\/Types\/previousevents.html, last access April 23, 2017. pp. 341\u2013357."},{"key":"S0956796817000053_ref47","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"S0956796817000053_ref33","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796817000053_ref31","first-page":"460","volume-title":"Proceedings of 24th Annual Symposium on Foundations of Computer Science, 1983","author":"Leivant","year":"1983"},{"key":"S0956796817000053_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"S0956796817000053_ref9","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"S0956796817000053_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"S0956796817000053_ref53","unstructured":"Univalent Foundations Program (2013) Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study: http:\/\/homotopytypetheory.org\/book. Last accessed April 21, 2017."},{"key":"S0956796817000053_ref35","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512671"},{"key":"S0956796817000053_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/322358.322370"},{"key":"S0956796817000053_ref5","unstructured":"Berger U. & Schwichtenberg H. (1991) An inverse of the evaluation functional for typed lambda-calculus. In Proceedings of the 6th Annual Symposium on Logic in Computer Science (LICS). IEEE Computer Society, pp. 203\u2013211."},{"key":"S0956796817000053_ref44","first-page":"371","volume-title":"Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)","author":"Pientka","year":"2008"},{"key":"S0956796817000053_ref14","first-page":"227","volume-title":"Proceedings, Symposium on Logic in Computer Science (LICS)","author":"Coquand","year":"1986"},{"key":"S0956796817000053_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00010-5"},{"key":"S0956796817000053_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237792"},{"key":"S0956796817000053_ref37","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000423"},{"key":"S0956796817000053_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"S0956796817000053_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_16"},{"key":"S0956796817000053_ref41","first-page":"199","volume-title":"Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI)","author":"Pfenning","year":"1988"},{"key":"S0956796817000053_ref23","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0956796817000053_ref30","unstructured":"Krishnaswami N. R. & Dreyer D. (2013) Internalizing relational parametricity in the extensional calculus of constructions. In Computer Science Logic 2013 (CSL), Rocca S. R. D. (ed), LIPIcs, vol. 23. Schloss Dagstuhl \u2013 Leibniz-Zentrum fuer Informatik, pp. 432\u2013451."},{"key":"S0956796817000053_ref16","first-page":"50","volume-title":"Colog-88, International Conference on Computer Logic","author":"Coquand","year":"1988"},{"key":"S0956796817000053_ref11","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0956796817000053_ref15","volume-title":"Electronic Proceedings of the 3rd Annual Bra workshop on Logical Frameworks","author":"Coquand","year":"1992"},{"key":"S0956796817000053_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_5"},{"key":"S0956796817000053_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00418-7"},{"key":"S0956796817000053_ref24","doi-asserted-by":"crossref","unstructured":"Goguen H. , McBride C. & McKinna J. (2006) Eliminating dependent pattern matching. In Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of his 65th Birthday, Futatsugi K. , Jouannaud J.-P. & Meseguer J. (eds), pp. 521\u2013540.","DOI":"10.1007\/11780274_27"},{"key":"S0956796817000053_ref50","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000034"},{"key":"S0956796817000053_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804309"},{"key":"S0956796817000053_ref4","first-page":"239","volume-title":"Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming (ICFP)","author":"Augustsson","year":"1998"},{"key":"S0956796817000053_ref6","first-page":"108","volume-title":"Proceedings of 14th International Conference Foundations of Software Science and Computational Structures","author":"Bernardy","year":"2011"},{"key":"S0956796817000053_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90053-5"},{"key":"S0956796817000053_ref42","first-page":"209","volume-title":"Proceedings of 5th International Conference Mathematical Foundations of Programming Semantics","author":"Pfenning","year":"1989"},{"key":"S0956796817000053_ref13","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796817000053","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T04:38:01Z","timestamp":1602045481000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796817000053\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":56,"alternative-id":["S0956796817000053"],"URL":"https:\/\/doi.org\/10.1017\/s0956796817000053","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"article-number":"e14"}}