{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:02Z","timestamp":1760202542567},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540744634"},{"type":"electronic","value":"9783540744641"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74464-1_2","type":"book-chapter","created":{"date-parts":[[2007,9,12]],"date-time":"2007-09-12T02:58:12Z","timestamp":1189565892000},"page":"18-32","source":"Crossref","is-referenced-by-count":14,"title":["Crafting a Proof Assistant"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio Sacerdoti","family":"Coen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefano","family":"Zacchiroli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/11617990_2","volume-title":"Types for Proofs and Programs","author":"A. Asperti","year":"2004","unstructured":"Asperti, A., Guidi, F., Coen, C.S., Tassi, E., Zacchiroli, S.: A content based mathematical search engine: Whelp. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 17\u201332. Springer, Heidelberg (2004)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000","author":"D. Aspinall","year":"2000","unstructured":"Aspinall, D.: Proof General: A generic tool for proof development. In: Schwartzbach, M.I., Graf, S. (eds.) ETAPS 2000 and TACAS 2000. LNCS, vol.\u00a01785, Springer, Heidelberg (2000)"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G.: Implicit coercions in type systems. In: Types for Proofs and Programs: International Workshop, TYPES 1995, pp. 1\u201315 (1995)","DOI":"10.1007\/3-540-61780-9_58"},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/s001650050049","volume":"11","author":"Y. Bertot","year":"1999","unstructured":"Bertot, Y.: The CtCoq system: Design and architecture. Formal Aspects of Computing\u00a011, 225\u2013243 (1999)","journal-title":"Formal Aspects of Computing"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Theoretical Aspects of Computer Software","author":"Y. Bertot","year":"1994","unstructured":"Bertot, Y., Kahn, G., Th\u00e9ry, L.: Proof by pointing. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol.\u00a0789, Springer, Heidelberg (1994)"},{"key":"2_CR6","unstructured":"Coscoy, Y.: Explication textuelle de preuves pour le Calcul des Constructions Inductives. PhD thesis, Universit\u00e9 de Nice-Sophia Antipolis (2000)"},{"key":"2_CR7","unstructured":"Coscoy, Y., Kahn, G., Thery, L.: Extracting Text from Proofs. Technical Report RR-2459, Inria (Institut National de Recherche en Informatique et en Automatique), France (1995)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/3-540-45793-3_36","volume-title":"Computer Science Logic","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Jojgov, G.I.: Open proofs and open terms: A basis for interactive logic. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 537\u2013552. Springer, Heidelberg (2002)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1007\/BFb0105406","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: A Mizar Mode for HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol.\u00a01125, pp. 203\u2013220. Springer, Heidelberg (1996)"},{"issue":"1","key":"2_CR10","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Luo, Z.: Coercive subtyping. Journal of Logic and Computation\u00a09(1), 105\u2013130 (1999)","journal-title":"Journal of Logic and Computation"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-58085-9_78","volume-title":"Types for Proofs and Programs","author":"L. Magnusson","year":"1994","unstructured":"Magnusson, L., Nordstr\u00f6m, B.: The ALF proof editor and its proof engine. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol.\u00a0806, pp. 213\u2013237. Springer, Heidelberg (1994)"},{"key":"2_CR12","unstructured":"Mathematical Markup Language (MathML) Version 2.0. W3C Recommendation (February 21 2001) (2003), http:\/\/www.w3.org\/TR\/MathML2"},{"key":"2_CR13","unstructured":"Mu $\\tilde{n}$ oz, C.: A Calculus of Substitutions for Incomplete-Proof Representation in Type Theory. PhD thesis, INRIA (November 1997)"},{"key":"2_CR14","unstructured":"OMDoc: An open markup format for mathematical documents (draft, version 1.2) (2005), http:\/\/www.mathweb.org\/omdoc\/pubs\/omdoc1.2.pdf"},{"key":"2_CR15","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/11812289_16","volume-title":"Proceedings of Mathematical Knowledge Management 2006","author":"L. Padovani","year":"2006","unstructured":"Padovani, L., Zacchiroli, S.: From notation to semantics: There and back again. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS (LNAI), vol.\u00a03119, pp. 194\u2013207. Springer, Heidelberg (2006)"},{"key":"2_CR16","unstructured":"Riazanov, A.: Implementing an Efficient Theorem Prover. PhD thesis, The University of Manchester (2003)"},{"key":"2_CR17","series-title":"ENTCS","first-page":"125","volume-title":"Proceedings of User Interface for Theorem Provers 2006.","author":"C.S. Coen","year":"2007","unstructured":"Coen, C.S., Tassi, E., Zacchiroli, S.: Tinycals: step by step tacticals. In: Proceedings of UITP 2006: User Interface for Theorem Provers. Seattle, WA, August 21, 2006. ENTCS, vol.\u00a0174(2), pp. 125\u2013142. Elsevier Science, North-Holland (May 2007) ISSN: 1571-0661"},{"key":"2_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1007\/978-3-540-27818-4_25","volume-title":"Mathematical Knowledge Management 2004","author":"C.S. Coen","year":"2004","unstructured":"Coen, C.S., Zacchiroli, S.: Efficient ambiguous parsing of mathematical formulae. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 347\u2013362. Springer, Heidelberg (2004)"},{"key":"2_CR19","unstructured":"Strecker, M.: Construction and Deduction in Type Theories. PhD thesis, Universit\u00e4t Ulm (1998)"},{"key":"2_CR20","unstructured":"Wiedijk, F.: Mmode, a mizar mode for the proof assistant coq. Technical Report NIII-R0333, University of Nijmegen (2003)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74464-1_2.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:30:45Z","timestamp":1619505045000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74464-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540744634","9783540744641"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74464-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}