{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T06:04:28Z","timestamp":1726034668742},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030232498"},{"type":"electronic","value":"9783030232504"}],"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-23250-4_8","type":"book-chapter","created":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T07:01:17Z","timestamp":1562050877000},"page":"109-124","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards Specifying Symbolic Computation"],"prefix":"10.1007","author":[{"given":"Jacques","family":"Carette","sequence":"first","affiliation":[]},{"given":"William M.","family":"Farmer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,7,3]]},"reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-94821-8_2","volume-title":"Interactive Theorem Proving","author":"A Anand","year":"2018","unstructured":"Anand, A., Boulier, S., Cohen, C., Sozeau, M., Tabareau, N.: Towards certified meta-programming with typed Template-Coq. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 20\u201339. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-94821-8_2"},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-1-4613-9647-5_25","volume-title":"Computers and Mathematics","author":"M Beeson","year":"1989","unstructured":"Beeson, M.: Logic and computation in MATHPERT: an expert system for learning mathematics. In: Kaltofen, E., Watt, S. (eds.) Computers and Mathematics, pp. 202\u2013214. Springer, New York (1989). \n                    https:\/\/doi.org\/10.1007\/978-1-4613-9647-5_25"},{"key":"8_CR3","first-page":"103","volume-title":"The Correctness Problem in Computer Science","author":"R Boyer","year":"1981","unstructured":"Boyer, R., Moore, J.: Metafunctions: proving them correct and using them efficiently as new proof procedures. In: Boyer, R., Moore, J. (eds.) The Correctness Problem in Computer Science, pp. 103\u2013185. Academic Press, Cambridge (1981)"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1016\/j.jal.2005.10.006","volume":"4","author":"B Buchberger","year":"2006","unstructured":"Buchberger, B., et al.: Theorema: towards computer-aided mathematical theory exploration. J. Appl. Log. 4, 470\u2013504 (2006)","journal-title":"J. Appl. Log."},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-319-94821-8_13","volume-title":"Interactive Theorem Proving","author":"J Carette","year":"2018","unstructured":"Carette, J., Farmer, W.M., Laskowski, P.: HOL light QE. In: Avigad, J., Mahboubi, A. (eds.) ITP 2018. LNCS, vol. 10895, pp. 215\u2013234. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-94821-8_13"},{"key":"8_CR6","doi-asserted-by":"publisher","unstructured":"Christiansen, D.R.: Type-directed elaboration of quasiquotations: a high-level syntax for low-level reflection. In: Proceedings of the 26th 2014 International Symposium on Implementation and Application of Functional Languages, IFL 2014, pp. 1:1\u20131:9. ACM, New York (2014). \n                    https:\/\/doi.org\/10.1145\/2746325.2746326","DOI":"10.1145\/2746325.2746326"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Dunstan, M., Kelsey, T., Linton, S., Martin, U.: Lightweight formal methods for computer algebra systems. In: Weispfenning, V., Trager, B.M. (eds.) Proceedings of the 1998 International Symposium on Symbolic and Algebraic Computation, pp. 80\u201387. ACM (1998)","DOI":"10.1145\/281508.281560"},{"issue":"ICFP","key":"8_CR8","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/3110278","volume":"1","author":"G Ebner","year":"2017","unstructured":"Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. Proc. ACM Program. Lang. 1(ICFP), 34 (2017)","journal-title":"Proc. ACM Program. Lang."},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/0168-0072(93)90144-3","volume":"64","author":"WM Farmer","year":"1993","unstructured":"Farmer, W.M.: A simple type theory with partial functions and subtypes. Ann. Pure Appl. Log. 64, 211\u2013240 (1993)","journal-title":"Ann. Pure Appl. Log."},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-25984-8_35","volume-title":"Automated Reasoning","author":"WM Farmer","year":"2004","unstructured":"Farmer, W.M.: Formalizing undefinedness arising in calculus. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 475\u2013489. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-25984-8_35"},{"key":"8_CR11","unstructured":"Farmer, W.M.: Andrews\u2019 type system with undefinedness. In: Benzm\u00fcller, C., Brown, C., Siekmann, J., Statman, R. (eds.) Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on his 70th Birthday, pp. 223\u2013242. Studies in Logic, College Publications (2008)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-62075-6_11","volume-title":"Intelligent Computer Mathematics","author":"WM Farmer","year":"2017","unstructured":"Farmer, W.M.: Theory morphisms in Church\u2019s type theory with quotation and evaluation. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) CICM 2017. LNCS (LNAI), vol. 10383, pp. 147\u2013162. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-62075-6_11"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1016\/j.ic.2018.03.001","volume":"260","author":"WM Farmer","year":"2018","unstructured":"Farmer, W.M.: Incorporating quotation and evaluation into Church\u2019s type theory. Inf. Comput. 260, 9\u201350 (2018)","journal-title":"Inf. Comput."},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 60\u201366. Springer, Heidelberg (2009). \n                    https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-540-85110-3_26","volume-title":"Intelligent Computer Mathematics","author":"C Kaliszyk","year":"2008","unstructured":"Kaliszyk, C.: Automating side conditions in formalized partial functions. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) CICM 2008. LNCS (LNAI), vol. 5144, pp. 300\u2013314. Springer, Heidelberg (2008). \n                    https:\/\/doi.org\/10.1007\/978-3-540-85110-3_26"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-540-73086-6_8","volume-title":"Towards Mechanized Mathematical Assistants","author":"C Kaliszyk","year":"2007","unstructured":"Kaliszyk, C., Wiedijk, F.: Certified Computer Algebra on Top of an Interactive Theorem Prover. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus\/MKM -2007. LNCS (LNAI), vol. 4573, pp. 94\u2013105. Springer, Heidelberg (2007). \n                    https:\/\/doi.org\/10.1007\/978-3-540-73086-6_8"},{"key":"8_CR17","unstructured":"Khan, M.T.: Formal specification and verification of computer algebra software. Ph.D. thesis, RISC, Johannes Kepler Universit\u00e4t Linz (2014)"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-642-31374-5_16","volume-title":"Intelligent Computer Mathematics","author":"MT Khan","year":"2012","unstructured":"Khan, M.T., Schreiner, W.: Towards the formal specification and verification of maple programs. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 231\u2013247. Springer, Heidelberg (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-31374-5_16"},{"key":"8_CR19","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/0304-3975(92)90167-E","volume":"104","author":"C Limongelli","year":"1992","unstructured":"Limongelli, C., Temperini, M.: Abstract specification of structures and methods in symbolic mathematical computation. Theor. Comput. Sci. 104, 89\u2013107 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR20","unstructured":"Melham, T., Cohn, R., Childs, I.: On the semantics of ReFLect as a basis for a reflective theorem prover. Computing Research Repository (CoRR) abs\/1309.5742 (2013). \n                    arxiv:1309.5742"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-41582-1_10","volume-title":"Implementation and Application of Functional Languages","author":"P Walt van der","year":"2013","unstructured":"van der Walt, P., Swierstra, W.: Engineering proof by reflection in agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157\u2013173. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-41582-1_10"},{"key":"8_CR22","unstructured":"Watt, S.M.: Making computer algebra more symbolic. In: Proceedings of Transgressive Computing 2006, Granada, Spain, pp. 43\u201349 (2006)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-23250-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,2]],"date-time":"2019-07-02T07:04:20Z","timestamp":1562051060000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-23250-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030232498","9783030232504"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-23250-4_8","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":"3 July 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","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":"8 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2019\/cicm.php?event=&menu=general","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}