- Tytuł:
- Strong Normalization of a Typed Lambda Calculus for Intuitionistic Bounded Linear-time Temporal Logic
- Autorzy:
- Kamide, Norihiro
- Powiązania:
- https://bibliotekanauki.pl/articles/1368573.pdf
- Data publikacji:
- 2012
- Wydawca:
- Uniwersytet Jagielloński. Wydawnictwo Uniwersytetu Jagiellońskiego
- Opis:
- 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 $\lambda$-calculus $\lambda_{B[l]}$ with a Curry-Howard correspondence is introduced for an intuitionistic 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 $\lambda_{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.
- Źródło:
-
Reports on Mathematical Logic; 2012, 47; 29-61
0137-2904
2084-2589 - Pojawia się w:
- Reports on Mathematical Logic
- Dostawca treści:
- Biblioteka Nauki
Artykuł