{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:31:14Z","timestamp":1725489074101},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540730835"},{"type":"electronic","value":"9783540730866"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73086-6_22","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T10:57:56Z","timestamp":1187089076000},"page":"265-279","source":"Crossref","is-referenced-by-count":1,"title":["Formal Representation of Mathematics in a Dependently Typed Set Theory"],"prefix":"10.1007","author":[{"given":"Feryal Fulya","family":"Horozal","sequence":"first","affiliation":[]},{"given":"Chad E.","family":"Brown","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/11618027_7","volume-title":"Mathematical Knowledge Management","author":"S. Autexier","year":"2006","unstructured":"Autexier, S., Fiedler, A.: Textbook proofs meet formal logic - the problem of underspecification and granularity. In: Kohlhase, M. (ed.) MKM 2005. LNCS (LNAI), vol.\u00a03863, pp. 96\u2013110. Springer, Heidelberg (2006)"},{"key":"22_CR2","volume-title":"Introduction to Real Analysis","author":"R.G. Bartle","year":"1982","unstructured":"Bartle, R.G., Sherbert, D.R.: Introduction to Real Analysis. John Wiley and Sons, New York (1982)"},{"key":"22_CR3","unstructured":"Baur, J.: Syntax und semantik mathematischer texte. Diploma thesis, Saarland University, Saarbr\u00fccken, Germany (1999)"},{"key":"22_CR4","series-title":"An EATCS Series","volume-title":"Texts in Theoretical Computer Science","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2004)"},{"key":"22_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/11814771_19","volume-title":"Automated Reasoning","author":"E.C. Brown","year":"2006","unstructured":"Brown, E.C.: Combining Type Theory and Untyped Set Theory. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 205\u2013219. Springer, Heidelberg (2006)"},{"key":"22_CR6","unstructured":"Brown, C.E.: Encoding functional relations in Scunak. In: LFMTP 2006 (September 2006)"},{"key":"22_CR7","unstructured":"Brown, C.E.: Scunak users manual (2006), \n                    \n                      http:\/\/gtps.math.cmu.edu\/cebrown\/manual.ps"},{"key":"22_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/11812289_10","volume-title":"Mathematical Knowledge Management","author":"C.E. Brown","year":"2006","unstructured":"Brown, C.E.: Verifying and invalidating textbook proofs using scunak. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol.\u00a04108, pp. 110\u2013123. Springer, Heidelberg (2006)"},{"key":"22_CR9","unstructured":"Brown, C.E.: Dependently Typed Set Theory. SEKI-Working-Paper SWP\u20132006\u201303, SEKI Publications, Saarland Univ., (2006) ISSN 1860\u20135931"},{"key":"22_CR10","unstructured":"Kotowicz, J.: Real sequences and basic operations on them. Journal of Formalized Mathematics 1 (1989)"},{"key":"22_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4872-9","volume-title":"Mathematics, Form, and Function","author":"S.M. Lane","year":"1986","unstructured":"Lane, S.M.: Mathematics, Form, and Function. Springer, Heidelberg (1986)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"22_CR13","unstructured":"Reed, J.: Proof irrelevance and strict definitions in a logical framework. Technical Report 02-153, School of Computer Science, Carnegie Mellon University (2002)"},{"key":"22_CR14","unstructured":"Rudnicki, P.: An overview of the mizar project. In: Workshop on Types for Proofs and Programs, pp. 311\u2013332 (1992)"},{"key":"22_CR15","unstructured":"Wiedijk, F.: Mizar: An impression, \n                    \n                      http:\/\/www.cs.kun.nl\/~freek\/mizar\/mizarmanual.ps.gz"}],"container-title":["Lecture Notes in Computer Science","Towards Mechanized Mathematical Assistants"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73086-6_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:59:45Z","timestamp":1619517585000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73086-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540730835","9783540730866"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73086-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}