{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T13:57:56Z","timestamp":1725890276155},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540851097"},{"type":"electronic","value":"9783540851103"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85110-3_19","type":"book-chapter","created":{"date-parts":[[2008,7,26]],"date-time":"2008-07-26T06:00:32Z","timestamp":1217052032000},"page":"232-245","source":"Crossref","is-referenced-by-count":7,"title":["High-Level Theories"],"prefix":"10.1007","author":[{"given":"Jacques","family":"Carette","sequence":"first","affiliation":[]},{"given":"William M.","family":"Farmer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-74915-8_26","volume-title":"Computer Science Logic","author":"F. Blanqui","year":"2007","unstructured":"Blanqui, F., Jouannaud, J.-P., Strub, P.-Y.: Building decision procedures in the calculus of inductive constructions. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 328\u2013342. Springer, Heidelberg (2007)"},{"key":"19_CR2","volume-title":"TCS 2008: 5th IFIP International Conference on Theoretical Computer Science","author":"F. Blanqui","year":"2008","unstructured":"Blanqui, F., Jouannaud, J.-P., Strub, P.-Y.: From formal proofs to mathematical proofs: A safe, incremental way for building in first-order decision procedures. In: TCS 2008: 5th IFIP International Conference on Theoretical Computer Science. Springer, Heidelberg (2008)"},{"key":"19_CR3","first-page":"19","volume":"39","author":"B. Buchberger","year":"1976","unstructured":"Buchberger, B.: Theoretical basis for the reduction of polynomials to canonical forms. SIGSAM Bulletin\u00a039, 19\u201324 (1976)","journal-title":"SIGSAM Bulletin"},{"key":"19_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., Craciun, A., Jebelean, T., Kovacs, L., Kutsia, T., Nakagawa, K., Piroi, F., Popov, N., Robu, J., Rosenkranz, M., Windsteiger, W.: Theorema: Towards computer-aided mathematical theory exploration. Journal of Applied Logic\u00a04, 470\u2013504 (2006)","journal-title":"Journal of Applied Logic"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2005.10.012","volume":"62","author":"J. Carette","year":"2004","unstructured":"Carette, J.: Gaussian Elimination: a case study in efficient genericity with MetaOCaml. Science of Computer Programming\u00a062(1), 3\u201324 (2004); Special Issue on the First MetaOCaml Workshop (2004)","journal-title":"Science of Computer Programming"},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1145\/1277548.1277560","volume-title":"Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation (ISSAC)","author":"J. Carette","year":"2007","unstructured":"Carette, J.: A canonical form for piecewise defined functions. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation (ISSAC), pp. 77\u201384. ACM Press, New York (2007)"},{"key":"19_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-540-73086-6_2","volume-title":"Towards Mechanized Mathematical Assistants","author":"J. Carette","year":"2007","unstructured":"Carette, J., Farmer, W.M., Sorge, V.: A rational reconstruction of a system for experimental mathematics. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM\/CALCULEMUS 2007. LNCS (LNAI), vol.\u00a04573, pp. 13\u201326. Springer, Heidelberg (2007)"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Carette, J., Kiselyov, O.: Multi-stage programming with Functors and Monads: eliminating abstraction overhead from generic code (accepted, 2008); Special issue for GPCE 2004 and 2005","DOI":"10.1007\/11561347_18"},{"key":"19_CR9","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual, Version 7.4 (2003), http:\/\/pauillac.inria.fr\/coq\/doc\/main.html"},{"key":"19_CR10","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.: The calculus of constructions. Information and Computation\u00a076, 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 50\u201366. Springer, Heidelberg (1990)"},{"key":"19_CR12","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/978-3-642-81955-1_11","volume-title":"Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970","author":"N.G. Bruijn de","year":"1983","unstructured":"de Bruijn, N.G.: Automath, a language for mathematics. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pp. 159\u2013200. Springer, Heidelberg (1983)"},{"issue":"1","key":"19_CR13","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. J. Autom. Reasoning\u00a031(1), 33\u201372 (2003)","journal-title":"J. Autom. Reasoning"},{"key":"19_CR14","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"2000","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, London (2000)","edition":"2"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-58233-9_6","volume-title":"Higher-Order Algebra, Logic, and Term Rewriting","author":"W.M. Farmer","year":"1994","unstructured":"Farmer, W.M.: Theory interpretation in simple type theory. In: Heering, J., et al. (eds.) HOA 1993. LNCS, vol.\u00a0816, pp. 96\u2013123. Springer, Heidelberg (1994)"},{"key":"19_CR16","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":"19_CR17","unstructured":"Farmer, W.M.: Chiron: A multi-paradigm logic. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, vol.\u00a010(23), pp. 1\u201319, University of Bia\u0142ystok (2007)"},{"key":"19_CR18","unstructured":"Farmer, W.M.: Chiron: A set theory with types, undefinedness, quotation, and evaluation. SQRL Report No.\u00a038, McMaster University (2007) (revised 2008)"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/3-540-55602-8_192","volume-title":"Automated Deduction - CADE-11","author":"W.M. Farmer","year":"1992","unstructured":"Farmer, W.M., Guttman, J.D., Thayer, F.J.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 567\u2013581. Springer, Heidelberg (1992)"},{"key":"19_CR20","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1023\/A:1022971915900","volume":"38","author":"W.M. Farmer","year":"2003","unstructured":"Farmer, W.M., von Mohrenschildt, M.: An overview of a formal framework for managing mathematics. Annals of Mathematics and Artificial Intelligence\u00a038, 165\u2013191 (2003)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"19_CR21","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/978-3-7091-6510-2_12","volume-title":"Relational Methods in Computer Science","author":"R. Janicki","year":"1997","unstructured":"Janicki, R., Parnas, D.L., Zucker, J.: Tabular representations in relational documents. In: Brink, C., Kahl, W., Schmidt, G. (eds.) Relational Methods in Computer Science, pp. 184\u2013196. Springer, Heidelberg (1997)"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Wiedijk, F.: Certified computer algebra on top of an interactive theorem prover. In: Calculemus\/MKM, pp. 94\u2013105 (2007)","DOI":"10.1007\/978-3-540-73086-6_8"},{"key":"19_CR23","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebra. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"19_CR24","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2005.11.021","volume":"151","author":"R.L. McCasland","year":"2006","unstructured":"McCasland, R.L., Bundy, A., Smith, P.F.: Ascertaining mathematical theorems. Electronic Notes in Theoretical Computer Science\u00a0151, 21\u201338 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"19_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: Combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"key":"19_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"19_CR27","series-title":"Internationales Begegnungs- und Forschungszentrum (IBFI)","volume-title":"Dagstuhl Seminar Proceedings of Mathematics, Algorithms, Proofs","author":"V. Prevosto","year":"2005","unstructured":"Prevosto, V.: Certified mathematical hierarchies: The FoCal system. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Dagstuhl Seminar Proceedings of Mathematics, Algorithms, Proofs, Dagstuhl, Germany. Internationales Begegnungs- und Forschungszentrum (IBFI), vol.\u00a005021. Schloss Dagstuhl, Germany (2005)"},{"key":"19_CR28","unstructured":"Rudnicki, P.: An overview of the MIZAR project. Technical report, Department of Computing Science, University of Alberta (1992)"},{"key":"19_CR29","unstructured":"Xu, J.: Mei \u2014 A module system for mechanized mathematics systems. In: Programming Languages for Mechanized Mathematics Workshop, Hagenberg, Austria (2007)"},{"key":"19_CR30","unstructured":"Xu, J.: Mei \u2014 A Module System for Mechanized Mathematics Systems. PhD thesis, McMaster University (January 2008)"}],"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-540-85110-3_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:14:42Z","timestamp":1619522082000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85110-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540851097","9783540851103"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85110-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}