{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:21:12Z","timestamp":1742980872926,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030148041"},{"type":"electronic","value":"9783030148058"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-14805-8_7","type":"book-chapter","created":{"date-parts":[[2019,2,20]],"date-time":"2019-02-20T13:04:29Z","timestamp":1550667869000},"page":"115-134","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Project Report: Dependently Typed Programming with Lambda Encodings in Cedille"],"prefix":"10.1007","author":[{"given":"Ananda","family":"Guneratne","sequence":"first","affiliation":[]},{"given":"Chad","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,2,21]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Basold, H., Geuvers, H.: Type theory based on dependent inductive and coinductive types. In: Shankar, N. (ed.) IEEE Symposium on Logic in Computer Science (LICS) (2016)","key":"7_CR1","DOI":"10.1145\/2933575.2934514"},{"unstructured":"Bezem, M., Coquand, T., Huber, S.: A model of type theory in cubical sets. In: Matthes, R., Schubert, A. (eds.) 19th International Conference on Types for Proofs and Programs, TYPES 2013 of LIPIcs, vol. 26, pp. 107\u2013128. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)","key":"7_CR2"},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/0304-3975(85)90135-5","volume":"39","author":"C B\u00f6hm","year":"1985","unstructured":"B\u00f6hm, C., Berarducci, A.: Automatic synthesis of typed lambda-programs on term algebras. Theor. Comput. Sci. 39, 135\u2013154 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR4","volume-title":"The Calculi of Lambda Conversion","author":"A Church","year":"1941","unstructured":"Church, A.: The Calculi of Lambda Conversion. Princeton University Press, Princeton (1941). Ann. Math. Stud. (6)"},{"issue":"2\u20133","key":"7_CR5","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The calculus of constructions. Inf. Comput. 76(2\u20133), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, pp. 50\u201366. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52335-9_47"},{"unstructured":"The Agda Development Team: Agda, Version 2.5.1 (2016)","key":"7_CR7"},{"issue":"1","key":"7_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/322358.322370","volume":"30","author":"S Fortune","year":"1983","unstructured":"Fortune, S., Leivant, D., O\u2019Donnell, M.: The expressiveness of simple and second-order type structures. J. ACM 30(1), 151\u2013185 (1983)","journal-title":"J. ACM"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/3-540-45413-6_16","volume-title":"Typed Lambda Calculi and Applications","author":"H Geuvers","year":"2001","unstructured":"Geuvers, H.: Induction is not derivable in second order dependent type theory. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 166\u2013181. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45413-6_16"},{"doi-asserted-by":"crossref","unstructured":"Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Twenty-Five Years of Constructive Type Theory of Oxford Logic Guides, vol. 36, pp. 83\u2013111. Oxford University Press, Oxford (1998)","key":"7_CR10","DOI":"10.1093\/oso\/9780198501275.003.0008"},{"unstructured":"Koopman, P., Plasmeijer, R., Jansen, J.M.: Church encoding of data types considered harmful for implementations. In: Plasmeijer, R., Tobin-Hochstadt, S. (eds.) 26th Symposium on Implementation and Application of Functional Languages (IFL) (2014). Presented version","key":"7_CR11"},{"unstructured":"Kopylov, A.: Dependent intersection: a new way of defining records in type theory. In: 18th IEEE Symposium on Logic in Computer Science (LICS), pp. 86\u201395 (2003)","key":"7_CR12"},{"issue":"1","key":"7_CR13","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/0890-5401(91)90053-5","volume":"93","author":"D Leivant","year":"1991","unstructured":"Leivant, D.: Finitely stratified polymorphism. Inf. Comput. 93(1), 93\u2013113 (1991)","journal-title":"Inf. Comput."},{"unstructured":"Luo, Z.: An extended calculus of constructions. Ph.D. thesis (1990)","key":"7_CR14"},{"unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual. LogiCal Project, Version 8.5 (2016)","key":"7_CR15"},{"unstructured":"McAllester, D.A.: Implementation and abstraction in mathematics. CoRR, abs\/1407.7274 (2014)","key":"7_CR16"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-45842-5_13","volume-title":"Types for Proofs and Programs","author":"C McBride","year":"2002","unstructured":"McBride, C.: Elimination with a motive. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 197\u2013216. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45842-5_13"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/3-540-45413-6_27","volume-title":"Typed Lambda Calculi and Applications","author":"A Miquel","year":"2001","unstructured":"Miquel, A.: The implicit calculus of constructions extending pure type systems with an intersection type binder and subtyping. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 344\u2013359. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45413-6_27"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-19027-9_10","volume-title":"ESOP \u201988","author":"M Parigot","year":"1988","unstructured":"Parigot, M.: Programming with proofs: a second order type theory. In: Ganzinger, H. (ed.) ESOP 1988. LNCS, vol. 300, pp. 145\u2013159. Springer, Heidelberg (1988). https:\/\/doi.org\/10.1007\/3-540-19027-9_10"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/3-540-52753-2_47","volume-title":"CSL 1989","author":"M Parigot","year":"1990","unstructured":"Parigot, M.: On the representation of data in lambda-calculus. In: B\u00f6rger, E., B\u00fcning, H.K., Richter, M.M. (eds.) CSL 1989. LNCS, vol. 440, pp. 309\u2013321. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52753-2_47"},{"issue":"1","key":"7_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/345099.345100","volume":"22","author":"BC Pierce","year":"2000","unstructured":"Pierce, B.C., Turner, D.N.: Local type inference. ACM Trans. Program. Lang. Syst. 22(1), 1\u201344 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"unstructured":"Stump, A.: From realizability to induction via dependent intersection. Available from the author\u2019s web page, under review as of 19 June 2017","key":"7_CR22"},{"key":"7_CR23","doi-asserted-by":"publisher","first-page":"e14","DOI":"10.1017\/S0956796817000053","volume":"27","author":"A Stump","year":"2017","unstructured":"Stump, A.: The calculus of dependent lambda eliminations. J. Funct. Program. 27, e14 (2017)","journal-title":"J. Funct. Program."},{"key":"7_CR24","doi-asserted-by":"publisher","first-page":"e3 (31 p.)","DOI":"10.1017\/S0956796816000034","volume":"26","author":"A Stump","year":"2016","unstructured":"Stump, A., Fu, P.: Efficiency of lambda-encodings in total type theory. J. Funct. Program. 26, e3 (31 p.) (2016)","journal-title":"J. Funct. Program."},{"unstructured":"The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study (2013). https:\/\/homotopytypetheory.org\/book","key":"7_CR25"},{"issue":"1","key":"7_CR26","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1017\/S0956796807006557","volume":"18","author":"G Washburn","year":"2008","unstructured":"Washburn, G., Weirich, S.: Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism. J. Funct. Program. 18(1), 87\u2013140 (2008)","journal-title":"J. Funct. Program."},{"unstructured":"Werner, B.: Une Th\u00e9orie des constructions inductives. Ph.D. thesis, Paris Diderot University, France (1994)","key":"7_CR27"}],"container-title":["Lecture Notes in Computer Science","Trends in Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-14805-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,28]],"date-time":"2020-11-28T05:54:55Z","timestamp":1606542895000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-14805-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030148041","9783030148058"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-14805-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"21 February 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TFP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Trends in Functional Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"College Park, MD","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 June 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 June 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tfp2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"18","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"56% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3,7","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3,35","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}