Contextual modal type theory with polymorphic contexts

DOI10.1007/978-3-031-30044-8_11zbMATH Open1541.68089MaRDI QIDQ6535241FDOQ6535241

Authors: Yuito Murase, Yuichi Nishiwaki, Atsushi Igarashi 

Publication date: 24 November 2023

Recommendations

• Contextual modal type theory
• Denotation of contextual modal type theory (CMTT): syntax and meta-programming
• Multimodal dependent type theory
• On the computational interpretation of \(\mathbf{CK}_{n}\) for contextual information processing
• scientific article; zbMATH DE number 6174931

zbMATH Keywords

metaprogrammingcontextual modal typesFitch-style modal lambda-calculipolymorphic contexts

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cites Work

• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• VeriML: typed computation of logical terms inside a language with effects
• A judgmental reconstruction of modal logic
• Handlers of Algebraic Effects
• Title not available (Why is that?)
• Lectures on the Curry-Howard isomorphism
• A modal analysis of staged computation
• Title not available (Why is that?)
• Contextual modal type theory
• Environment classifiers
• A temporal logic approach to binding-time analysis
• A polymorphic modal type system for Lisp-like multi-staged languages
• Title not available (Why is that?)
• Staged computation with names and necessity
• A Logical Foundation for Environment Classifiers
• Macros as multi-stage computations: type-safe, generative, binding macros in MacroML
• Title not available (Why is that?)
• Fitch-style modal lambda calculi
• Staged computation with staged lexical scope
• Refined environment classifiers. Type- and scope-safe code generation with mutable cells

Cited In (1)

• Title not available (Why is that?)

This page was built for publication: Contextual modal type theory with polymorphic contexts

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535241)