{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T15:32:42Z","timestamp":1775489562636,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540425540","type":"print"},{"value":"9783540448020","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44802-0_21","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:15:38Z","timestamp":1180656938000},"page":"292-307","source":"Crossref","is-referenced-by-count":36,"title":["Categorical and Kripke Semantics for Constructive S4 Modal Logic"],"prefix":"10.1007","author":[{"given":"Natasha","family":"Alechina","sequence":"first","affiliation":[]},{"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[]},{"given":"Valeria","family":"de Paiva","sequence":"additional","affiliation":[]},{"given":"Eike","family":"Ritter","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,30]]},"reference":[{"key":"21_CR1","doi-asserted-by":"crossref","unstructured":"N. Benton, G. Bierman, and V. dePaiva. Computational types from a logical perspective. Journal of Functional Programming, 8(2), 1998.","DOI":"10.1017\/S0956796898002998"},{"key":"21_CR2","unstructured":"G. M. Bierman and V. de Paiva. Intuitionistic necessity revisited. Technical Report CSR-96-10, University of Birmingham, School of Computer Science, June 1996."},{"key":"21_CR3","unstructured":"J. Benthem, van. Modal logic and classical logic. Bibliopolis, Naples, 1983."},{"key":"21_CR4","unstructured":"Z. Benaissa, E. Moggi, W. Taha, and T. Sheard. Logical modalities and multi-stage programming. In Workshop on Intuitionistic Modal Logics and Application (IMLA\u201999), Satellite to FLoC\u201999, Trento, Italy, 6th July 1999. Proceedings available from http:\/\/www.dcs.shef.ac.uk\/~floc99im ."},{"key":"21_CR5","unstructured":"H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures Notre Dame, Indiana, second edition, 1957."},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"R. Davies and F. Pfenning. A modal analysis of staged computation. In Guy Steele, Jr., editor, Proc. of 23rd POPL, pages 258\u2013270. ACM Press, 1996.","DOI":"10.1145\/237721.237788"},{"key":"21_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-62688-3_34","volume-title":"Proc. of TLCA\u201997","author":"J. Despeyroux","year":"1997","unstructured":"J. Despeyroux, F. Pfenning, and C. Sch\u00fcrmann. Primitive recursion for higher-order abstract syntax. In P. de Groote and J. Roger Hindley, editors, Proc. of TLCA\u201997, pages 147\u2013163. LNCS 242, Springer Verlag, 1997."},{"key":"21_CR8","volume-title":"Elements of Intuitionism","author":"M. Dummett","year":"1977","unstructured":"M. Dummett. Elements of Intuitionism Clarendon Press, Oxford, 1977."},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"W. B. Ewald. Intuitionistic tense and modal logic. Journal of Symbolic Logic, 51, 1986.","DOI":"10.2307\/2273953"},{"key":"21_CR10","first-page":"31","volume":"39","author":"K. Fine","year":"1974","unstructured":"K. Fine. An incomplete logic containing S4. Theoria, 39:31\u201342, 1974.","journal-title":"Theoria"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"M. Fairtlough and M. Mendler. Propositional lax logic. Information and Computation, 137, 1997.","DOI":"10.1006\/inco.1997.2627"},{"key":"21_CR12","unstructured":"M. Fairtlough, M. Mendler, and M. Walton. First-order lax logic as a framework for constraint logic programming. Technical Report MIP-9714, University of Passau, July 1997. Postscript available through http:\/\/www.dcs.shef.ac.uk\/~michael ."},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"G. Fischer-Servi. Semantics for a class of intuitionistic modal calculi. In M. L. Dalla Chiara, editor, Italian Studies in the Philosophy of Science, pages 59\u201372. Reidel, 1980.","DOI":"10.1007\/978-94-009-8937-5_5"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Neil Ghani, Valeria de Paiva, and Eike Ritter. Explicit Substitutions for Constructive Necessity. In Proceedings ICALP\u201998, 1998.","DOI":"10.1007\/BFb0055098"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"J. Goubault-Larrecq. Logical foundations of eval\/quote mechanisms, and the modal logic S4. Manuscript, 1996.","DOI":"10.1007\/978-94-011-3981-6_5"},{"key":"21_CR16","first-page":"31","volume":"6","author":"R. Goldblatt","year":"1976","unstructured":"R. Goldblatt. Metamathematics of modal logic. Reports on Mathematical Logic, 6,7:31\u201342, 21\u201352, 1976.","journal-title":"Reports on Mathematical Logic"},{"key":"21_CR17","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1002\/malq.19810273104","volume":"27","author":"R. Goldblatt","year":"1981","unstructured":"R. Goldblatt. Grothendieck Topology as Geometric Modality. Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik, 27:495\u2013529, 1981.","journal-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik"},{"key":"21_CR18","unstructured":"R. Goldblatt. Mathematics of Modality. CSLI Lecture Notes No. 43. Center for the Study of Language and Information, Stanford University, 1993."},{"key":"21_CR19","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0022-4049(98)00170-4","volume":"148","author":"B. P. Hilken","year":"2000","unstructured":"B. P. Hilken. Duality for intuitionistic modal algebras. Journal of Pure and Applied Algebra, 148:171\u2013189, 2000.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"21_CR20","unstructured":"P. T. Johnstone. Stone Spaces. Cambridge University Press, 1982."},{"key":"21_CR21","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0304-3975(96)00169-7","volume":"175","author":"S. Kobayashi","year":"1997","unstructured":"S. Kobayashi. Monad as modality. Theoretical Computer Science, 175:29\u201374, 1997.","journal-title":"Theoretical Computer Science"},{"key":"21_CR22","doi-asserted-by":"crossref","unstructured":"J. Lambek and Ph. J. Scott. Introduction to Higher-Order Categorical Logic. Cambridge University Press, 1985.","DOI":"10.1090\/conm\/030\/749773"},{"key":"21_CR23","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/BF02483860","volume":"12","author":"D. S. Macnab","year":"1981","unstructured":"D. S. Macnab. Modal operators on Heyting algebras. Algebra Universalis, 12:5\u201329, 1981.","journal-title":"Algebra Universalis"},{"key":"21_CR24","unstructured":"M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Department of Computer Science, University of Edinburgh, ECS-LFCS-93-255, March 1993."},{"issue":"6","key":"21_CR25","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1093\/jigpal\/8.6.821","volume":"8","author":"M. Mendler","year":"2000","unstructured":"M. Mendler. Characterising combinational timing analyses in intuitionistic modal logic. The Logic Journal of the IGPL, 8(6):821\u2013852, November 2000.","journal-title":"The Logic Journal of the IGPL"},{"key":"21_CR26","doi-asserted-by":"crossref","unstructured":"E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55\u201392, July 1991.","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"F. Pfenning and R. Davies. A judgemental reconstruction of modal logic. Mathematical Structures in Computer Science, 2001.","DOI":"10.1017\/S0960129501003322"},{"key":"21_CR28","unstructured":"D. Prawitz. Natural Deduction: A Proof-Theoretic Study. Almqvist and Wiksell, 1965."},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"G. Plotkin and C. Stirling. A framework for intuitionistic modal logics. In Theoretical aspects of reasoning about knowledge, Monterey, 1986.","DOI":"10.1016\/B978-0-934613-04-0.50032-6"},{"key":"21_CR30","unstructured":"A.K. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, 1994."},{"key":"21_CR31","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1111\/j.1755-2567.1974.tb00077.x","volume":"40","author":"S.K. Thomason","year":"1974","unstructured":"S.K. Thomason. An incompleteness theorem in modal logic. Theoria, 40:30\u201334, 1974.","journal-title":"Theoria"},{"key":"21_CR32","unstructured":"A. S. Troelstra and D. vanDalen. Constructivism in Mathematics, volume II. North-Holland, 1988."},{"key":"21_CR33","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/0168-0072(90)90059-B","volume":"50","author":"D. Wijesekera","year":"1990","unstructured":"D. Wijesekera. Constructive modal logic I. Annals of Pure and Applied Logic, 50:271\u2013301, 1990.","journal-title":"Annals of Pure and Applied Logic"},{"key":"21_CR34","unstructured":"F. Wolter and M. Zakharyaschev. Intuitionistic Modal Logics. In Logic in Florence, 1995."},{"key":"21_CR35","unstructured":"F. Wolter and M. Zakharyaschev. Intuitionistic modal logics as fragments of classical bimodal logics. In E. Orlowska, editor, Logic at Work. Kluwer, 1997."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44802-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,11]],"date-time":"2023-05-11T23:47:36Z","timestamp":1683848856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44802-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425540","9783540448020"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-44802-0_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}