Paper Info
Title
On the Computational Interpretation of CKn for Contextual Information Processing
Abstract
We aim to establish the multi-modal logic CKn 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 CKn. The system CKn 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 CKn as a type theory and introduce its computational λ-calculus, λCKn. Extending previous work on CKn, we present a cut-free contextual sequent system in the spirit of Masini's two-dimensional generalisation of natural deduction and Brünnler's nested sequents and give a computational interpretation for CKn following the Curry-Howard Correspondence. The associated modal type theory λCKn permits an interpretation for both the modalities □ and ◊ of CKn 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, λCKn is suitable for proof search in CKn. At the same time, λCKn 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, CKn is not bound to a particular contextual interpretation. Thus, λCKn 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 λCKn.
Year
DOI
Venue
2014
10.3233/FI-2014-984
Fundam. Inform.
Keywords
Field
DocType
system ckn,computational interpretation,type theory,type operator,associated modal type theory,constructive modal logic,multi-modal logic ckn,contextual information processing,constructive modal logic s4,modal type theory,static type checking,existing modal type theory,contextual analysis,information processing,generalization,mathematical proofs,calculus
Discrete mathematics,Natural deduction,Subject reduction,Constructive,Computer science,Type theory,Description logic,Mathematical proof,Sequent,Modal logic
Journal
Volume
Issue
ISSN
130
1
0169-2968
Citations 
PageRank 
References 
0
0.34
17
Authors
2
Name
Order
Citations
PageRank
Michael Mendler131434.60
Stephan Scheele2174.36