PL EN


2012 | 47 | 29–61
Article title

Strong Normalization of a Typed Lambda Calculus for Intuitionistic Bounded Linear-time Temporal Logic

Authors
Selected contents from this journal
Title variants
Languages of publication
EN
Abstracts
EN
Linear-time temporal logics (LTLs) are known to be useful for verifying concurrent systems, and a simple natural deduction framework for LTLs has been required to obtain a good computational interpretation. In this paper, a typed -calculus B[l] with a Curry-Howard correspondence is introduced for an in-tuitionistic bounded linear-time temporal logic B[l], of which the time domain is bounded by a fixed positive integer l. The strong normalization theorem for B[l] is proved as a main result. The base logic B[l] is defined as a Gentzen-type sequent calculus, and despite the restriction on the time domain, B[l] can derive almost all the typical temporal axioms of LTLs. The proposed frame-work allows us to obtain a uniform and simple proof-theoretical treatment of both natural deduction and sequent calculus, i.e., the equivalence between them, the cut-elimination theorem, the decidability theorem, the Curry-Howard correspondence and the strong normalization theorem can be obtained uniformly.
Keywords
Year
Issue
47
Pages
29–61
Physical description
Dates
online
2012-08-23
Contributors
  • Cyber University, Faculty of Information Technology and Business, Japan Cyber Educational Institute, Ltd
References
Document Type
Publication order reference
YADDA identifier
bwmeta1.element.desklight-aad82ad0-6891-420b-abe1-28fb032698bd
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.