{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:06Z","timestamp":1775790726726,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642415814","type":"print"},{"value":"9783642415821","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41582-1_10","type":"book-chapter","created":{"date-parts":[[2013,11,15]],"date-time":"2013-11-15T12:38:21Z","timestamp":1384519101000},"page":"157-173","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":25,"title":["Engineering Proof by Reflection in Agda"],"prefix":"10.1007","author":[{"given":"Paul","family":"van der Walt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wouter","family":"Swierstra","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,11,16]]},"reference":[{"key":"10_CR1","unstructured":"Norell, U.: 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 (2007)"},{"key":"10_CR2","first-page":"1","volume-title":"In: Proceedings of the 4th International Workshop on Types in Language Design and Implementation, TLDI \u201909","author":"U Norell","year":"2009","unstructured":"Norell, U.: Dependently typed programming in Agda. In: Proceedings of the 4th International Workshop on Types in Language Design and Implementation, TLDI \u201909, pp. 1\u20132. ACM, New York (2009)"},{"key":"10_CR3","unstructured":"van der Walt, P.: Reflection in Agda. Master\u2019s thesis, Department of Computer Science, Utrecht University, Utrecht, The Netherlands. http:\/\/igitur-archive.library.uu.nl\/student-theses\/2012-1030-200720\/UUindex.html (2012)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Pitman, K.M.: Special forms in Lisp. In: Proceedings of the ACM Conference on LISP and Functional Programming, pp. 179\u2013187. ACM (1980)","DOI":"10.1145\/800087.802804"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: Proceedings of the 1997 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM \u201997 (1997)","DOI":"10.1145\/258993.259019"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Sheard, T., Peyton Jones, S.: Template meta-programming for Haskell. In: Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, pp. 1\u201316 (2002)","DOI":"10.1145\/581690.581691"},{"key":"10_CR7","first-page":"167","volume-title":"In: Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages","author":"P Martin-L\u00f6f","year":"1985","unstructured":"Martin-L\u00f6f, P.: Constructive mathematics and computer programming. In: Proceedings of a Discussion Meeting of the Royal Society of London on Mathematical Logic and Programming Languages, pp. 167\u2013184. Prentice-Hall Inc., Upper Saddle River (1985)"},{"issue":"2\/3","key":"10_CR8","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.P.: The calculus of constructions. Inf. Comput. 76(2\/3), 95\u2013120 (1988)","journal-title":"Inf. Comput."},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1145\/1411204.1411213","volume-title":"In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP \u201908","author":"N Oury","year":"2008","unstructured":"Oury, N., Swierstra, W.: The power of pi. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP \u201908, pp. 39\u201350. ACM, New York (2008)"},{"key":"10_CR10","unstructured":"Agda Developers: Agda release notes, regarding reflection. The Agda Wiki: http:\/\/wiki.portal.chalmers.se\/agda\/agda.php?n=Main.Version-2-2-8 and http:\/\/wiki.portal.chalmers.se\/agda\/agda.php?n=Main.Version-2-3-0 (2013). Accessed 9 Feb 2013"},{"key":"10_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"10_CR12","volume-title":"Certified Programming with Dependent Types","author":"A Chlipala","year":"2011","unstructured":"Chlipala, A.: Certified Programming with Dependent Types. MIT Press, New York (2011)"},{"key":"10_CR13","unstructured":"Jedynak, W.: Agda ring solver using reflection. GitHub. https:\/\/github.com\/wjzz\/Agda-reflection-for-semiring-solver (2012). Accessed 26 June 2012"},{"key":"10_CR14","unstructured":"Demers, F., Malenfant, J.: Reflection in logic, functional and object-oriented programming: a short comparative study. In: Proceedings of the IJCAI, vol. 95, pp. 29\u201338 (1995)"},{"key":"10_CR15","first-page":"23","volume-title":"In: Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201984","author":"BC Smith","year":"1984","unstructured":"Smith, B.C.: Reflection and semantics in LISP. In: Proceedings of the 11th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL \u201984, pp. 23\u201335. ACM, New York (1984)"},{"issue":"2","key":"10_CR16","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/s10990-007-9022-0","volume":"22","author":"A Stump","year":"2009","unstructured":"Stump, A.: Directly reflective meta-programming. High. Order Symbolic Comput. 22(2), 115\u2013144 (2009)","journal-title":"High. Order Symbolic Comput."},{"key":"10_CR17","volume-title":"Smalltalk-80: The Language and Its Implementation","author":"A Goldberg","year":"1983","unstructured":"Goldberg, A., Robson, D.: Smalltalk-80: The Language and Its Implementation. Addison-Wesley Longman Publishing Co. Inc., Boston (1983)"},{"key":"10_CR18","unstructured":"Sheard, T.: Staged programming. http:\/\/web.cecs.pdx.edu\/~sheard\/staged.html. Accessed 20 Aug 2012"},{"key":"10_CR19","unstructured":"Altenkirch, T.: [Agda mailing list] More powerful quoting and reflection? mailing list communication. https:\/\/lists.chalmers.se\/pipermail\/agda\/2012\/004127.html (2012). Accessed 14 Sept 2012"},{"issue":"2","key":"10_CR20","first-page":"95","volume":"3","author":"G Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. J. Formalized Reasoning 3(2), 95\u2013152 (2010). (RR-7392 RR-7392)","journal-title":"J. Formalized Reasoning"},{"key":"10_CR21","first-page":"333","volume-title":"ASCM 2007. LNCS (LNAI)","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: The four colour theorem: engineering of a formal proof. In: Kapur, D. (ed.) ASCM 2007. LNCS (LNAI), vol. 5081, p. 333. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Functional Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-41582-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T12:33:05Z","timestamp":1676637185000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-41582-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642415814","9783642415821"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41582-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]},"assertion":[{"value":"16 November 2013","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}