Journal
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC
Volume 9, Issue 3, Pages -Publisher
ASSOC COMPUTING MACHINERY
DOI: 10.1145/1352582.1352591
Keywords
design; theory; type theory; logical frameworks; intuitionistic modal logic
Categories
Ask authors/readers for more resources
The intuitionistic modal logic of necessity is based on the judgmental notion of categorical truth. In this article we investigate the consequences of relativizing these concepts to explicitly specified contexts. We obtain contextual modal logic and its type-theoretic analogue. Contextual modal type theory provides an elegant, uniform foundation for understanding metavariables and explicit substitutions. We sketch some applications in functional programming and logical frameworks.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available
Share Paper
