{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:30:15Z","timestamp":1770276615723,"version":"3.49.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030336356","type":"print"},{"value":"9783030336363","type":"electronic"}],"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-33636-3_10","type":"book-chapter","created":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T10:02:20Z","timestamp":1571479340000},"page":"255-297","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["System F in Agda, for Fun and Profit"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9036-8252","authenticated-orcid":false,"given":"James","family":"Chapman","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4687-2739","authenticated-orcid":false,"given":"Roman","family":"Kireev","sequence":"additional","affiliation":[]},{"given":"Chad","family":"Nester","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7619-6378","authenticated-orcid":false,"given":"Philip","family":"Wadler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,10,20]]},"reference":[{"key":"10_CR1","unstructured":"Abadi, M., Cardelli, L., Plotkin, G.: Types for the Scott numerals (1993)"},{"key":"10_CR2","doi-asserted-by":"publisher","unstructured":"Allais, G., Chapman, J., McBride, C., McKinna, J.: Type-and-scope safe programs and their proofs. In: Bertot, Y., Vafeiadis, V. (eds.) Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), pp. 195\u2013207. ACM, New York (2017). \n                    https:\/\/doi.org\/10.1145\/3018610.3018613","DOI":"10.1145\/3018610.3018613"},{"key":"10_CR3","doi-asserted-by":"publisher","unstructured":"Allais, G., McBride, C., Boutillier, P.: New equations for neutral terms. In: Weirich, S. (ed.) Proceedings of the 2013 ACM SIGPLAN Workshop on Dependently-typed Programming (DTP 2013), pp. 13\u201324. ACM, New York (2013). \n                    https:\/\/doi.org\/10.1145\/2502409.2502411","DOI":"10.1145\/2502409.2502411"},{"issue":"1","key":"10_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/issn.1972-5787\/4389","volume":"7","author":"T Altenkirch","year":"2014","unstructured":"Altenkirch, T., Chapman, J., Uustalu, T.: Relative monads formalised. J. Formalized Reasoning 7(1), 1\u201343 (2014). \n                    https:\/\/doi.org\/10.6092\/issn.1972-5787\/4389","journal-title":"J. Formalized Reasoning"},{"issue":"1","key":"10_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-11(1:3)2015","volume":"11","author":"T Altenkirch","year":"2015","unstructured":"Altenkirch, T., Chapman, J., Uustalu, T.: Monads need not be endofunctors. Logical Methods Comput. Sci. 11(1), 1\u201340 (2015). \n                    https:\/\/doi.org\/10.2168\/LMCS-11(1:3)2015","journal-title":"Logical Methods Comput. Sci."},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/3-540-48168-0_32","volume-title":"Computer Science Logic","author":"T Altenkirch","year":"1999","unstructured":"Altenkirch, T., Reus, B.: Monadic presentations of lambda terms using generalized inductive types. In: Flum, J., Rodriguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 453\u2013468. Springer, Heidelberg (1999). \n                    https:\/\/doi.org\/10.1007\/3-540-48168-0_32"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying ethereum smart contract bytecode in isabelle\/HOL. In: Andronick, J., Felty, A. (eds.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 66\u201377. ACM, New York (2018). \n                    https:\/\/doi.org\/10.1145\/3167084","DOI":"10.1145\/3167084"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"BE Aydemir","year":"2005","unstructured":"Aydemir, B.E., et al.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50\u201365. Springer, Heidelberg (2005). \n                    https:\/\/doi.org\/10.1007\/11541868_4"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed lambda-calculus. In: Kahn, G. (ed.) Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS 1991), pp. 203\u2013211. IEEE Computer Society Press (1991). \n                    https:\/\/doi.org\/10.1109\/LICS.1991.151645","DOI":"10.1109\/LICS.1991.151645"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Brown, M., Palsberg, J.: Breaking through the normalization barrier: a self-interpreter for F-omega. In: Majumdar, R. (ed.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pp. 5\u201317. ACM, New York (2016). \n                    https:\/\/doi.org\/10.1145\/2837614.2837623","DOI":"10.1145\/2837614.2837623"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Cai, Y., Giarrusso, P.G., Ostermann, K.: System F-omega with equirecursive types for datatype-generic programming. In: Majumdar, R. (ed.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pp. 30\u201343. ACM, New York (2016). \n                    https:\/\/doi.org\/10.1145\/2837614.2837660","DOI":"10.1145\/2837614.2837660"},{"key":"10_CR12","unstructured":"Chakravarty, M., et al.: Functional Blockchain Contracts. Technical report, IOHK (2019). \n                    https:\/\/iohk.io\/research\/papers\/#KQL88VAR"},{"key":"10_CR13","unstructured":"Chapman, J.: Type checking and normalisation. Ph.D. thesis, University of Nottingham, UK (2009). \n                    http:\/\/eprints.nottingham.ac.uk\/10824\/"},{"key":"10_CR14","unstructured":"Chapman, J., Kireev, R., Nester, C., Wadler, P.: Literate Agda source of MPC 2019 paper (2019). \n                    https:\/\/github.com\/input-output-hk\/plutus\/blob\/f9f7aef94d9614b67c037337079ad89329889ffa\/papers\/system-f-in-agda\/paper.lagda"},{"issue":"1","key":"10_CR15","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1023\/A:1019964114625","volume":"15","author":"C Coquand","year":"2002","unstructured":"Coquand, C.: A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. High. Order Symbolic Comput. 15(1), 57\u201390 (2002). \n                    https:\/\/doi.org\/10.1023\/A:1019964114625","journal-title":"High. Order Symbolic Comput."},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-74464-1_7","volume-title":"Types for Proofs and Programs","author":"NA Danielsson","year":"2007","unstructured":"Danielsson, N.A.: A formalisation of a dependently typed language as an inductive-recursive family. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 93\u2013109. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-74464-1_7"},{"key":"10_CR17","doi-asserted-by":"publisher","unstructured":"van Doorn, F., Geuvers, H., Wiedijk, F.: Explicit convertibility proofs in pure type systems. In: Proceedings of the Eighth ACM SIGPLAN International Workshop on Logical Frameworks & Meta-languages: Theory & Practice, (LFMTP 2013), pp. 25\u201336. ACM, New York (2013). \n                    https:\/\/doi.org\/10.1145\/2503887.2503890","DOI":"10.1145\/2503887.2503890"},{"key":"10_CR18","unstructured":"Dreyer, D.: Understanding and Evolving the ML Module System. Ph.D. thesis, Carnegie Mellon University (2005)"},{"issue":"9","key":"10_CR19","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1145\/1291220.1291196","volume":"42","author":"Derek Dreyer","year":"2007","unstructured":"Dreyer, D.: A type system for recursive modules. In: Ramsey, N. (ed.) Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming (ICFP 2007), pp. 289\u2013302. ACM, New York (2007). \n                    https:\/\/doi.org\/10.1145\/1291220.1291196","journal-title":"ACM SIGPLAN Notices"},{"issue":"2","key":"10_CR20","doi-asserted-by":"publisher","first-page":"525","DOI":"10.2307\/2586554","volume":"65","author":"Peter Dybjer","year":"2000","unstructured":"Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symbolic Logic 65(2), 525\u2013549 (2000). \n                    http:\/\/www.jstor.org\/stable\/2586554","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-89722-6_10","volume-title":"Principles of Security and Trust","author":"I Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of ethereum smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243\u2013269. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-89722-6_10"},{"key":"10_CR22","unstructured":"Harz, D., Knottenbelt, W.J.: Towards Safer Smart Contracts: A Survey of Languages and Verification Methods (2018). \n                    https:\/\/arxiv.org\/abs\/1809.09805"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Hindley, J.R., Seldin, J.P.: Lambda-Calculus and Combinators: An Introduction. Cambridge University Press, Cambridge (2008)","DOI":"10.1017\/CBO9780511809835"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/BFb0037110","volume-title":"Typed Lambda Calculi and Applications","author":"A Jung","year":"1993","unstructured":"Jung, A., Tiuryn, J.: A new characterization of lambda definability. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 245\u2013257. Springer, Heidelberg (1993). \n                    https:\/\/doi.org\/10.1007\/BFb0037110"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-030-33636-3_15","volume-title":"MPC 2019","author":"M Peyton Jones","year":"2019","unstructured":"Peyton Jones, M., Gkoumas, V., Kireev, R., MacKenzie, K., Nester, C., Wadler, P.: Unraveling recursion: compiling an IR with recursion to system F. In: Hutton, G. (ed.) MPC 2019. LNCS, vol. 11825, pp. 414\u2013443. Springer, Cham (2019). \n                    https:\/\/doi.org\/10.1007\/978-3-030-33636-3_15"},{"key":"10_CR27","unstructured":"Kov\u00e1cs, A.: System F Omega. \n                    https:\/\/github.com\/AndrasKovacs\/system-f-omega"},{"key":"10_CR28","doi-asserted-by":"publisher","unstructured":"Martens, C., Crary, K.: LF in LF: mechanizing the metatheories of LF in Twelf. In: Proceedings of the Seventh International Workshop on Logical Frameworks and Meta-languages, Theory and Practice (LFMTP 2012), pp. 23\u201332. ACM, New York (2012). \n                    https:\/\/doi.org\/10.1145\/2364406.2364410","DOI":"10.1145\/2364406.2364410"},{"key":"10_CR29","unstructured":"McBride, C.: Datatypes of datatypes. In: Summer School on Generic and Effectful Programming, St Anne\u2019s College, Oxford (2015). \n                    https:\/\/www.cs.ox.ac.uk\/projects\/utgp\/school\/conor.pdf"},{"key":"10_CR30","unstructured":"Nomadic Labs: Michelson in Coq. Git Repository. \n                    https:\/\/gitlab.com\/nomadic-labs\/mi-cho-coq\/"},{"key":"10_CR31","doi-asserted-by":"publisher","unstructured":"O\u2019Connor, R.: Simplicity: a new language for blockchains. In: Bielova, N., Gaboardi, M. (eds.) Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security (PLAS 2017), pp. 107\u2013120. ACM, New York (2017). \n                    https:\/\/doi.org\/10.1145\/3139337.3139340","DOI":"10.1145\/3139337.3139340"},{"key":"10_CR32","doi-asserted-by":"publisher","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., Ro\u015fu, G.: A formal verification tool for ethereum VM bytecode. In: Garcia, A., Pasareanu, C.S. (eds.) Proceedings of the 2018 26th ACM Join Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC\/FSE 2018), pp. 912\u2013915. ACM, New York (2018). \n                    https:\/\/doi.org\/10.1145\/3236024.3264591","DOI":"10.1145\/3236024.3264591"},{"key":"10_CR33","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"key":"10_CR34","unstructured":"Pollack, R., Poll, E.: Typechecking in pure type systems. In: Informal Proceedings of Logical Frameworks 1992, pp. 271\u2013288 (1992)"},{"key":"10_CR35","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-0-387-21798-7_15","volume-title":"Monographs in Computer Science","author":"John C. Reynolds","year":"2003","unstructured":"Reynolds, J.C.: What do types mean? - from intrinsic to extrinsic semantics. In: McIver, A., Morgan, C. (eds.) Programming Methodology. Monographs in Computer Science, pp. 309\u2013327. Springer, New York (2003). \n                    https:\/\/doi.org\/10.1007\/978-0-387-21798-7_15"},{"key":"10_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-030-03044-5_5","volume-title":"Formal Methods: Foundations and Applications","author":"P Wadler","year":"2018","unstructured":"Wadler, P.: Programming language foundations in agda. In: Massoni, T., Mousavi, M.R. (eds.) SBMF 2018. LNCS, vol. 11254, pp. 56\u201373. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-030-03044-5_5"},{"key":"10_CR37","unstructured":"Wadler, P., Kokke, W.: Programming Language Foundations in Agda. \n                    https:\/\/plfa.github.io\/"},{"key":"10_CR38","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1016\/j.entcs.2007.11.013","volume":"199","author":"Kevin Watkins","year":"2008","unstructured":"Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: Specifying properties of concurrent computations in CLF. In: Sch\u00fcrmann, C. (ed.) Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages (LFM 2004). ENTCS, vol. 199, pp. 67\u201387 (2008). \n                    https:\/\/doi.org\/10.1016\/j.entcs.2007.11.013","journal-title":"Electronic Notes in Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-33636-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,19]],"date-time":"2019-10-19T10:10:58Z","timestamp":1571479858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-33636-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030336356","9783030336363"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-33636-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MPC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Mathematics of Program Construction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mpc2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.nott.ac.uk\/~pszgmh\/mpc19.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"68% - 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 (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}