{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T15:32:46Z","timestamp":1775489566728,"version":"3.50.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2000,8,1]],"date-time":"2000-08-01T00:00:00Z","timestamp":965088000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,8,1]],"date-time":"2000-08-01T00:00:00Z","timestamp":965088000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Studia Logica"],"published-print":{"date-parts":[[2000,8]]},"DOI":"10.1023\/a:1005291931660","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T16:13:47Z","timestamp":1040487227000},"page":"383-416","source":"Crossref","is-referenced-by-count":94,"title":["On an Intuitionistic Modal Logic"],"prefix":"10.1007","volume":"65","author":[{"given":"G. M.","family":"Bierman","sequence":"first","affiliation":[]},{"given":"V. C. V.","family":"de Paiva","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"276787_CR1","unstructured":"Barber, A., Linear Type Theories, Semantics and Action Calculi., PhD thesis, University of Edinburgh, 1997."},{"issue":"1","key":"276787_CR2","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1093\/logcom\/2.1.31","volume":"2","author":"M. Benevides","year":"1992","unstructured":"Benevides, M., and T. Maibaum, \u2018A constructive presentation for the modal connective of necessity\u2019, Journal of Logic and Computation 2(1): 31\u201350, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"276787_CR3","doi-asserted-by":"crossref","unstructured":"Benton, P.N., \u2018A mixed linear and non-linear logic: Proofs, terms and models\u2019, in Proceedings of Conference on Computer Science Logic, volume 933 of Lecture Notes in Computer Science, 1995.","DOI":"10.1007\/BFb0022251"},{"issue":"2","key":"276787_CR4","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1017\/S0956796898002998","volume":"8","author":"P.N. Benton","year":"1998","unstructured":"Benton, P.N., G.M. Bierman, and V.C.V. de Paiva, \u2018Computational types from a logical perspective\u2019, Journal of Functional Programming 8(2): 177\u2013193, 1998.","journal-title":"Journal of Functional Programming"},{"key":"276787_CR5","doi-asserted-by":"crossref","unstructured":"Bierman, G.M., \u2018What is a categorical model of intuitionistic linear logic?\u2019, in Proceedings of Second International Conference on Typed \u03bb-calculi and applications, volume 902 of Lecture Notes in Computer Science, pages 78\u201393, 1995.","DOI":"10.1007\/BFb0014046"},{"key":"276787_CR6","unstructured":"Bierman, G.M., and V.C.V. de Paiva, \u2018Intuitionistic necessity revisited\u2019, In Proceedings of Logic at Work Conference. Amsterdam, Holland, December 1992."},{"issue":"2","key":"276787_CR7","first-page":"226","volume":"1","author":"G.M. Bierman","year":"1995","unstructured":"Bierman, G.M., and V.C.V. de Paiva, \u2018Yet another intuitionistic modal logic (abstract)\u2019, Bulletin of Symbolic Logic, 1(2): 226, 1995.","journal-title":"Bulletin of Symbolic Logic"},{"key":"276787_CR8","unstructured":"Bierman, G.M., and V.C.V. de Paiva, \u2018Intuitionistic necessity revisited\u2019, Technical Report CSR\u201396\u201310, School of Computer Science, University of Birmingham, June 1996."},{"key":"276787_CR9","doi-asserted-by":"crossref","unstructured":"Bull, R., and K. Segerberg, \u2018Basic modal logic\u2019, in Handbook of Philosophical Logic, pages 1\u201389. D. Reidel, 1984.","DOI":"10.1007\/978-94-009-6259-0_1"},{"issue":"4","key":"276787_CR10","doi-asserted-by":"crossref","first-page":"249","DOI":"10.2307\/2266613","volume":"17","author":"H.B. Curry","year":"1957","unstructured":"Curry, H.B., \u2018The elimination theorem when modality is present\u2019, Journal of Symbolic Logic 17(4): 249\u2013265, 1957.","journal-title":"Journal of Symbolic Logic"},{"key":"276787_CR11","unstructured":"Curry, H.B., Foundations of Mathematical Logic, McGraw-Hill, 1963."},{"key":"276787_CR12","doi-asserted-by":"crossref","unstructured":"Van Dalen, D., \u2018Intuitionistic logic\u2019, volume 3 of Handbook of Philosophical Logic, chapter 4, pages 225\u2013339. Reidel, 1986.","DOI":"10.1007\/978-94-009-5203-4_4"},{"key":"276787_CR13","doi-asserted-by":"crossref","unstructured":"Davies, R., and F. Pfenning, \u2018A modal analysis of staged computation\u2019, in Proceedings of Symposium on Principles of Programming Languages, pages 258\u2013270, 1996.","DOI":"10.1145\/237721.237788"},{"key":"276787_CR14","doi-asserted-by":"crossref","unstructured":"Eilenberg, S., and G.M. Kelly, \u2018Closed categories\u2019, in Proceedings of Conference on Categorical Algebra, La Jolla, 1966.","DOI":"10.1007\/978-3-642-99902-4_22"},{"key":"276787_CR15","doi-asserted-by":"crossref","unstructured":"Fairtlough, M., and M. Mendler, \u2018An intuitionistic modal logic with applications to the formal verification of hardware\u2019, in Proceedings of Conference on Computer Science Logic, volume 933 of Lecture Notes in Computer Science, 1995.","DOI":"10.1007\/BFb0022268"},{"key":"276787_CR16","doi-asserted-by":"crossref","unstructured":"Flagg, R.C., \u2018Church's thesis is consistent with epistemic arithmetic\u2019, In Intensional Mathematics, 1985.","DOI":"10.1016\/S0049-237X(08)70142-3"},{"issue":"2","key":"276787_CR17","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0304-3975(93)90011-H","volume":"110","author":"J. Gallier","year":"1993","unstructured":"Gallier, J., \u2018Constructive logics part I: A tutorial on proof systems and typed \u03bb-calculi\u2019, Theoretical Computer Science 110(2): 249\u2013339, 1993.","journal-title":"Theoretical Computer Science"},{"key":"276787_CR18","doi-asserted-by":"crossref","unstructured":"Gentzen, G., \u2018Investigations into logical deduction\u2019, in M.E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, pages 68\u2013131, North-Holland, 1969.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"276787_CR19","doi-asserted-by":"crossref","unstructured":"Ghilardi, S., and G. Meloni, \u2018Modal and tense predicate logic: models in presheaves and categorical conceptualization\u2019, in Categorical Algebra and its Applications, volume 1348 of Lecture Notes in Mathematics, pages 130\u2013142, 1988.","DOI":"10.1007\/BFb0081355"},{"key":"276787_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Girard, J.-Y., \u2018Linear logic\u2019, Theoretical Computer Science 50: 1\u2013101, 1987.","journal-title":"Theoretical Computer Science"},{"key":"276787_CR21","unstructured":"Girard, J.-Y., Y. Lafont, and P. Taylor, Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 1989."},{"key":"276787_CR22","unstructured":"Gor\u00c9, R.P., Cut-free Sequent and Tableau Systems for Propositional Normal Modal Logics, PhD thesis, Computer Laboratory, University of Cambridge, 1992. Available as Computer Laboratory Technical Report 257."},{"key":"276787_CR23","unstructured":"Howard, W.A., \u2018The formulae-as-types notion of construction\u2019, in J.R. Hindley and J.P. Seldin (eds.), To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism, Academic Press, 1980."},{"key":"276787_CR24","unstructured":"Lambek, J., and P.J. Scott, Introduction to Higher Order Categorical Logic, volume 7 of Cambridge studies in advanced mathematics, Cambridge University Press, 1987."},{"key":"276787_CR25","doi-asserted-by":"crossref","unstructured":"Mac Lane, S., Categories for the Working Mathematican, volume 5 of Graduate Texts in Mathematics, Springer Verlag, 1971.","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"276787_CR26","unstructured":"Martini, S., and A. Masini, \u2018A computational interpretation of modal proofs\u2019, Technical Report TR-27\/93, Dipartimento di informatica, Universit\u00e0 di Pisa, November 1993."},{"key":"276787_CR27","unstructured":"Mints, G.E., Selected Papers in Proof Theory, Bibliopolis, 1992."},{"key":"276787_CR28","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1023\/A:1005016206457","volume":"60","author":"G.E. Mints","year":"1998","unstructured":"Mints, G.E., \u2018Linear lambda-terms and natural deduction\u2019, Studia Logica 60: 209\u2013231, 1998.","journal-title":"Studia Logica"},{"issue":"5\u20136","key":"276787_CR29","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/s001530050106","volume":"37","author":"G.E. Mints","year":"1998","unstructured":"Mints, G.E., \u2018Normal deduction in the intuitionistic linear logic\u2019, Archive for Mathematical Logic 37(5\u20136): 415\u2013426, 1998.","journal-title":"Archive for Mathematical Logic"},{"issue":"1","key":"276787_CR30","first-page":"55","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E., \u2018Notions of computation and monads\u2019, Information and Control 93(1): 55\u201392, 1991.","journal-title":"Information and Control"},{"key":"276787_CR31","unstructured":"Pitts, A.M., \u2018Categorical logic\u2019, Technical Report 367, Computer Laboratory, University of Cambridge, May 1995."},{"key":"276787_CR32","unstructured":"Prawitz, D., Natural Deduction, volume 3 of Stockholm Studies in Philosophy, Almqvist and Wiksell, 1965."},{"key":"276787_CR33","doi-asserted-by":"crossref","unstructured":"Prawitz, D., \u2018Ideas and results in proof theory\u2019, In J.E. Fenstad (ed.), Proceedings of Second Scandinavian Logic Symposium, pages 235\u2013307, 1971.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"276787_CR34","series-title":"Technical Report","volume-title":"Topos-theoretic approaches to modalities","author":"G.E. Reyes","year":"1991","unstructured":"Reyes, G.E., and H. Zolfaghari, \u2018Topos-theoretic approaches to modalities\u2019, Technical Report 911\u20138, Universit\u00e9 de Montr\u00e9al, Qu\u00e9bec, April 1991."},{"issue":"4","key":"276787_CR35","first-page":"461","volume":"8","author":"T.W. Satre","year":"1972","unstructured":"Satre, T.W., \u2018Natural deduction rules for modal logics\u2019, Notre Dame Journal of Formal Logic 8(4): 461\u2013475, October 1972.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"276787_CR36","doi-asserted-by":"crossref","unstructured":"Schwichtenberg, H., \u2018Proof theory: Some applications of cut-elimination\u2019, in J. Barwise (ed.), Handbook of Mathematical Logic, chapter D.2, pages 867\u2013896, North Holland, 1977.","DOI":"10.1016\/S0049-237X(08)71124-8"},{"key":"276787_CR37","unstructured":"Simpson, A., The Proof Theory and Semantics of Intuitionistic Modal Logics, PhD thesis, University of Edinburgh, December 1993."},{"key":"276787_CR38","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","volume":"49","author":"C.P. Stirling","year":"1987","unstructured":"Stirling, C.P., \u2018Modal logics for communicating systems\u2019, Theoretical Computer Science 49: 311\u2013347, 1987.","journal-title":"Theoretical Computer Science"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005291931660.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005291931660\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005291931660.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:30:46Z","timestamp":1754631046000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005291931660"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,8]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,8]]}},"alternative-id":["276787"],"URL":"https:\/\/doi.org\/10.1023\/a:1005291931660","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,8]]}}}