Multimodal Dependent Type Theory
- Submitting institution
-
University of Bristol
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 243014445
- Type
- E - Conference contribution
- DOI
-
10.1145/3373718.3394736
- Title of conference / published proceedings
- LICS '20 : Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
- First page
- 492
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- July
- Year of publication
- 2020
- 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
-
3
- Research group(s)
-
D - Fundamentals of Computing
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- This paper is the first work that develops a modal dependent type theory that supports an arbitrary number of interacting modalities. Despite only appearing in 2020 this paper shows marks of early impact, leading to invited talks at the University of Paris, Stockholm University, and the IT University of Copenhagen. Moreover, colleagues at Carnegie Mellon University have based their new work on it (arXiv:2005.11290), leading to a new collaboration. This was one of the very few papers at LICS 2020 to receive an invitation for submission of an expanded version to the Logical Methods in Computer Science journal.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -