{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T19:55:37Z","timestamp":1725738937851},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642393198"},{"type":"electronic","value":"9783642393204"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39320-4_3","type":"book-chapter","created":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T07:22:52Z","timestamp":1372663372000},"page":"35-50","source":"Crossref","is-referenced-by-count":7,"title":["The Formalization of Syntax-Based Mathematical Algorithms Using Quotation and Evaluation"],"prefix":"10.1007","author":[{"given":"William M.","family":"Farmer","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Van Tassel, J.: Experience with embedding hardware description languages in HOL. In: Stavridou, V., Melham, T.F., Boute, R.T. (eds.) Proceedings of the IFIP TC10\/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience. IFIP Transactions A: Computer Science and Technology, vol.\u00a0A-10, pp. 129\u2013156. North-Holland (1993)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-22673-1_23","volume-title":"Intelligent Computer Mathematics","author":"J. Carette","year":"2011","unstructured":"Carette, J., Farmer, W.M., O\u2019Connor, R.: Mathscheme: Project description. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS, vol.\u00a06824, pp. 287\u2013288. Springer, Heidelberg (2011)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Carnap, R.: Die Logische Syntax der Sprache. Springer (1934)","DOI":"10.1007\/978-3-662-25375-5"},{"key":"3_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-74621-8_10","volume-title":"Frontiers of Combining Systems","author":"E. Contejean","year":"2007","unstructured":"Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Certification of automated termination proofs. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 148\u2013162. Springer, Heidelberg (2007)"},{"key":"3_CR5","unstructured":"Demers, F.-N., Malenfant, J.: Reflection in logic, functional and object-oriented programming: A short comparative study. In: IJCAI 1995 Workshop on Reflection and Metalevel Architectures and their Applications in AI, pp. 29\u201338 (1995)"},{"key":"3_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-540-73086-6_6","volume-title":"Towards Mechanized Mathematical Assistants","author":"W.M. Farmer","year":"2007","unstructured":"Farmer, W.M.: Biform theories in Chiron. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 66\u201379. Springer, Heidelberg (2007)"},{"key":"3_CR7","unstructured":"Farmer, W.M.: Chiron: A set theory with types, undefinedness, quotation, and evaluation. SQRL Report No.\u00a038, McMaster University (2007), \n                    \n                      http:\/\/imps.mcmaster.ca\/doc\/chiron-tr.pdf\n                    \n                    \n                   (revised 2012)"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/j.jal.2007.11.001","volume":"6","author":"W.M. Farmer","year":"2008","unstructured":"Farmer, W.M.: The seven virtues of simple type theory. Journal of Applied Logic\u00a06, 267\u2013286 (2008)","journal-title":"Journal of Applied Logic"},{"key":"3_CR9","unstructured":"Farmer, W.M., Larjani, P.: Frameworks for reasoning about syntax that utilize quotation and evaluation. McSCert Report No.\u00a09, McMaster University (2013), \n                    \n                      http:\/\/imps.mcmaster.ca\/doc\/syntax.pdf"},{"key":"3_CR10","unstructured":"The F#\u00a0Software Foundation"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Grundy, J., Melham, T., O\u2019Leary, J.: A reflective functional language for hardware design and theorem proving. Journal of Functional Programming\u00a016 (2006)","DOI":"10.1017\/S0956796805005757"},{"key":"3_CR12","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge (1995), \n                    \n                      http:\/\/www.cl.cam.ac.uk\/~jrh13\/papers\/reflect.ps.gz"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.apal.2008.09.007","volume":"157","author":"P. Koellner","year":"2009","unstructured":"Koellner, P.: On reflection principles. Annals of Pure and Applied Logic\u00a0157, 206\u2013219 (2009)","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1017\/S0956796800000423","volume":"2","author":"T.\u00c6. Mogensen","year":"1994","unstructured":"Mogensen, T.\u00c6.: Efficient self-interpretation in lambda calculus. Journal of Functional Programming\u00a02, 345\u2013364 (1994)","journal-title":"Journal of Functional Programming"},{"key":"3_CR15","unstructured":"Rice University Programming Languages Team. Metaocaml: A compiled, type-safe, multi-stage programming language (2011), \n                    \n                      http:\/\/www.metaocaml.org\/"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/636517.636528","volume":"37","author":"T. Sheard","year":"2002","unstructured":"Sheard, T., Jones, S.P.: Template meta-programming for Haskell. ACM SIGPLAN Notices\u00a037, 60\u201375 (2002)","journal-title":"ACM SIGPLAN Notices"},{"key":"3_CR17","unstructured":"Spivak, M.: Calculus, 4th edn. Publish or Perish (2008)"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0304-3975(00)00053-0","volume":"248","author":"W. Taha","year":"2000","unstructured":"Taha, W., Sheard, T.: MetaML and multi-stage programming with explicit annotations. Theoretical Computer Science\u00a0248, 211\u2013242 (2000)","journal-title":"Theoretical Computer Science"},{"key":"3_CR19","unstructured":"van der Walt, P.: Reflection in Agda. Master\u2019s thesis, Universiteit Utrecht (2012)"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-540-30142-4_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 305\u2013320. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39320-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T02:12:12Z","timestamp":1557886332000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39320-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642393198","9783642393204"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39320-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}