{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:21:09Z","timestamp":1784233269281,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642141270","type":"print"},{"value":"9783642141287","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_5","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T10:45:36Z","timestamp":1277808336000},"page":"34-48","source":"Crossref","is-referenced-by-count":2,"title":["Structured Formal Development with Quotient Types in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Maksym","family":"Bortin","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christoph","family":"L\u00fcth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","volume-title":"Algebra of Programing","author":"R. Bird","year":"1997","unstructured":"Bird, R., de Moor, O.: Algebra of Programing. Prentice Hall, Englewood Cliffs (1997)"},{"key":"5_CR2","first-page":"2","volume":"13","author":"M. Bortin","year":"2006","unstructured":"Bortin, M., Johnsen, E.B., L\u00fcth, C.: Structured formal development in Isabelle. Nordic Journal of Computing\u00a013, 2\u201321 (2006)","journal-title":"Nordic Journal of Computing"},{"key":"5_CR3","unstructured":"Burstall, R.M., Goguen, J.A.: Putting theories together to make specifications. In: Proc. Fifth International Joint Conference on Artificial Intelligence IJCAI 1977, pp. 1045\u20131058 (1977)"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1007\/3-540-10007-5_41","volume-title":"Abstract Software Specifications","author":"R.M. Burstall","year":"1980","unstructured":"Burstall, R.M., Goguen, J.A.: The semantics of CLEAR, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol.\u00a086, pp. 292\u2013332. Springer, Heidelberg (1980)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-39185-1_6","volume-title":"Types for Proofs and Programs","author":"L. Chicli","year":"2003","unstructured":"Chicli, L., Pottier, L., Simpson, C.: Mathematical quotients and quotient types in Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 95\u2013107. Springer, Heidelberg (2003)"},{"key":"5_CR6","doi-asserted-by":"crossref","DOI":"10.1142\/3831","volume-title":"CafeOBJ Report","author":"R. Diaconescu","year":"1998","unstructured":"Diaconescu, R., Futatsugi, K.: CafeOBJ Report. World Scientific, Singapore (1998)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1007\/3-540-60117-1_14","volume-title":"Mathematics of Program Construction","author":"H. Doornbos","year":"1995","unstructured":"Doornbos, H., Backhouse, R.C.: Induction and recursion on datatypes. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol.\u00a0947, pp. 242\u2013256. Springer, Heidelberg (1995)"},{"key":"5_CR8","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":"5_CR9","unstructured":"Goguen, J.A.: A categorical manifesto. Tech. Rep. PRG-72, Oxford University Computing Laboratory, Programming Research Group, Oxford, England (1989)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/BFb0014055","volume-title":"Typed Lambda Calculi and Applications","author":"M. Hofmann","year":"1995","unstructured":"Hofmann, M.: A simple model for quotient types. In: Dezani-Ciancaglini, M., Plotkin, G. (eds.) TLCA 1995. LNCS, vol.\u00a0902, pp. 216\u2013234. Springer, Heidelberg (1995)"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(96)00068-0","volume":"167","author":"M. Hofmann","year":"1996","unstructured":"Hofmann, M., Sannella, D.: On behavioural abstraction and behavioural satisfaction in higher-order logic. Theoretical Computer Science\u00a0167, 3\u201345 (1996)","journal-title":"Theoretical Computer Science"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/11541868_9","volume-title":"Theorem Proving in Higher Order Logics","author":"P.V. Homeier","year":"2005","unstructured":"Homeier, P.V.: A design structure for higher order quotients. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 130\u2013146. Springer, Heidelberg (2005)"},{"issue":"1-2","key":"5_CR13","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1016\/j.jlap.2005.09.005","volume":"67","author":"T. Mossakowski","year":"2006","unstructured":"Mossakowski, T., Autexier, S., Hutter, D.: Development graphs \u2014 proof management for structured specifications. Journal of Logic and Algebraic Programming\u00a067(1-2), 114\u2013145 (2006)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"CASL Reference Manual","year":"2004","unstructured":"Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol.\u00a02960. Springer, Heidelberg (2004)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"5_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/3-540-45685-6_18","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Nogin","year":"2002","unstructured":"Nogin, A.: Quotient types: A modular approach. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 263\u2013280. Springer, Heidelberg (2002)"},{"issue":"4","key":"5_CR17","doi-asserted-by":"crossref","first-page":"658","DOI":"10.1145\/1183278.1183280","volume":"7","author":"L.C. Paulson","year":"2006","unstructured":"Paulson, L.C.: Defining functions on equivalence classes. ACM Trans. Comput. Log.\u00a07(4), 658\u2013675 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/3-540-12727-5_24","volume-title":"CAAP 1983","author":"D. Sannella","year":"1983","unstructured":"Sannella, D., Burstall, R.: Structured theories in LCF. In: Protasi, M., Ausiello, G. (eds.) CAAP 1983. LNCS, vol.\u00a0159, pp. 377\u2013391. Springer, Heidelberg (1983)"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/BFb0028401","volume-title":"Theorem Proving in Higher Order Logics","author":"O. Slotosch","year":"1997","unstructured":"Slotosch, O.: Higher order quotients and their implementation in Isabelle\/HOL. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 291\u2013306. Springer, Heidelberg (1997)"},{"key":"5_CR20","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0167-6423(90)90025-9","volume":"14","author":"D.R. Smith","year":"1990","unstructured":"Smith, D.R., Lowry, M.R.: Algorithm theories and design tactics. Science of Computer Programming\u00a014, 305\u2013321 (1990)","journal-title":"Science of Computer Programming"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Mathematics of Program Construction","author":"Y.V. Srinivas","year":"1995","unstructured":"Srinivas, Y.V., Jullig, R.: Specware: Formal support for composing software. In: M\u00f6ller, B. (ed.) MPC 1995. LNCS, vol.\u00a0947, Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:19:15Z","timestamp":1619785155000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}