{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:22:51Z","timestamp":1755220971524,"version":"3.43.0"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"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":[[2003,2]]},"DOI":"10.1023\/a:1022937306253","type":"journal-article","created":{"date-parts":[[2003,4,7]],"date-time":"2003-04-07T18:16:51Z","timestamp":1049739411000},"page":"51-80","source":"Crossref","is-referenced-by-count":1,"title":["Intensional Completeness in an Extension of G\u00f6del\/Dummett Logic"],"prefix":"10.1007","volume":"73","author":[{"given":"Matt","family":"Fairtlough","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Mendler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5117571_CR1","doi-asserted-by":"crossref","first-page":"249","DOI":"10.2307\/2266613","volume":"17","author":"H. B. Curry","year":"1952","unstructured":"Curry, H. B., \u2018The elimination theorem when modality is present\u2019, Journal of Symbolic Logic, 17:249\u2013265, 1952.","journal-title":"Journal of Symbolic Logic"},{"key":"5117571_CR2","unstructured":"Curry, H. B., A Theory of Formal Deducibility, vol. 6 of Notre Dame Mathematical Lectures. Notre Dame, Indiana, second edition, 1957."},{"key":"5117571_CR3","doi-asserted-by":"crossref","unstructured":"Dragalin, A. G., Mathematical Intuitionism. Introduction to Proof Theory. American Mathematical Society, 1988.","DOI":"10.1090\/mmono\/067"},{"key":"5117571_CR4","doi-asserted-by":"crossref","first-page":"644","DOI":"10.2307\/2272042","volume":"41","author":"H. C. M. De Swart","year":"1976","unstructured":"De Swart, H. C. M., \u2018Another intuitionistic completeness proof\u2019, Journal of Symbolic Logic, 41:644\u2013662, 1976.","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"5117571_CR5","doi-asserted-by":"crossref","first-page":"97","DOI":"10.2307\/2964753","volume":"24","author":"M. Dummett","year":"1959","unstructured":"Dummett, M., \u2018A propositional calculus with a denumerable matrix\u2019, Journal of Symbolic Logic, 24(2):97\u2013106, June 1959.","journal-title":"Journal of Symbolic Logic"},{"key":"5117571_CR6","volume-title":"Elements of Intuitionism","author":"M. Dummett","year":"1977","unstructured":"Dummett, M., Elements of Intuitionism, Clarendon Press, Oxford, 1977."},{"issue":"1","key":"5117571_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1997.2627","volume":"137","author":"M. Fairtlough","year":"1997","unstructured":"Fairtlough, M. and M. V. Mendler, \u2018Propositional Lax Logic\u2019, Information and Computation, 137(1):1\u201333, August 1997.","journal-title":"Information and Computation"},{"key":"5117571_CR8","doi-asserted-by":"crossref","unstructured":"Fairtlough, M., M. Mendler, and X. Cheng, \u2018Abstraction and refinement in higher-order logic\u2019, in R. J. Boulton and P. B. Jackson, editors, 14th International Conference on Theorem Proving in Higher Order Logic (TPHOLs'2001, LNCS 2152, pp. 201\u2013216, Springer, September 2001.","DOI":"10.1007\/3-540-44755-5_15"},{"key":"5117571_CR9","unstructured":"Fairtlough, M., 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."},{"key":"5117571_CR10","unstructured":"Friedman, H., \u2018Intuitionistic completeness of Heyting's predicate calculus\u2019, Notices of the American Mathematical Society, 22, 1975."},{"key":"5117571_CR11","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1002\/malq.19810273104","volume":"27","author":"R. I. Goldblatt","year":"1981","unstructured":"Goldblatt, R. I., \u2018Grothendieck topology as geometric modality\u2019, 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":"5117571_CR12","unstructured":"Goldblatt, R., Topoi: The categorical analysis of logic, North Holland, 2nd edition, 1986."},{"key":"5117571_CR13","unstructured":"Johnstone, P. T., Stone spaces, Cambridge University Press, 1982."},{"key":"5117571_CR14","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/BF01186549","volume":"35","author":"A. Kolmogoroff","year":"1932","unstructured":"Kolmogoroff, A., \u2018Zur Deutung der intuitionistischen Logik\u2019, Mathematische Zeitschrift, 35:58\u201365, 1932.","journal-title":"Mathematische Zeitschrift"},{"key":"5117571_CR15","doi-asserted-by":"crossref","unstructured":"Kripke, S., \u2018Semantical analysis of intuitionistic logic I\u2019, in J. Crossley and M. Dummett, editors, Formal Systems and Recursive Functions, pp. 92\u2013129, North-Holland, 1963.","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"5117571_CR16","doi-asserted-by":"crossref","unstructured":"Lawvere, F. W, \u2018Introduction to toposes, algebraic geometry and logic\u2019, in Lecture Notes in Mathematics, no. 274, pp. 1\u201312, Springer-Verlag, 1972.","DOI":"10.1007\/BFb0073962"},{"key":"5117571_CR17","doi-asserted-by":"crossref","unstructured":"Lopez-Escobar, E. G. K. and W. Veldman, \u2018Intuitionistic completeness of a restricted second-order logic\u2019, in ISLIC Proof Theory Symposium, LNCS 500, pp. 198\u2013232, Springer, 1974.","DOI":"10.1007\/BFb0079553"},{"key":"5117571_CR18","doi-asserted-by":"crossref","unstructured":"Lipton, J., \u2018Constructive Kripke semantics and realizability\u2019, in Y. N. Moschovakis, editor, Proc. Logic for Computer Science, pp. 319\u2013357, Springer, 1991.","DOI":"10.1007\/978-1-4612-2822-6_13"},{"key":"5117571_CR19","unstructured":"Mac Lane, S., Categories for the Working Mathematician, Springer-Verlag, 1988."},{"key":"5117571_CR20","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF02483860","volume":"12","author":"D. S. Macnab","year":"1981","unstructured":"Macnab, D. S., \u2018Modal operators on Heyting algebras\u2019, Algebra Universalis, 12:5\u201329, 1981.","journal-title":"Algebra Universalis"},{"issue":"4","key":"5117571_CR21","first-page":"857","volume":"7","author":"J. T. Medvedev","year":"1966","unstructured":"Medvedev, Ju. T., \u2018Interpretation of logical formulas by means of finite problems\u2019, Soviet Math. Dokl., 7(4):857\u2013860, 1966.","journal-title":"Soviet Math. Dokl."},{"key":"5117571_CR22","unstructured":"Mendler, M., A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Edinburgh University, Department of Computer Science, ECS-LFCS\u201393\u2013255, 1993."},{"issue":"6","key":"5117571_CR23","doi-asserted-by":"crossref","first-page":"821","DOI":"10.1093\/jigpal\/8.6.821","volume":"8","author":"M. Mendler","year":"2000","unstructured":"Mendler, M., \u2018Characterising combinational timing analyses in intuitionistic modal logic\u2019, The Logic Journal of the IGPL, 8(6):821\u2013852, November 2000. Abstract appeared ibid. vol. 6, No. 6, (Nov 1998).","journal-title":"The Logic Journal of the IGPL"},{"key":"5117571_CR24","doi-asserted-by":"crossref","unstructured":"Mendler, M. and M. Fairtlough, \u2018Ternary simulation: A refinement of binary functions or an abstraction of real-time behaviour?\u2019, in M. Sheeran and S. Singh, editors, Proc. 3rd Workshop on Designing Correct Circuits (DCC'96), Springer Electronic Workshops in Computing, 1996.","DOI":"10.14236\/ewic\/DCC1996.8"},{"key":"5117571_CR25","unstructured":"Mitchell, J. and E. Moggi, \u2018Kripke-style models for typed lambda calculus\u2019, in Proc. Logic in Computer Science, 1987."},{"issue":"4","key":"5117571_CR26","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1305\/ndjfl\/1093635238","volume":"30","author":"P. Miglioli","year":"1989","unstructured":"Miglioli, P., U. Moscato, M. Ornaghi, S. Quazza, and G. Usberti, \u2018Some results on intermediate constructive logics\u2019, Notre Dame Journal of Formal Logic, 30(4):543\u2013562, 1989.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"5117571_CR27","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E. Moggi","year":"1991","unstructured":"Moggi, E., \u2018Notions of computation and monads\u2019, Information and Computation, 93:55\u201392, 1991.","journal-title":"Information and Computation"},{"key":"5117571_CR28","doi-asserted-by":"crossref","unstructured":"Troelstra, A. S., \u2018Realizability\u2019, in S. R. Buss, editor, Handbook of Proof Theory, chapter VI, pp. 407\u2013474, Elsevier, 1998.","DOI":"10.1016\/S0049-237X(98)80021-9"},{"key":"5117571_CR29","unstructured":"Troelstra, A. S. and D. Van Dalen, Constructivism in Mathematics, North-Holland, 1988."},{"key":"5117571_CR30","doi-asserted-by":"crossref","unstructured":"Van Dalen, D., \u2018Intuitionistic logic\u2019, in D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, volume III, chapter 4, pp. 225\u2013339, Reidel, 1986.","DOI":"10.1007\/978-94-009-5203-4_4"},{"key":"5117571_CR31","doi-asserted-by":"crossref","first-page":"159","DOI":"10.2307\/2272955","volume":"41","author":"W. Veldman","year":"1976","unstructured":"Veldman, W., \u2018An intuitionistic completeness theorem for intuitionistic predicate logic\u2019, Journal of Symbolic Logic, 41:159\u2013166, 1976.","journal-title":"Journal of Symbolic Logic"},{"key":"5117571_CR32","doi-asserted-by":"crossref","unstructured":"Wadler, P., \u2018Comprehending monads\u2019, in Conference on Lisp and Functional Programming, ACM Press, June 1990.","DOI":"10.1145\/91556.91592"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022937306253.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1022937306253\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1022937306253.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:28:47Z","timestamp":1754630927000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1022937306253"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["5117571"],"URL":"https:\/\/doi.org\/10.1023\/a:1022937306253","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2003,2]]}}}