{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T14:16:59Z","timestamp":1777645019450,"version":"3.51.4"},"reference-count":0,"publisher":"SAGE Publications","issue":"1","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/journals.sagepub.com\/page\/policies\/text-and-data-mining-license"}],"content-domain":{"domain":["journals.sagepub.com"],"crossmark-restriction":true},"short-container-title":["Fundamenta Informaticae"],"published-print":{"date-parts":[[2014,2]]},"abstract":"<jats:p>\n                    We aim to establish the multi-modal logic CK\n                    <jats:sub>n<\/jats:sub>\n                    as a baseline for a constructive correspondence theory of constructive modal logics. Just like many classical multi-modal logics may be studied as theories of the basic system K obtained by model-theoretic specialisation, we envisage constructive modal logics to be derived as proof-theoretic enrichments of CK\n                    <jats:sub>n<\/jats:sub>\n                    . The system CK\n                    <jats:sub>n<\/jats:sub>\n                    would then act as a core system for constructive contextual reasoning with controlled information flow. In this paper, as a first step towards this goal, we study CK\n                    <jats:sub>n<\/jats:sub>\n                    as a type theory and introduce its computational \u03bb-calculus, \u03bbCK\n                    <jats:sub>n<\/jats:sub>\n                    . Extending previous work on CK\n                    <jats:sub>n<\/jats:sub>\n                    , we present a cut-free contextual sequent system in the spirit of Masini's two-dimensional generalisation of natural deduction and Br\u00fcnnler's nested sequents and give a computational interpretation for CK\n                    <jats:sub>n<\/jats:sub>\n                    following the Curry-Howard Correspondence. The associated modal type theory \u03bbCK\n                    <jats:sub>n<\/jats:sub>\n                    permits an interpretation for both the modalities \u25a1 and \u25ca of CK\n                    <jats:sub>n<\/jats:sub>\n                    as type operators with simple and independent constructors and destructors, which has been missing in the literature. It is shown that the calculus satisfies subject reduction, strong normalisation and confluence. Since normal forms can be characterised by way of a Gentzen-style typing system with sub-formula property, \u03bbCK\n                    <jats:sub>n<\/jats:sub>\n                    is suitable for proof search in CK\n                    <jats:sub>n<\/jats:sub>\n                    . At the same time, \u03bbCK\n                    <jats:sub>n<\/jats:sub>\n                    enjoys natural deduction style typing which is important for programming applications. In contrast to most existing modal type theories, which are obtained as theories of the constructive modal logic S4, CK\n                    <jats:sub>n<\/jats:sub>\n                    is not bound to a particular contextual interpretation. Thus, \u03bbCK\n                    <jats:sub>n<\/jats:sub>\n                    constitutes the core of a functional language which provides static type checking of information processing to support safe contextual navigation in relational structures like those treated by description logics. We review some existing work on modal type theories and discuss their relation to \u03bbCK\n                    <jats:sub>n<\/jats:sub>\n                    .\n                  <\/jats:p>","DOI":"10.3233\/fi-2014-984","type":"journal-article","created":{"date-parts":[[2019,12,3]],"date-time":"2019-12-03T00:47:18Z","timestamp":1575334038000},"page":"125-162","update-policy":"https:\/\/doi.org\/10.1177\/sage-journals-update-policy","source":"Crossref","is-referenced-by-count":2,"title":["On the Computational Interpretation of CK\n                    <sub>n<\/sub>\n                    for Contextual Information Processing"],"prefix":"10.1177","volume":"130","author":[{"given":"Michael","family":"Mendler","sequence":"first","affiliation":[{"name":"Faculty of Information Systems and Applied Computer Sciences, The Otto-Friedrich-University of Bamberg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephan","family":"Scheele","sequence":"additional","affiliation":[{"name":"Faculty of Information Systems and Applied Computer Sciences, The Otto-Friedrich-University of Bamberg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","published-online":{"date-parts":[[2014,2,1]]},"container-title":["Fundamenta Informaticae"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2014-984","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/journals.sagepub.com\/doi\/pdf\/10.3233\/FI-2014-984","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T06:31:05Z","timestamp":1777444265000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/10.3233\/FI-2014-984"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":0,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.3233\/FI-2014-984"],"URL":"https:\/\/doi.org\/10.3233\/fi-2014-984","relation":{},"ISSN":["0169-2968","1875-8681"],"issn-type":[{"value":"0169-2968","type":"print"},{"value":"1875-8681","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2]]}}}