{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T06:25:45Z","timestamp":1748413545230},"reference-count":51,"publisher":"Oxford University Press (OUP)","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017,9]]},"DOI":"10.1093\/logcom\/exu079","type":"journal-article","created":{"date-parts":[[2014,12,15]],"date-time":"2014-12-15T01:19:49Z","timestamp":1418606389000},"page":"1753-1798","source":"Crossref","is-referenced-by-count":24,"title":["How to identify, translate and combine logics?"],"prefix":"10.1093","volume":"27","author":[{"given":"Florian","family":"Rabe","sequence":"first","affiliation":[]}],"member":"286","published-online":{"date-parts":[[2014,12,14]]},"reference":[{"key":"key\n\t\t\t\t20170830122809_B1","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","year":"1986"},{"key":"key\n\t\t\t\t20170830122809_B2","article-title":"Lambda calculi with types.","volume-title":"Handbook of Logic in Computer Science","year":"1992"},{"key":"key\n\t\t\t\t20170830122809_B3","article-title":"The Open Math Standard, Version 2.0. Technical report, The Open Math Society,","year":"2004"},{"key":"key\n\t\t\t\t20170830122809_B4","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/s11787-012-0052-y","article-title":"Quantified multimodal logics in simple type theory.","volume":"7","year":"2013","journal-title":"Logica Universalis"},{"key":"key\n\t\t\t\t20170830122809_B5","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/3-7643-7304-0_6","article-title":"Equipollent logical systems.","volume-title":"Logica Universalis","year":"2005"},{"key":"key\n\t\t\t\t20170830122809_B6","first-page":"118","article-title":"A Proof Theoretic Interpretation of Model Theoretic Hiding.","volume-title":"Recent Trends in Algebraic Development Techniques 2010","year":"2012"},{"key":"key\n\t\t\t\t20170830122809_B7","first-page":"289","article-title":"Project abstract: Logic Atlas and Integrator (LATIN).","volume-title":"Intelligent Computer Mathematics","year":"2011"},{"key":"key\n\t\t\t\t20170830122809_B8","first-page":"139","article-title":"Towards logical frameworks in the heterogeneous tool set hets.","volume-title":"Recent Trends in Algebraic Development Techniques 2010","year":"2012"},{"key":"key\n\t\t\t\t20170830122809_B9","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/S0304-3975(96)00160-0","article-title":"May I borrow your logic? (Transporting logical structures along maps).","volume":"173","year":"1997","journal-title":"Theoretical Computer Science"},{"key":"key\n\t\t\t\t20170830122809_B10","article-title":"The Coq proof assistant: reference manual.","volume-title":"Technical report, INRIA","author":"Coq Development Team.","year":"2014"},{"key":"key\n\t\t\t\t20170830122809_B11","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1017\/S0960129596002253","article-title":"Weak inclusion systems.","volume":"7","year":"1997","journal-title":"Mathematical Structures in Computer Science"},{"key":"key\n\t\t\t\t20170830122809_B12","first-page":"83","article-title":"Logical support for modularization.","volume-title":"Logical Environments","year":"1993"},{"key":"key\n\t\t\t\t20170830122809_B13","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1023\/A:1016330812768","article-title":"Grothendieck institutions.","volume":"10","year":"2002","journal-title":"Applied Categorical Structures"},{"key":"key\n\t\t\t\t20170830122809_B14","first-page":"44","article-title":"Structuring theories on consequence","volume-title":"Recent Trends in Data Type Specification","year":"1987"},{"key":"key\n\t\t\t\t20170830122809_B15","first-page":"163","article-title":"A machine-checked proof of the odd order theorem.","year":"2013","journal-title":"Interactive Theorem Proving"},{"key":"key\n\t\t\t\t20170830122809_B16","first-page":"313","article-title":"A study in the foundations of programming methodology: specifications, institutions, charters and parchments","volume-title":"Workshop on Category Theory and Computer Programming","year":"1986"},{"key":"key\n\t\t\t\t20170830122809_B17","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","article-title":"Institutions: abstract model theory for specification and programming.","volume":"39","year":"1992","journal-title":"Journal of the Association for Computing Machinery"},{"key":"key\n\t\t\t\t20170830122809_B18","first-page":"73","article-title":"HOL: A proof generating system for higher-order logic.","volume-title":"VLSI Specification, Verification and Synthesis","year":"1988"},{"key":"key\n\t\t\t\t20170830122809_B19","first-page":"265","article-title":"HOL light: A tutorial introduction","volume-title":"Proceedings of the First International Conference on Formal Methods in Computer-Aided Design","year":"1996"},{"key":"key\n\t\t\t\t20170830122809_B20","doi-asserted-by":"crossref","first-page":"159","DOI":"10.2307\/2267044","article-title":"The completeness of the first-order functional calculus.","volume":"14","year":"1949","journal-title":"Journal of Symbolic Logic"},{"key":"key\n\t\t\t\t20170830122809_B21","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics.","volume":"40","year":"1993","journal-title":"Journal of the Association for Computing Machinery"},{"key":"key\n\t\t\t\t20170830122809_B22","first-page":"64","article-title":"Extending MKM formats at the statement level","volume-title":"Intelligent Computer Mathematics","year":"2012"},{"key":"key\n\t\t\t\t20170830122809_B23","doi-asserted-by":"crossref","first-page":"4919","DOI":"10.1016\/j.tcs.2011.03.022","article-title":"Representing model theory in a type-theoretical logical framework","volume":"412","year":"2011","journal-title":"Theoretical Computer Science"},{"key":"key\n\t\t\t\t20170830122809_B24","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0168-0072(94)90009-4","article-title":"Structured presentations and logic representations.","volume":"67","year":"1994","journal-title":"Annals of Pure and Applied Logic"},{"key":"key\n\t\t\t\t20170830122809_B25","doi-asserted-by":"crossref","first-page":"883","DOI":"10.1017\/S0960129511000144","article-title":"Formalizing foundations of mathematics","volume":"21","year":"2011","journal-title":"Mathematical Structures in Computer Science"},{"key":"key\n\t\t\t\t20170830122809_B26","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","article-title":"seL4: formal verification of an operating-system kernel.","volume":"53","year":"2010","journal-title":"Communications of the ACM"},{"key":"key\n\t\t\t\t20170830122809_B27","article-title":"The LATIN Project,","year":"2009"},{"key":"key\n\t\t\t\t20170830122809_B28","first-page":"323","article-title":"A mechanized translation from higher-order logic to set theory","volume-title":"Interactive Theorem Proving","year":"2010"},{"key":"key\n\t\t\t\t20170830122809_B29","volume-title":"Functional Semantics of Algebraic Theories","year":"1963"},{"key":"key\n\t\t\t\t20170830122809_B30","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1016\/j.apal.2012.09.005","article-title":"Kripke semantics and proof systems for combining intuitionistic logic and classical logic","volume":"164","year":"2013","journal-title":"Annals of Pure and Applied Logic"},{"key":"key\n\t\t\t\t20170830122809_B31","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","article-title":"Recursive functions of symbolic expressions and their computation by machine, Part I","volume":"3","year":"1960","journal-title":"Communications of the ACM"},{"key":"key\n\t\t\t\t20170830122809_B32","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1007\/s11787-009-0005-2","article-title":"What is a logic translation?","volume":"3","year":"2009","journal-title":"Logica Universalis"},{"key":"key\n\t\t\t\t20170830122809_B33","first-page":"275","article-title":"General logics.","volume-title":"Proceedings, Logic Colloquium, 1987","year":"1989"},{"key":"key\n\t\t\t\t20170830122809_B34","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/3-7643-7304-0_7","article-title":"What is a logic?","volume-title":"Logica Universalis","year":"2005"},{"key":"key\n\t\t\t\t20170830122809_B35","first-page":"3","article-title":"On the meanings of the logical constants and the justifications of the logical laws.","volume":"1","year":"1996","journal-title":"Nordic Journal of Philosophical Logic"},{"key":"key\n\t\t\t\t20170830122809_B36","first-page":"519","article-title":"The heterogeneous tool set.","year":"2007","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems 2007, vol. 4424 of Lecture Notes in Computer Science"},{"key":"key\n\t\t\t\t20170830122809_B37","first-page":"349","article-title":"Combining and representing logical systems using model-theoretic parchments.","volume-title":"Recent Trends in Algebraic Development Techniques","year":"1997"},{"key":"key\n\t\t\t\t20170830122809_B38","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","year":"2002"},{"key":"key\n\t\t\t\t20170830122809_B39","volume-title":"Isabelle: A Generic Theorem Prover,","year":"1994"},{"key":"key\n\t\t\t\t20170830122809_B40","doi-asserted-by":"crossref","first-page":"1063","DOI":"10.1016\/B978-044450813-3\/50019-9","article-title":"Logical frameworks.","volume-title":"Handbook of automated reasoning","year":"2001"},{"key":"key\n\t\t\t\t20170830122809_B41","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","article-title":"System description: Twelf - a meta-logical framework for deductive systems.","volume":"1632","year":"1999","journal-title":"Lecture Notes in Computer Science"},{"key":"key\n\t\t\t\t20170830122809_B42","doi-asserted-by":"crossref","first-page":"945","DOI":"10.1017\/S0960129512000424","article-title":"A Logical Framework Combining Model and proof theory","volume":"23","year":"2013","journal-title":"Mathematical Structures in Computer Science"},{"key":"key\n\t\t\t\t20170830122809_B43","first-page":"339","article-title":"The MMT API: A generic MKM system","volume-title":"Intelligent Computer Mathematics","year":"2013"},{"key":"key\n\t\t\t\t20170830122809_B44","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.ic.2013.06.001","article-title":"A scalable module system.","volume":"230","year":"2013","journal-title":"Information and Computation"},{"key":"key\n\t\t\t\t20170830122809_B45","first-page":"40","article-title":"A practical module system for LF.","volume-title":"Proceedings of the Workshop on Logical Frameworks: Meta-Theory and Practice (LFMTP)","year":"2009"},{"key":"key\n\t\t\t\t20170830122809_B46","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2536740.2536741","article-title":"Logical relations for a logical framework","volume":"14","year":"2013","journal-title":"ACM Transactions on Computational Logic"},{"key":"key\n\t\t\t\t20170830122809_B47","article-title":"Mechanically verifying logic translations","year":"2010"},{"key":"key\n\t\t\t\t20170830122809_B48","article-title":"An executable formalization of the HOL\/Nuprl connection in the metalogical framework Twelf.","volume-title":"11th International Conference on Logic for Programming Artificial Intelligence and Reasoning","year":"2004"},{"key":"key\n\t\t\t\t20170830122809_B49","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1093\/logcom\/9.2.149","article-title":"Fibring of logics as a categorial construction","volume":"9","year":"1999","journal-title":"Journal of Logic and Computation"},{"key":"key\n\t\t\t\t20170830122809_B50","first-page":"413","article-title":"A kernel language for algebraic specification and implementation","volume-title":"Fundamentals of Computation Theory","year":"1983"},{"key":"key\n\t\t\t\t20170830122809_B51","first-page":"26","article-title":"Computer assisted reasoning with MIZAR.","volume-title":"Proceedings of the 9th International Joint Conference on Artificial Intelligence","year":"1985"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/27\/6\/1753\/19646428\/exu079.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,8,30]],"date-time":"2017-08-30T16:28:25Z","timestamp":1504110505000},"score":1,"resource":{"primary":{"URL":"http:\/\/academic.oup.com\/logcom\/article\/27\/6\/1753\/2687725\/How-to-identify-translate-and-combine-logics"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,12,14]]},"references-count":51,"journal-issue":{"issue":"6","published-online":{"date-parts":[[2014,12,14]]},"published-print":{"date-parts":[[2017,9]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exu079","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,12,14]]}}}