Contextual modal type theory with polymorphic contexts

DOI10.1007/978-3-031-30044-8_11MaRDI QIDQ6535241zbMATH OpenFDO

Authors Yuito Murase, Yuichi Nishiwaki, Atsushi Igarashi

Publication date 24 November 2023

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30044-8_11

zbMATH Keywords

contextual modal typesFitch-style modal lambda-calculimetaprogrammingpolymorphic contexts

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(2)

• Semantical analysis of contextual types
• scientific article; zbMATH DE number 6174931 (Why is no real title available?)

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)