A Logical Foundation for Environment Classifiers

DOI10.1007/978-3-642-02273-9_25zbMath1211.68064arXiv1010.3806OpenAlexW1960887414MaRDI QIDQ5902143

Atsushi Igarashi, Takeshi Tsukada

Publication date: 7 July 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

modal logicCurry-Howard correspondenceenvironment classifiersmulti-stage calculus

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Uses Software

• MiniML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• MetaML and multi-stage programming with explicit annotations
• A tour of tempo: a program specializer for the C language
• Environment classifiers
• A modal analysis of staged computation
• Closed types for a safe imperative MetaML
• Intuitionistic Letcc via Labelled Deduction
• Contextual modal type theory
• Programming Languages and Systems
• A polymorphic modal type system for lisp-like multi-staged languages
• Staged computation with names and necessity