{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T19:20:10Z","timestamp":1743016810881,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642284113"},{"type":"electronic","value":"9783642284120"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28412-0_9","type":"book-chapter","created":{"date-parts":[[2012,2,18]],"date-time":"2012-02-18T09:14:28Z","timestamp":1329556468000},"page":"118-138","source":"Crossref","is-referenced-by-count":1,"title":["A Proof Theoretic Interpretation of Model Theoretic Hiding"],"prefix":"10.1007","author":[{"given":"Mihai","family":"Codescu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fulya","family":"Horozal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Till","family":"Mossakowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-540-44616-3_5","volume-title":"Recent Trends in Algebraic Development Techniques","author":"S. Autexier","year":"2000","unstructured":"Autexier, S., Hutter, D., Mantel, H., Schairer, A.: Towards an Evolutionary Formal Software-Development Using CASL. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol.\u00a01827, pp. 73\u201388. Springer, Heidelberg (2000)"},{"key":"9_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59851-7","volume-title":"Algebraic Foundations of Systems Specification","author":"E. Astesiano","year":"1999","unstructured":"Astesiano, E., Kreowski, H.-J., Krieg-Br\u00fcckner, B.: Algebraic Foundations of Systems Specification. Springer, Heidelberg (1999)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol.\u00a02, Oxford University Press (1992)","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/3-540-10007-5_41","volume-title":"Abstract Software Specifications","author":"R. Burstall","year":"1980","unstructured":"Burstall, R., Goguen, J.: The semantics of Clear, a specification language. In: Bjorner, D. (ed.) Abstract Software Specifications. LNCS, vol.\u00a086, pp. 292\u2013332. Springer, Heidelberg (1980)"},{"issue":"2","key":"9_CR5","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1145\/77600.77621","volume":"37","author":"J.A. Bergstra","year":"1990","unstructured":"Bergstra, J.A., Heering, J., Klint, P.: Module algebra. J. ACM\u00a037(2), 335\u2013372 (1990)","journal-title":"J. ACM"},{"issue":"2","key":"9_CR6","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1016\/S0304-3975(01)00317-6","volume":"286","author":"T. Borzyszkowski","year":"2002","unstructured":"Borzyszkowski, T.: Logical systems for structured specifications. Theor. Comput. Sci.\u00a0286(2), 197\u2013245 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR7","unstructured":"Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F., Sojakova, K.: Towards Logical Frameworks in the Heterogeneous Tool Set Hets. In: Workshop on Abstract Development Techniques (2010)"},{"issue":"1","key":"9_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/147508.147524","volume":"39","author":"J. Goguen","year":"1992","unstructured":"Goguen, J., Burstall, R.: Institutions: Abstract model theory for specification and programming. Journal of the Association for Computing Machinery\u00a039(1), 95\u2013146 (1992)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-39993-3_7","volume-title":"From Object-Orientation to Formal Methods","author":"J. Goguen","year":"2004","unstructured":"Goguen, J., Rosu, G.: Composing Hidden Information Modules over Inclusive Institutions. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From Object-Orientation to Formal Methods. LNCS, vol.\u00a02635, pp. 96\u2013123. Springer, Heidelberg (2004)"},{"issue":"1","key":"9_CR10","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Horozal, F., Rabe, F.: Representing Model Theory in a Type-Theoretical Logical Framework. Theoretical Computer Science (to appear, 2011), http:\/\/kwarc.info\/frabe\/Research\/HR_folsound_10.pdf","DOI":"10.1016\/j.tcs.2011.03.022"},{"key":"9_CR12","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/0168-0072(94)90009-4","volume":"67","author":"R. Harper","year":"1994","unstructured":"Harper, R., Sannella, D., Tarlecki, A.: Structured presentations and logic representations. Annals of Pure and Applied Logic\u00a067, 113\u2013160 (1994)","journal-title":"Annals of Pure and Applied Logic"},{"key":"9_CR13","unstructured":"Iancu, M., Rabe, F.: Formalizing Foundations of Mathematics. Mathematical Structures in Computer Science (to appear, 2011), http:\/\/kwarc.info\/frabe\/Research\/IR_foundations_10.pdf"},{"key":"9_CR14","unstructured":"Kohlhase, M., Mossakowski, T., Rabe, F.: The LATIN Project (2009), https:\/\/trac.omdoc.org\/LATIN\/"},{"key":"9_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11826095","volume-title":"OMDoc \u2013 An Open Markup Format for Mathematical Documents (version 1.2)","author":"M. Kohlhase","year":"2006","unstructured":"Kohlhase, M.: OMDoc \u2013 An Open Markup Format for Mathematical Documents (version 1.2). LNCS (LNAI), vol.\u00a04180. Springer, Heidelberg (2006)"},{"issue":"2","key":"9_CR16","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/S0304-3975(96)00163-6","volume":"173","author":"S. Kahrs","year":"1997","unstructured":"Kahrs, S., Sannella, D., Tarlecki, A.: The definition of extended ML: A gentle introduction. Theoretical Computer Science\u00a0173(2), 445\u2013484 (1997)","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"9_CR17","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 - Proof management for structured specifications. J. Log. Algebr. Program.\u00a067(1-2), 114\u2013145 (2006)","journal-title":"J. Log. Algebr. Program."},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: An Intuitionistic Theory of Types: Predicative Part. In: Proceedings of the 1973 Logic Colloquium, pp. 73\u2013118. North-Holland (1974)","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-71209-1_40","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Mossakowski","year":"2007","unstructured":"Mossakowski, T., Maeder, C., L\u00fcttich, K.: The Heterogeneous Tool Set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 519\u2013522. Springer, Heidelberg (2007)"},{"key":"9_CR20","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":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-03429-9_18","volume-title":"Recent Trends in Algebraic Development Techniques","author":"T. Mossakowski","year":"2009","unstructured":"Mossakowski, T., Tarlecki, A.: Heterogeneous Logical Environments for Distributed Specifications. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol.\u00a05486, pp. 266\u2013289. Springer, Heidelberg (2009)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"9_CR23","unstructured":"Rabe, F.: A Logical Framework Combining Model and Proof Theory. Submitted to Mathematical Structures in Computer Science (2010), http:\/\/kwarc.info\/frabe\/Research\/rabe_combining_09.pdf"},{"key":"9_CR24","unstructured":"Rabe, F., Kohlhase, M.: A Scalable Module System (2010), http:\/\/kwarc.info\/frabe\/Research\/mmt.pdf"},{"key":"9_CR25","doi-asserted-by":"crossref","unstructured":"Rabe, F., Sch\u00fcrmann, C.: A Practical Module System for LF. In: Cheney, J., Felty, A. (eds.) Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP), pp. 40\u201348. ACM Press (2009)","DOI":"10.1145\/1577824.1577831"},{"key":"9_CR26","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/0890-5401(88)90008-9","volume":"76","author":"D. Sannella","year":"1988","unstructured":"Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Information and Computation\u00a076, 165\u2013210 (1988)","journal-title":"Information and Computation"},{"key":"9_CR27","volume-title":"Foundations of Algebraic Specification and Formal Program Development","author":"D. Sannella","year":"2011","unstructured":"Sannella, D., Tarlecki, A.: Foundations of Algebraic Specification and Formal Program Development. Springer, Heidelberg (2011)"},{"key":"9_CR28","doi-asserted-by":"crossref","unstructured":"Sannella, D., Wirsing, M.: A kernel language for algebraic specification and implementation. In: ADT (1983)","DOI":"10.1007\/3-540-12689-9_122"},{"key":"9_CR29","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(86)90051-4","volume":"42","author":"M. Wirsing","year":"1986","unstructured":"Wirsing, M.: Structured algebraic specifications: A kernel language. Theor. Comput. Sci.\u00a042, 123\u2013249 (1986)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Zholudev, V., Kohlhase, M.: TNTBase: a Versioned Storage for XML. In: Proceedings of Balisage: The Markup Conference 2009. Balisage Series on Markup Technologies, vol.\u00a03. Mulberry Technologies, Inc. (2009)","DOI":"10.4242\/BalisageVol3.Zholudev01"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28412-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T04:22:52Z","timestamp":1742530972000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28412-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642284113","9783642284120"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28412-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}