{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:20:45Z","timestamp":1725456045516},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540516620"},{"type":"electronic","value":"9783540467403"}],"license":[{"start":{"date-parts":[[1989,1,1]],"date-time":"1989-01-01T00:00:00Z","timestamp":599616000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1989]]},"DOI":"10.1007\/bfb0018356","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T07:50:09Z","timestamp":1132645809000},"page":"250-272","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Logic representation in LF"],"prefix":"10.1007","author":[{"given":"Robert","family":"Harper","sequence":"first","affiliation":[]},{"given":"Donald","family":"Sannella","sequence":"additional","affiliation":[]},{"given":"Andrzej","family":"Tarlecki","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"16_CR1","unstructured":"A. Avron, F. Honsell, and I. Mason. Using typed lambda calculus to implement formal systems on a machine. Technical Report ECS-LFCS-87-31, Laboratory for the Foundations of Computer Science, Edinburgh University, June 1987."},{"key":"16_CR2","unstructured":"A. Avron. Simple consequence relations. Technical Report ECS-LFCS-87-30, Laboratory for the Foundations of Computer Science, Edinburgh University, June 1987."},{"key":"16_CR3","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1016\/0003-4843(74)90016-3","volume":"7","author":"K.J. Barwise","year":"1974","unstructured":"K.J. Barwise. Axioms for abstract model theory. Ann. of Mathematical Logic 7:221\u2013265, 1974.","journal-title":"Ann. of Mathematical Logic"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"R. Burstall and J. Goguen. The semantics of CLEAR, a specification language. In Proc. of Advanced Course on Abstract Software Specifications, Copenhagen, pages 292\u2013332, Springer LNCS 86, 1980.","DOI":"10.1007\/3-540-10007-5_41"},{"key":"16_CR5","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/0168-0072(86)90053-9","volume":"32","author":"J. Cartmell","year":"1986","unstructured":"J. Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209\u2013243, 1986.","journal-title":"Annals of Pure and Applied Logic"},{"key":"16_CR6","unstructured":"R.L. Constable, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, 1986."},{"key":"16_CR7","unstructured":"N.G. de Bruijn. A survey of the project AUTOMATH. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589\u2013606, Academic Press, 1980."},{"key":"16_CR8","unstructured":"J. Fiadeiro and A. Sernadas. Structuring theories on consequence. In D. Sannella and A. Tarlecki, editors, Selected Papers from the Fifth Workshop on Specification of Abstract Data Types, Gullane, Scotland, pages 44\u201372, Springer LNCS 332, 1988."},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"J. Goguen and R. Burstall. Introducing institutions. In E. Clarke and D. Kozen, editors, Logics of Programs, pages 221\u2013256, Springer LNCS 164, 1984.","DOI":"10.1007\/3-540-12896-4_366"},{"key":"16_CR10","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. In Proc. of the 2nd IEEE Symp. on Logic in Computer Science, Ithaca, New York, pages 194\u2013204, 1987."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"R. Harper, D. Sannella, A. Tarlecki. Structure and representation in LF. In Proc. of the 4th IEEE Symp. on Logic in Computer Science, Asilomar, California, pages 226\u2013237, 1989.","DOI":"10.1007\/BFb0018356"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"J. Meseguer. General logics. In Proc. Logic Colloquium '87, North-Holland, 1989.","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"D. Sannella and R. Burstall. Structured theories in LCF. In Proc. of the 8th Colloq. on Algebra and Trees in Programming, L'Aquila, Italy, pages 377\u2013391, Springer LNCS 159, 1983.","DOI":"10.1007\/3-540-12727-5_24"},{"key":"16_CR14","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/0890-5401(88)90008-9","volume":"76","author":"D. Sannella","year":"1988","unstructured":"D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation, 76:165\u2013210, 1988.","journal-title":"Information and Computation"},{"key":"16_CR15","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0022-0000(86)90057-7","volume":"33","author":"A. Tarlecki","year":"1986","unstructured":"A. Tarlecki. Quasi-varieties in abstract algebraic institutions. Journal of Computer and System Sciences, 33:333\u2013360, 1986.","journal-title":"Journal of Computer and System Sciences"},{"key":"16_CR16","unstructured":"A. Tarlecki, R. Burstall, and J. Goguen. Some fundamental algebraic tools for the semantics of computation, Part III: Indexed categories. To appear, Theoretical Computer Science."},{"key":"16_CR17","volume-title":"The Language Theory of AUTOMATH","author":"D.T. Daalen van","year":"1980","unstructured":"D.T. van Daalen. The Language Theory of AUTOMATH. Ph.D. thesis, Technical University of Eindhoven, Eindhoven, Netherlands, 1980."}],"container-title":["Lecture Notes in Computer Science","Category Theory and Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0018356","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T14:38:56Z","timestamp":1683297536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0018356"}},"subtitle":["Report on work in progress"],"short-title":[],"issued":{"date-parts":[[1989]]},"ISBN":["9783540516620","9783540467403"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0018356","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1989]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}