Dual-Context Calculi for Modal Logic
- Submitting institution
-
University of Bristol
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 243014433
- Type
- E - Conference contribution
- DOI
-
10.1109/LICS.2017.8005089
- Title of conference / published proceedings
- 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- First page
- 1
- Volume
- -
- Issue
- -
- ISSN
- 1043-6871
- Open access status
- Technical exception
- Month of publication
- August
- Year of publication
- 2017
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
0
- Research group(s)
-
D - Fundamentals of Computing
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper is the first to systematically develop the theory of a large class of modal type systems. A revised and expanded version with full proofs has appeared in the Logical Methods in Computer Science journal. It exerted influence on later work, including Fitch-style systems (Clouston, FoSSaCS 2018), and multimodal dependent type theory (Gratzer et al, LICS 2020). It further pushed the work of Kavvos and colleagues towards two new topics, namely Homotopy Type Theory (where similar systems are used in the formalisation of mathematics), and concurrent separation logic (where a GL-style modal operator is used).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
