{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:06:40Z","timestamp":1761955600291,"version":"build-2065373602"},"reference-count":39,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T00:00:00Z","timestamp":1236124800000},"content-version":"unspecified","delay-in-days":4933,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[1995,9]]},"abstract":"<jats:p>We propose a new framework for representing logics, called LF<jats:sup>+<\/jats:sup>, which is based on the Edinburgh Logical Framework. The new framework allows us to give, apparently for the first time, general definitions that capture how well a logic has been represented. These definitions are possible because we are able to distinguish in a generic way that part of the LF<jats:sup>+<\/jats:sup>entailment corresponding to the underlying logic. This distinction does not seem to be possible with other frameworks. Using our definitions, we show that, for example, natural deduction first-order logic can be well-represented in LF<jats:sup>+<\/jats:sup>, whereas linear and relevant logics cannot. We also show that our syntactic definitions of representation have a simple formulation as indexed isomorphisms, which both confirms that our approach is a natural one and provides a link between type-theoretic and categorical approaches to frameworks.<\/jats:p>","DOI":"10.1017\/s0960129500000785","type":"journal-article","created":{"date-parts":[[2009,3,4]],"date-time":"2009-03-04T09:01:13Z","timestamp":1236157273000},"page":"323-349","source":"Crossref","is-referenced-by-count":3,"title":["Equivalences between logics and their representing type theories"],"prefix":"10.1017","volume":"5","author":[{"given":"Philippa","family":"Gardner","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2009,3,4]]},"reference":[{"volume-title":"Category Theory for Computing Science","year":"1990","author":"Barr","key":"S0960129500000785_ref008"},{"key":"S0960129500000785_ref033","doi-asserted-by":"publisher","DOI":"10.1142\/S012905419200019X"},{"key":"S0960129500000785_ref030","doi-asserted-by":"crossref","unstructured":"Par\u00e9 R. and Schumacher D. (1978) Abstract Families and the Adjoint Functor Theorems. In: Johnstone and Par\u00e9 (eds.) Indexed Categories and their Applications 1\u2013125.","DOI":"10.1007\/BFb0061361"},{"key":"S0960129500000785_ref028","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16492-8_94"},{"key":"S0960129500000785_ref025","first-page":"1","volume-title":"Applications of Categorical Algebra","author":"Lawvere","year":"1970"},{"volume-title":"Proceedings of the 1993 Workshop on Types for Proofs and Programs","year":"1993","author":"Dowek","key":"S0960129500000785_ref014"},{"volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs","year":"1992","author":"Simpson","key":"S0960129500000785_ref037"},{"volume-title":"A Relevant Analysis of Natural Deduction","year":"1992","author":"Miller","key":"S0960129500000785_ref029"},{"key":"S0960129500000785_ref024","first-page":"479","volume-title":"To H. B. Curry: Essays in Combinatoric Logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"volume-title":"Een nadere bewijstheoretishe analyse van GSTT's","year":"1989","author":"Terlouw","key":"S0960129500000785_ref039"},{"key":"S0960129500000785_ref022","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S0960129500000785_ref021","first-page":"73","volume-title":"VSLI Specification, Verification and Synthesis","author":"Gordon","year":"1987"},{"key":"S0960129500000785_ref018","unstructured":"Gardner P. A. (1993a) The Construction of \u03b2\u03b7-long normal forms in Dependent Type Theories (manuscript)."},{"key":"S0960129500000785_ref004","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90023-U"},{"key":"S0960129500000785_ref023","doi-asserted-by":"crossref","unstructured":"Harper R. , Sannella D. and Tarlecki A. (1989) Structure and Representation in LF, Technical Report ECS-LFCS-89\u201375, Edinburgh University, 1989. (Preliminary version in the Proceedings of the Fourth Annual Symposium on Logic in Computer Science 226\u2013237.)","DOI":"10.1109\/LICS.1989.39177"},{"volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs","year":"1992","author":"Aczel","key":"S0960129500000785_ref001"},{"key":"S0960129500000785_ref019","doi-asserted-by":"crossref","unstructured":"Geuvers J. H. (1992) The Church-Rosser Property for \u03b2\u03b7-reduction in Typed Lambda Calculi, Proceedings of the Seventh Annual Symposium on Logic in Computer Science 453\u2013460.","DOI":"10.1109\/LICS.1992.185556"},{"key":"S0960129500000785_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"volume-title":"Natural Deduction: A Proof-theoretical study","year":"1965","author":"Prawitz","key":"S0960129500000785_ref032"},{"key":"S0960129500000785_ref007","unstructured":"Beradi S. (1990) Type dependence and constructive mathematics, Ph.D. thesis. Mathematical Institute, Torino."},{"key":"S0960129500000785_ref035","unstructured":"Salvesen A. (1991) The Church-Rosser Property for Pure Type Systems with \u03b2\u03b7-reduction. (Submitted)"},{"key":"S0960129500000785_ref002","unstructured":"Augustsson L. , Coquand T. and Nordstr\u00f6m B. (1990) A Short Description of Another Logical Framework. In: Huet G. and Plotkin G. D. (eds.) Proceedings of the First Workshop on Logical Frameworks 39\u201342."},{"volume-title":"The Church-Rosser Property for LF with \u03b2\u03b7- reduction","year":"1990","author":"Salvesen","key":"S0960129500000785_ref034"},{"volume-title":"Combinatory Logic","year":"1958","author":"Curry","key":"S0960129500000785_ref013"},{"key":"S0960129500000785_ref027","unstructured":"Martin-L\u00f6f P. (1985) On the Meanings of the Logical Constants and the Justifications of the Logical Laws, Technical Report 2, Universit\u00e0 di Siena."},{"volume-title":"To H.B. Curry: Essays in Combinatory Logic. Lambda Calculus and Formalism","year":"1980","author":"Seldin","key":"S0960129500000785_ref036"},{"key":"S0960129500000785_ref006","doi-asserted-by":"publisher","DOI":"10.2307\/2273784"},{"key":"S0960129500000785_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245294"},{"key":"S0960129500000785_ref011","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"volume-title":"Implementing Mathematics with the NuPrl Proof Development System","year":"1986","key":"S0960129500000785_ref012"},{"volume-title":"Logic, Semantics and Metamathematics","year":"1956","author":"Tarski","key":"S0960129500000785_ref038"},{"key":"S0960129500000785_ref015","first-page":"117","article-title":"Relevant Logic and Entailment","volume":"3","author":"Dunn","year":"1984","journal-title":"Handbook of Philosophical Logic"},{"key":"S0960129500000785_ref026","unstructured":"Luo Z. and Pollack R. (1992) LEGO Proof Development System: User's Manual, Technical Report ECS-LFCS-92\u2013211, Edinburgh University."},{"key":"S0960129500000785_ref017","first-page":"146","article-title":"A New Type Theory for Representing Logics","volume":"698","author":"Gardner","year":"1993","journal-title":"Springer-Verlag Lecture Notes in Artificial Intelligence"},{"key":"S0960129500000785_ref031","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"key":"S0960129500000785_ref010","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511621192"},{"key":"S0960129500000785_ref005","first-page":"117","volume-title":"Handbook of Logic in Computer Science 2","author":"Barendregt","year":"1992"},{"key":"S0960129500000785_ref016","unstructured":"Gardner P. A. (1992) Representing Logics in Type Theory, Ph.D. Thesis, Technical Report ECS-LFCS-92\u2013227, Edinburgh University."},{"key":"S0960129500000785_ref009","first-page":"589","volume-title":"To H. B. Curry: Essays in Combinatoric Logic, Lambda Calculus and Formalism","author":"de Bruijn","year":"1980"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129500000785","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T00:06:01Z","timestamp":1738973161000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129500000785\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,9]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1995,9]]}},"alternative-id":["S0960129500000785"],"URL":"https:\/\/doi.org\/10.1017\/s0960129500000785","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[1995,9]]}}}