{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:48:46Z","timestamp":1740098926412,"version":"3.37.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319620749"},{"type":"electronic","value":"9783319620756"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-62075-6_4","type":"book-chapter","created":{"date-parts":[[2017,6,27]],"date-time":"2017-06-27T10:58:50Z","timestamp":1498561130000},"page":"40-55","source":"Crossref","is-referenced-by-count":1,"title":["Automatically Proving Equivalence by Type-Safe Reflection"],"prefix":"10.1007","author":[{"given":"Franck","family":"Slama","sequence":"first","affiliation":[]},{"given":"Edwin","family":"Brady","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,6,28]]},"reference":[{"key":"4_CR1","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","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. An EATCS Series. Springer, Heidelberg (2004)"},{"key":"4_CR2","unstructured":"Brady, E.: Constructing correct circuits: verification of functional aspects of hardware specifications with dependent types. In: Trends in Functional Programming (TFP 2007) (2007)"},{"key":"4_CR3","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1017\/S095679681300018X","volume":"23","author":"E Brady","year":"2013","unstructured":"Brady, E.: Idris, a general-purpose dependently typed programming language: design and implementation. J. Funct. Program. 23, 552\u2013593 (2013)","journal-title":"J. Funct. Program."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-31374-5_14","volume-title":"Intelligent Computer Mathematics","author":"J Carette","year":"2012","unstructured":"Carette, J., O\u2019Connor, R.: Theory presentation combinators. In: Jeuring, J., Campbell, J.A., Carette, J., Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS, vol. 7362, pp. 202\u2013215. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31374-5_14"},{"key":"4_CR5","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)"},{"key":"4_CR6","unstructured":"Cr\u00e9gut, P.: Une proc\u00e9dure de d\u00e9cision reflexive pour un fragment de l\u2019arithm\u00e9tique de Presburger. In: Journ\u00e9es Francophones des Langages Applicatifs (2004)"},{"issue":"2","key":"4_CR7","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/S1571-0661(04)80508-5","volume":"70","author":"D Delahaye","year":"2002","unstructured":"Delahaye, D.: A proof dedicated meta-language. Electr. Notes Theor. Comput. Sci. 70(2), 96\u2013109 (2002)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-45221-5_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Delahaye","year":"2013","unstructured":"Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: when achilles outruns the tortoise using deduction modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013. LNCS, vol. 8312, pp. 274\u2013290. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-45221-5_20"},{"key":"4_CR9","unstructured":"Delahaye, D., Mayero, M.: Field, une proc\u00e9dure de d\u00e9cision pour les nombres r\u00e9els en Coq. In: Cast\u00e9ran, P. (ed.) Journ\u00e9es francophones des langages applicatifs (JFLA\u201901), pp. 33\u201348. Collection Didactique, INRIA (2001)"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reasoning 31(1), 33\u201372 (2003). http:\/\/dx.doi.org\/10.1023\/A:1027357912519","DOI":"10.1023\/A:1027357912519"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-642-39320-4_3","volume-title":"Intelligent Computer Mathematics","author":"WM Farmer","year":"2013","unstructured":"Farmer, W.M.: The formalization of syntax-based mathematical algorithms using quotation and evaluation. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) CICM 2013. LNCS, vol. 7961, pp. 35\u201350. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39320-4_3"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Gregoire, B., Mahboubi, A.: Proving equalities in a commutative ring done right in Coq. In: Theorem Proving in Higher Order Logics (TPHOLS 2005), pp. 98\u2013113 (2005)","DOI":"10.1007\/11541868_7"},{"key":"4_CR13","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"W Howard","year":"1980","unstructured":"Howard, W.: The formulae-as-types notion of construction. In: Seldin, J., Hindley, J. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, London (1980)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Kokke, P., Swierstra, W.: Auto in Agda \u2013 programming proof search using reflection. In: 12th International Conference on Mathematics of Program Construction, MPC 2015, pp. 276\u2013301 (2015)","DOI":"10.1007\/978-3-319-19797-5_14"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/11617990_10","volume-title":"Types for Proofs and Programs","author":"F Lindblad","year":"2006","unstructured":"Lindblad, F., Benke, M.: A tool for automated theorem proving in Agda. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 154\u2013169. Springer, Heidelberg (2006). doi: 10.1007\/11617990_10"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Malecha, G., Chlipala, A., Braibant, T.: Compositional computational reflection. In: 5th International Conference on Interactive Theorem Proving, ITP 2014, pp. 374\u2013389 (2014)","DOI":"10.1007\/978-3-319-08970-6_24"},{"key":"4_CR17","unstructured":"Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology (2007)"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, pp. 87\u2013100 (2013)","DOI":"10.1145\/2500365.2500579"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-62075-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,27]],"date-time":"2019-09-27T02:24:19Z","timestamp":1569551059000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-62075-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319620749","9783319620756"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-62075-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}