{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:07:36Z","timestamp":1725484056069},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540432876"},{"type":"electronic","value":"9783540458425"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"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":[[2002]]},"DOI":"10.1007\/3-540-45842-5_8","type":"book-chapter","created":{"date-parts":[[2007,5,27]],"date-time":"2007-05-27T00:00:38Z","timestamp":1180224038000},"page":"112-124","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Kripke-Style Model for the Admissibility of Structural Rules"],"prefix":"10.1007","author":[{"given":"Healfdene","family":"Goguen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"key":"8_CR1","unstructured":"Adriana Compagnoni and Healfdene Goguen. Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997. Submitted to Information and Computation."},{"key":"8_CR2","unstructured":"Thierry Coquand and Jean Gallier. A proof of strong normalization for the theory of constructions using a Kripke-like interpretation. In Workshop on Logical Frameworks-Preliminary Proceedings, 1990."},{"key":"8_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Higher-order abstract syntax in Coq","author":"J. Despeyroux","year":"1995","unstructured":"Jo\u00eblle Despeyroux, Amy Felty, and Andr\u00e9 Hirchowitz. Higher-order abstract syntax in Coq. In Proceedings of the International Conference on Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science. Springer-Verlag, April 1995."},{"key":"8_CR4","unstructured":"Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In 14th Annual Symposium on Logic in Computer Science [1]."},{"key":"8_CR5","unstructured":"Murdoch Gabbay and Andrew Pitts. A new approach to abstract syntax involving binders. In 14th Annual Symposium on Logic in Computer Science [1]."},{"issue":"2","key":"8_CR6","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"Herman Geuvers and Mark-Jan Nederhof. A modular proof of strong normalization for the calculus of constructions. Journal of Functional Programming, 1(2):155\u2013189, April 1991.","journal-title":"Journal of Functional Programming"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Healfdene Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, August 1994.","DOI":"10.1007\/BFb0014053"},{"key":"8_CR8","unstructured":"Healfdene Goguen and James McKinna. Candidates for substitution. Technical Report ECS-LFCS-97-358, University of Edinburgh, May 1997."},{"issue":"1","key":"8_CR9","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1992","unstructured":"Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, 1992.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. On the interpretation of type theory in locally cartesian closed categories. In Jerzy Tiuryn and Leszek Pacholski, editors, Proceedings of CSL, volume 933. Springer-Verlag, 1994.","DOI":"10.1007\/BFb0022273"},{"key":"8_CR11","unstructured":"Martin Hofmann. Semantical analysis of higher-order abstract syntax. In 14th Annual Symposium on Logic in Computer Science [1]."},{"key":"8_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Some algorithmic and prooftheoretical aspects of coercive subtyping","author":"A. Jones","year":"1996","unstructured":"Alex Jones, Zhaohui Luo, and Sergei Soloviev. Some algorithmic and prooftheoretical aspects of coercive subtyping. In Eduardo Gim\u00e9nez and Christine Paulin-Mohring, editors, Proceedings of TYPES\u201996, volume 1512 of Lecture Notes in Computer Science, 1996."},{"key":"8_CR13","unstructured":"Pierre Leleu. Metatheoretic results for a modal lambda calculus. Technical Report RR-3361, INRIA, 1998."},{"key":"8_CR14","unstructured":"Zhaohui Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, November 1990."},{"key":"8_CR15","series-title":"Lect Notes Comput Sci","first-page":"289","volume-title":"Pure type systems formalized","author":"J. McKinna","year":"1933","unstructured":"James McKinna and Robert Pollack. Pure type systems formalized. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 289\u2013305. Springer-Verlag, LNCS 664, March 1993."},{"key":"8_CR16","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan Smith. Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction. Oxford University Press, 1990."},{"key":"8_CR17","unstructured":"Robert Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, April 1995."},{"key":"8_CR18","unstructured":"David Pym. Functorial Kripke models of the lambdaPi-calculus, I: Type theory and internal logic. Draft."},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Thomas Streicher. Semantics of Type Theory: Correctness, Completeness and Independence Results. Birkh\u00e4user, 1991.","DOI":"10.1007\/978-1-4612-0433-6"},{"key":"8_CR20","unstructured":"L. van Benthem Jutting, James McKinna, and Robert Pollack. Typechecking in pure type systems. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programming. Springer-Verlag, 1993."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45842-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T01:26:28Z","timestamp":1683854788000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45842-5_8"}},"subtitle":["(Extended Abstract)"],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540432876","9783540458425"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45842-5_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"14 February 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}