{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,14]],"date-time":"2026-05-14T11:19:07Z","timestamp":1778757547298,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540600176","type":"print"},{"value":"9783540494041","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0022268","type":"book-chapter","created":{"date-parts":[[2005,11,22]],"date-time":"2005-11-22T06:12:29Z","timestamp":1132639949000},"page":"354-368","source":"Crossref","is-referenced-by-count":12,"title":["An intuitionistic modal logic with applications to the formal verification of hardware"],"prefix":"10.1007","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","published-online":{"date-parts":[[2005,6,15]]},"reference":[{"key":"26_CR1","volume-title":"Draft Technical Report","author":"N. Benton","year":"1993","unstructured":"N. Benton, G. Bierman, and V. de Paiva. Computational types from a logical perspective I. Draft Technical Report, Computer Laboratory University of Cambridge, U.K., August 1993."},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"B. Chellas. Modal Logic. Cambridge University Press, 1980.","DOI":"10.1017\/CBO9780511621192"},{"key":"26_CR3","doi-asserted-by":"crossref","first-page":"249","DOI":"10.2307\/2266613","volume":"17","author":"H. B. Curry","year":"1952","unstructured":"H. B. Curry. The elimination theorem when modality is present. Journal of Symbolic Logic, 17:249\u2013265, 1952.","journal-title":"Journal of Symbolic Logic"},{"key":"26_CR4","volume-title":"volume 6 of Notre Dame Mathematical Lectures","author":"H. B. Curry","year":"1957","unstructured":"H. B. Curry. A Theory of Formal Deducibility, volume 6 of Notre Dame Mathematical Lectures. Notre Dame, Indiana, second edition, 1957.","edition":"second edition"},{"key":"26_CR5","volume-title":"Elements of Intuitionism","author":"M. Dummett","year":"1977","unstructured":"M. Dummett. Elements of Intuitionism. Clarendon Press, Oxford, 1977."},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"W. B. Ewald. Intuitionistic tense and modal logic. Journal of Symbolic Logic, 51, 1986.","DOI":"10.2307\/2273953"},{"key":"26_CR7","unstructured":"M. Fairtlough and M. Mendier. An intuitionistic modal logic with applications to the formal verification of hardware. Technical Report ID-TR:1994-13, Department of Computer Science, Technical University of Denmark, 1994."},{"key":"26_CR8","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":"26_CR9","doi-asserted-by":"crossref","unstructured":"M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"26_CR10","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF01881550","volume":"45","author":"L. L. Maksimova","year":"1986","unstructured":"L. L. Maksimova. On maximal intermediate logics with the disjunction property. Studia Logica, 45:69\u201345, 1986.","journal-title":"Studia Logica"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"M. Mendler. Constrained proofs: A logic for dealing with behavioural constraints in formal hardware verification. In G. Jones and M. Sheeran, editors, Designing Correct Circuits, pages 1\u201328. Springer, 1990.","DOI":"10.1007\/978-1-4471-3544-9_1"},{"key":"26_CR12","unstructured":"M. Mendler. A Modal Logic for Handling Behavioural Constraints in Formal Hardware Verification. PhD thesis, Edinburgh University, Department of Computer Science, ECS-LFCS-93-255, 1993."},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"E. Moggi. Computational lambda-calculus and monads. In Proceedings LICS'89, pages 14\u201323, June 1989.","DOI":"10.1109\/LICS.1989.39155"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"G. Plotkin and C. Stirling. A framework for intuitionistic modal logics. In Theoretical aspects of reasoning about knowledge, pages 399\u2013406, Monterey, 1986.","DOI":"10.1016\/B978-0-934613-04-0.50032-6"},{"key":"26_CR15","unstructured":"A. Simpson. The Proof Theory and Semantics of Intuitionistic Modal Logic. PhD thesis, University of Edinburgh, Department of Computer Science, 1994."},{"key":"26_CR16","unstructured":"A. S. Troelstra and D. van Dalen. Constructivism in Mathematics, volume II. North-Holland, 1988."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022268","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T02:43:22Z","timestamp":1586573002000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022268"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600176","9783540494041"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0022268","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}