{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:08:22Z","timestamp":1761610102455,"version":"build-2065373602"},"reference-count":22,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":6784,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[1995]]},"DOI":"10.1016\/s1571-0661(04)00028-3","type":"journal-article","created":{"date-parts":[[2004,1,29]],"date-time":"2004-01-29T05:14:39Z","timestamp":1075353279000},"page":"515-534","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":11,"special_numbering":"C","title":["On a Modal \u03bb-Calculus for S4"],"prefix":"10.1016","volume":"1","author":[{"given":"F.","family":"Pfenning","sequence":"first","affiliation":[]},{"given":"H.C.","family":"Wong","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","article-title":"Computational interpretations of linear logic","volume":"111","author":"Abramsky","year":"1993","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.1016\/S1571-0661(04)00028-3_NEWBIB2","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1093\/logcom\/2.1.31","article-title":"A constructive presentation for the modal connective of necessity","volume":"2","author":"Mario Benevides","year":"1992","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB3","doi-asserted-by":"crossref","unstructured":"Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. A term calculus for intuitionistic linear logic. In M. Bezem and J.F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA'93, pages 75\u201390, Utrecht, The Netherlands, March 1993. Springer-Verlag LNCS 664.","DOI":"10.1007\/BFb0037099"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB4","unstructured":"Gavin Bierman. On Intuitionistic Linear Logic. PhD thesis, University of Cambridge Computer Laboratory, December 1993. Revised version available as technical report No. 346, August 1994."},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB5","unstructured":"Gavin Bierman and Valeria de Paiva. Intuitionistic necessity revisited. In Proceedings of the Logic at Work Conference, Amsterdam, Holland, December 1992."},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB6","doi-asserted-by":"crossref","unstructured":"Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Informal Proceedings of the Workshop on Types for Program Analysis, Aarhus, Denmark, May 1995.","DOI":"10.21236\/ADA296537"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB7","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1022676712939","article-title":"Higher-order and modal logic as a framework for explanation-based generalization","volume":"9","author":"Dietzen","year":"1992","journal-title":"Machine Learning"},{"issue":"4","key":"10.1016\/S1571-0661(04)00028-3_NEWBIB8","doi-asserted-by":"crossref","first-page":"1319","DOI":"10.2307\/2275370","article-title":"Extending the Curry-Howard interpretation to linear, relevant and other resource logics","volume":"57","author":"Dov Gabbay","year":"1992","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB9","series-title":"Logic and Computer Science","article-title":"On Girard's \u2018Candidats de R\u00e9ductibilit\u00e9\u201d","author":"Jean Gallier","year":"1990"},{"year":"1989","series-title":"Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science","author":"-Yves Girard","key":"10.1016\/S1571-0661(04)00028-3_NEWBIB10"},{"issue":"1","key":"10.1016\/S1571-0661(04)00028-3_NEWBIB11","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB12","doi-asserted-by":"crossref","unstructured":"Robert Harper and Greg Morrisett. Compiling polymorphism using intensional type analysis. In Peter Lee, editor, Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 130\u2013141, San Francisco, California, January 1995.","DOI":"10.1145\/199448.199475"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB13","series-title":"Proof theory of Modal Logics","article-title":"A computational interpretation of modal proofs","author":"Martini","year":"1994"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB14","doi-asserted-by":"crossref","unstructured":"Simone Martini and Andrea Masini. On the fine structure of the exponential rule. In J.-Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, Proceedings of the 1993 Workshop on Linear Logic, Ithaca, New York, 1994. MIT Press. To appear.","DOI":"10.1017\/CBO9780511629150.010"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB15","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0168-0072(92)90029-Y","article-title":"2-Sequent calculus: A proof theory of modality","volume":"58","author":"Masini","year":"1992","journal-title":"Annals Pure and Applied Logic"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB16","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1093\/logcom\/3.5.533","article-title":"2-Sequent calculus: Intuitionism and natural deduction","volume":"3","author":"Masini","year":"1993","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB17","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","article-title":"Uniform proofs as a foundation for logic programming","volume":"51","author":"Miller","year":"1991","journal-title":"Annals of Pure and Applied Logic"},{"year":"1992","series-title":"Two-Level Functional Languages","author":"Nielson","key":"10.1016\/S1571-0661(04)00028-3_NEWBIB18"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB19","series-title":"Logical Frameworks","first-page":"149","article-title":"programming in the LF logical framewor","author":"Pfenning","year":"1991"},{"year":"1965","series-title":"Natural Deduction","author":"Prawitz","key":"10.1016\/S1571-0661(04)00028-3_NEWBIB20"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB21","unstructured":"Harold Schellinx. The Noble Art of Linear Decorating. PhD thesis, Dutcch Institute for Logic, Language and Computation, University of Amsterdam, 1994. Available in the ILLC Dissertation Series, 1994-1"},{"key":"10.1016\/S1571-0661(04)00028-3_NEWBIB22","unstructured":"A. S. Troelstra. Natural deduction for intuitionistic linear logic. Unpublished manuscript, May 1993."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104000283?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104000283?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:03:21Z","timestamp":1761609801000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104000283"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"references-count":22,"alternative-id":["S1571066104000283"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)00028-3","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"On a Modal \u03bb-Calculus for S4","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)00028-3","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2000 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}