{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T19:26:52Z","timestamp":1743017212197,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"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_10","type":"book-chapter","created":{"date-parts":[[2012,2,18]],"date-time":"2012-02-18T09:14:28Z","timestamp":1329556468000},"page":"139-159","source":"Crossref","is-referenced-by-count":7,"title":["Towards Logical Frameworks in the Heterogeneous Tool Set Hets"],"prefix":"10.1007","author":[{"given":"Mihai","family":"Codescu","sequence":"first","affiliation":[]},{"given":"Fulya","family":"Horozal","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[]},{"given":"Till","family":"Mossakowski","sequence":"additional","affiliation":[]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[]},{"given":"Kristina","family":"Sojakova","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"10_CR1","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/S0304-3975(01)00368-1","volume":"286","author":"E. Astesiano","year":"2002","unstructured":"Astesiano, E., Bidoit, M., Kirchner, H., Krieg-Br\u00fcckner, B., Mosses, P., Sannella, D., Tarlecki, A.: CASL: The Common Algebraic Specification Language. Theoretical Computer Science\u00a0286(2), 153\u2013196 (2002)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10_CR2","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/A:1005060022386","volume":"60","author":"A. Avron","year":"1998","unstructured":"Avron, A., Honsell, F., Miculan, M., Paravano, C.: Encoding modal logics in logical frameworks. Studia Logica\u00a060(1), 161\u2013208 (1998)","journal-title":"Studia Logica"},{"key":"10_CR3","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":"10_CR4","volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Coq\u2019Art: The Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"10_CR5","first-page":"1","volume":"12","author":"M. Bortin","year":"2006","unstructured":"Bortin, M., Broch Johnsen, E., L\u00fcth, C.: Structured formal development in Isabelle. Nordic Journal of Computing\u00a012, 1\u201320 (2006)","journal-title":"Nordic Journal of Computing"},{"key":"10_CR6","unstructured":"Constable, R., Allen, S., Bromley, H., Cleaveland, W., Cremer, J., Harper, R., Howe, D., Knoblock, T., Mendler, N., Panangaden, P., Sasaki, J., Smith, S.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall (1986)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Clavel, M., Eker, S., Lincoln, P., Meseguer, J.: Principles of Maude. In: Meseguer, J. (ed.) Proceedings of the First International Workshop on Rewriting Logic, vol.\u00a04, pp. 65\u201389 (1996)","DOI":"10.1016\/S1571-0661(04)00034-9"},{"issue":"1","key":"10_CR8","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church, A.: A Formulation of the Simple Theory of Types. Journal of Symbolic Logic\u00a05(1), 56\u201368 (1940)","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR9","unstructured":"Diaconescu, R.: Institution-independent Model Theory. Birkh\u00e4user (2008)"},{"issue":"1","key":"10_CR10","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"},{"issue":"1","key":"10_CR11","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":"10_CR12","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":"10_CR13","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":"10_CR14","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":"10_CR15","unstructured":"Kohlhase, M., Mossakowski, T., Rabe, F.: The LATIN Project (2009), https:\/\/trac.omdoc.org\/LATIN\/"},{"issue":"1-2","key":"10_CR16","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. Journal of Logic and Algebraic Programming\u00a067(1-2), 114\u2013145 (2006)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Meseguer, J.: General logics. In: Ebbinghaus, H.-D., et al. (eds.) Proceedings of Logic Colloquium, 1987, pp. 275\u2013329. North-Holland (1989)","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"10_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":"10_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":"10_CR20","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1093\/oso\/9780198538592.003.0014","volume-title":"What is a Logical System?","author":"N. Mart\u00ed-Oliet","year":"1994","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: General logics and logical frameworks. In: What is a Logical System?, pp. 355\u2013391. Oxford University Press, Inc., New York (1994)"},{"key":"10_CR21","unstructured":"Mossakowski, T.: Heterogeneous Specification and the Heterogeneous Tool Set. Habilitation thesis (2005), http:\/\/www.informatik.uni-bremen.de\/~till\/"},{"key":"10_CR22","unstructured":"Norell, U.: The Agda WiKi (2005), http:\/\/wiki.portal.chalmers.se\/agda"},{"key":"10_CR23","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"10_CR25","unstructured":"Paulson, L.C., Coen, M.: Zermelo-Fraenkel Set Theory. Isabelle distribution, ZF\/ZF.thy (1993)"},{"issue":"1-2","key":"10_CR26","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1006\/inco.1999.2832","volume":"157","author":"F. Pfenning","year":"2000","unstructured":"Pfenning, F.: Structural cut elimination: I. intuitionistic and classical logic. Information and Computation\u00a0157(1-2), 84\u2013141 (2000)","journal-title":"Information and Computation"},{"key":"10_CR27","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"},{"key":"10_CR28","unstructured":"Poswolsky, A., Sch\u00fcrmann, C.: System Description: Delphin - A Functional Programming Language for Deductive Systems. In: Abel, A., Urban, C. (eds.) International Workshop on Logical Frameworks and Metalanguages: Theory and Practice. ENTCS, pp. 135\u2013141 (2008)"},{"key":"10_CR29","unstructured":"Pfenning, F., Sch\u00fcrmann, C., Kohlhase, M., Shankar, N., Owre, S.: The Logosphere Project (2003), http:\/\/www.logosphere.org\/"},{"key":"10_CR30","unstructured":"Rabe, F.: Representing Logics and Logic Translations. PhD thesis, Jacobs University Bremen (2008), http:\/\/kwarc.info\/frabe\/Research\/phdthesis.pdf"},{"key":"10_CR31","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":"10_CR32","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":"10_CR33","unstructured":"Sojakova, K.: Mechanically Verifying Logic Translations. Master\u2019s thesis, Jacobs University Bremen (2010)"},{"key":"10_CR34","unstructured":"Sch\u00fcrmann, C., Stehr, M.: An Executable Formalization of the HOL\/Nuprl Connection in the Metalogical Framework Twelf. In: 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (2004)"},{"key":"10_CR35","unstructured":"Trybulec, A., Blair, H.: Computer Assisted Reasoning with MIZAR. In: Joshi, A. (ed.) Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp. 26\u201328 (1985)"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28412-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T00:27:25Z","timestamp":1713572845000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28412-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642284113","9783642284120"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28412-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}