{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T01:14:16Z","timestamp":1769303656293,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642313738","type":"print"},{"value":"9783642313745","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31374-5_2","type":"book-chapter","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:00:57Z","timestamp":1340629257000},"page":"17-31","source":"Crossref","is-referenced-by-count":1,"title":["Proof, Message and Certificate"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-642-22673-1_10","volume-title":"Intelligent Computer Mathematics","author":"J. Alama","year":"2011","unstructured":"Alama, J., Brink, K., Mamane, L., Urban, J.: Large Formal Wikis: Issues and Solutions. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus\/MKM 2011. LNCS, vol.\u00a06824, pp. 133\u2013148. Springer, Heidelberg (2011)"},{"key":"2_CR2","first-page":"1","volume":"1","author":"A. Asperti","year":"2008","unstructured":"Asperti, A., Armentano, C.: A page in number theory. Journal of Formalized Reasoning\u00a01, 1\u201323 (2008)","journal-title":"Journal of Formalized Reasoning"},{"issue":"4","key":"2_CR3","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1017\/S0960129511000065","volume":"21","author":"A. Asperti","year":"2011","unstructured":"Asperti, A., Avigad, J.: Zen and the art of formalization. Mathematical Structures in Computer Science\u00a021(4), 679\u2013682 (2011)","journal-title":"Mathematical Structures in Computer Science"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-642-14128-7_13","volume-title":"Intelligent Computer Mathematics","author":"A. Asperti","year":"2010","unstructured":"Asperti, A., Sacerdoti Coen, C.: Some Considerations on the Usability of Interactive Provers. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 147\u2013156. Springer, Heidelberg (2010)"},{"issue":"5","key":"2_CR5","doi-asserted-by":"publisher","first-page":"877","DOI":"10.1017\/S0960129509990041","volume":"19","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Geuvers, H., Natarajan, R.: Social processes, program verification and all that. Mathematical Structures in Computer Science\u00a019(5), 877\u2013896 (2009)","journal-title":"Mathematical Structures in Computer Science"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-642-02444-3_2","volume-title":"Types for Proofs and Programs","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W.: About the Formalization of Some Results by Chebyshev in Number Theory. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 19\u201331. Springer, Heidelberg (2009)"},{"key":"2_CR7","series-title":"LNAI","first-page":"417","volume-title":"CICM 2012","author":"A. Asperti","year":"2012","unstructured":"Asperti, A., Ricciotti, W.: A Web Interface for Matita. In: Jeuring, J., et al. (eds.) CICM 2012. LNCS (LNAI), vol.\u00a07362, pp. 417\u2013421. Springer, Heidelberg (2012)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-22438-6_7","volume-title":"Automated Deduction \u2013 CADE-23","author":"A. Asperti","year":"2011","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: The Matita Interactive Theorem Prover. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 64\u201369. Springer, Heidelberg (2011)"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.53.1","volume":"53","author":"A. Asperti","year":"2011","unstructured":"Asperti, A., Tassi, E.: Superposition as a logical glue. EPTCS\u00a053, 1\u201315 (2011)","journal-title":"EPTCS"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. ACM Trans. Comput. Log.\u00a09(1) (2007)","DOI":"10.1145\/1297658.1297660"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Barendregt, H.: Towards an interactive mathematical proof language. In: Kamareddine, F. (ed.) Thirty Five Years of Automath, pp. 25\u201336. Kluwer (2003)","DOI":"10.1007\/978-94-017-0253-9_2"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical Big Operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"key":"2_CR13","doi-asserted-by":"publisher","first-page":"221","DOI":"10.2307\/2305937","volume":"57","author":"N. Bourbaki","year":"1950","unstructured":"Bourbaki, N.: The architecture of mathematics. Monthly\u00a057, 221\u2013232 (1950)","journal-title":"Monthly"},{"key":"2_CR14","unstructured":"Bourbaki, N.: Theory of Sets. Elements of mathematics. Addison Wesley (1968)"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S. Boutin","year":"1997","unstructured":"Boutin, S.: Using Reflection to Build Efficient and Certified Decision Procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg (1997)"},{"key":"2_CR16","unstructured":"De Bruijn, N.G.: Memories of the automath project. Invited Lecture at the Mathematics Knowledge Management Symposium, November 25-29. Heriot-Watt University, Edinburgh (2003)"},{"issue":"5","key":"2_CR17","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1145\/359104.359106","volume":"22","author":"R.A. De Millo","year":"1979","unstructured":"De Millo, R.A., Lipton, R.J., Perlis, A.J.: Social processes and proofs of theorems and programs. Commun. ACM\u00a022(5), 271\u2013280 (1979)","journal-title":"Commun. ACM"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging Mathematical Structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009)"},{"issue":"1","key":"2_CR19","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s12046-009-0001-5","volume":"34","author":"H. Geuvers","year":"2009","unstructured":"Geuvers, H.: Proof Assistants: history, ideas and future. Sadhana\u00a034(1), 3\u201325 (2009)","journal-title":"Sadhana"},{"issue":"2","key":"2_CR20","first-page":"95","volume":"3","author":"G. Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in coq. Journal of Formalized Reasoning\u00a03(2), 95\u2013152 (2010)","journal-title":"Journal of Formalized Reasoning"},{"key":"2_CR21","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof \u2013 the four color theorem. Notices of the American Mathematical Society\u00a055, 1382\u20131394 (2008)","journal-title":"Notices of the American Mathematical Society"},{"key":"2_CR22","first-page":"1","volume":"38","author":"G.H. Hardy","year":"1928","unstructured":"Hardy, G.H.: Mathematical proof. Mind\u00a038, 1\u201325 (1928)","journal-title":"Mind"},{"key":"2_CR23","volume-title":"A Mathematician\u2019s Apology","author":"G.H. Hardy","year":"1940","unstructured":"Hardy, G.H.: A Mathematician\u2019s Apology. Cambridge University Press, London (1940)"},{"key":"2_CR24","first-page":"1395","volume":"55","author":"J. Harrison","year":"2008","unstructured":"Harrison, J.: Formal proof \u2013 theory and practice. Notices of the American Mathematical Society\u00a055, 1395\u20131406 (2008)","journal-title":"Notices of the American Mathematical Society"},{"issue":"3","key":"2_CR25","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1511\/2003.44.200","volume":"4","author":"B. Hayes","year":"2006","unstructured":"Hayes, B.: Gauss\u2019s day of reckoning. American Scientist\u00a04(3), 200\u2013207 (2006)","journal-title":"American Scientist"},{"key":"2_CR26","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"W.A. Howard","year":"1980","unstructured":"Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479\u2013490. Academic Press, Boston (1980)"},{"key":"2_CR27","unstructured":"Ireland, K., Rosen, M.: A Classical Introduction to Modern Number Theory. Springer (2006)"},{"key":"2_CR28","volume-title":"Mathematical Reasoning with Diagrams: from intuition to automation","author":"M. Jamnik","year":"2001","unstructured":"Jamnik, M.: Mathematical Reasoning with Diagrams: from intuition to automation. CSLI Press, Stanford (2001)"},{"issue":"2","key":"2_CR29","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.entcs.2006.09.021","volume":"174","author":"C. Kaliszyk","year":"2007","unstructured":"Kaliszyk, C.: Web interfaces for proof assistants. Electr. Notes Theor. Comput. Sci.\u00a0174(2), 49\u201361 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-14128-7_30","volume-title":"Intelligent Computer Mathematics","author":"M. Kerber","year":"2010","unstructured":"Kerber, M.: Proofs, Proofs, Proofs, and Proofs. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 345\u2013354. Springer, Heidelberg (2010)"},{"key":"2_CR31","unstructured":"Knuth, D.E.: Literate Programming. Center for the Study of Language and Information (1992)"},{"key":"2_CR32","doi-asserted-by":"crossref","unstructured":"Lakatos, I.: Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press (1976)","DOI":"10.1017\/CBO9781139171472"},{"key":"2_CR33","doi-asserted-by":"publisher","first-page":"624","DOI":"10.1145\/359156.359160","volume":"22","author":"L. Lamport","year":"1979","unstructured":"Lamport, L.: Letter to the editor. Communications of the ACM\u00a022, 624 (1979)","journal-title":"Communications of the ACM"},{"key":"2_CR34","unstructured":"Lee, J.K.: Philosophical perspectives on proof in mathematics education. Philosophy of Mathematics Education Journal\u00a016 (2002)"},{"issue":"5714","key":"2_CR35","first-page":"1402","volume":"207","author":"D. MacKenzie","year":"2005","unstructured":"MacKenzie, D.: What in the name of Euclid is going on here? Science\u00a0207(5714), 1402\u20131403 (2005)","journal-title":"Science"},{"key":"2_CR36","doi-asserted-by":"crossref","unstructured":"Mackenzie, D.: Mechanizing Proof. MIT Press (2001)","DOI":"10.7551\/mitpress\/4529.001.0001"},{"key":"2_CR37","unstructured":"Nelsen, R.B.: Proofs without Words: Exercises in Visual Thinking. The Mathematical Association of America (1997)"},{"key":"2_CR38","doi-asserted-by":"crossref","unstructured":"Coen, C.S., Tassi, E., Zacchiroli, S.: Tinycals: step by step tacticals. In: Proceedings of User Interface for Theorem Provers 2006. Electronic Notes in Theoretical Computer Science, vol.\u00a0174, pp. 125\u2013142. Elsevier Science (2006)","DOI":"10.1016\/j.entcs.2006.09.026"},{"key":"2_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-642-14128-7_37","volume-title":"Intelligent Computer Mathematics","author":"C. Tankink","year":"2010","unstructured":"Tankink, C., Geuvers, H., McKinna, J., Wiedijk, F.: Proviola: A Tool for Proof Re-animation. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 440\u2013454. Springer, Heidelberg (2010)"},{"key":"2_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-14128-7_38","volume-title":"Intelligent Computer Mathematics","author":"J. Urban","year":"2010","unstructured":"Urban, J., Alama, J., Rudnicki, P., Geuvers, H.: A Wiki for Mizar: Motivation, Considerations, and Initial Prototype. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC 2010. LNCS, vol.\u00a06167, pp. 455\u2013469. Springer, Heidelberg (2010)"},{"key":"2_CR41","volume-title":"7th Dutch Proof Tools Day, Program + Proceedings","author":"F. Wiedijk","year":"2003","unstructured":"Wiedijk, F.: Formal proof sketches. In: Fokkink, W., van de Pol, J. (eds.) 7th Dutch Proof Tools Day, Program + Proceedings. CWI, Amsterdam (2003)"},{"key":"2_CR42","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"The Seventeen Provers of the World","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31374-5_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T02:41:26Z","timestamp":1676774486000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-31374-5_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313738","9783642313745"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31374-5_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}