Constructive linear-time temporal logic: proof systems and Kripke semantics

DOI10.1016/j.ic.2010.09.008zbMath1248.03031MaRDI QIDQ764262

Kensuke Kojima, Atsushi Igarashi

Publication date: 13 March 2012

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2010.09.008

zbMATH Keywords

cut elimination; sequent calculus; Kripke semantics; constructive linear-time temporal logic

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03B44: Temporal logic

Related Items

A Logical Foundation for Environment Classifiers, Constructive linear-time temporal logic: proof systems and Kripke semantics

Uses Software

• MiniML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Constructive modal logics. I
• Constructive linear-time temporal logic: proof systems and Kripke semantics
• Modal logics with functional alternative relations
• Propositional lax logic
• Monad as modality
• MetaML and multi-stage programming with explicit annotations
• Structural cut elimination. I: Intuitionistic and classical logic
• Environment classifiers
• A modal analysis of staged computation
• Intuitionistic tense and modal logic
• Computer Science Logic
• A polymorphic modal type system for lisp-like multi-staged languages
• Staged computation with names and necessity
• A Logical Foundation for Environment Classifiers