Denotation of contextual modal type theory (CMTT): syntax and meta-programming

DOI10.1016/J.JAL.2012.07.002zbMath1280.03037arXiv1202.0904OpenAlexW3104304502MaRDI QIDQ1948284

Aleksandar Nanevski, Murdoch James Gabbay

Publication date: 2 May 2013

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1202.0904

zbMATH Keywords

higher-order logicsyntaxCurry-Howard correspondencemeta-programmingmodal logic S4contextual modal type theory

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items (1)

A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types

This page was built for publication: Denotation of contextual modal type theory (CMTT): syntax and meta-programming