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

Norihiro Kamide


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.

[1] S. Baratella and A. Masini, An approach to infinitary temporal proof theory, Archive for Mathematical Logic 43:8 (2004), pp. 965–990. 
[2] S. Baratella and A. Masini, A proof-theoretic investigation of a logic of positions, Annals of Pure and Applied Logic 123 (2003), pp. 135–162. 
[3] Z. El-Abidine Benaissa, E. Moggi, W. Taha and T. Sheard, Logical modalities and multi-stage programming, Proceedings of Workshop on Intuitionistic Modal Logics and Applications (IMLA’99), 1999. 
[4] A. Biere, A. Cimatti, E.M. Clarke, O. Strichman and Y. Zhu, Bounded model checking, Advances in Computers 58 (2003), pp. 118–149. 
[5] A. Bolotov, A. Basukoski, O. Grigoriev and V. Shangin, Natural deduction calculus for linear-time temporal logic, Proceedings of the JELIA2006, Lecture Notes in Computer Science 4160 (2006), pp. 56–68. 
[6] S. Cerrito, M.C. Mayer and S. Prand, First order linear temporal logic over finite time structures, Lecture Notes in Computer Science 1705 (1999), pp. 62–76. [7] S. Cerrito and M.C. Mayer, Bounded model search in linear temporal logic and its application to planning, Lecture Notes in Computer Science 1397 (1998), pp. 124–140. 
[8] E.M. Clarke, O. Grumberg, and D.A. Peled, Model checking, The MIT Press, 1999. [9] R. Davies, A temporal-logic approach to binding-time analysis, Proceedings of the 11th Annual Symposium on Logic in Computer Science (LICS’96), 1996, pp. 184–195.
[10] R. Davies and F. Pfenning, A modal analysis of staged computation, Journal of the ACM 48:3 (2001), pp. 555–604. 
[11] J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and types, Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press, 1989. 
[12] E.A. Emerson, Temporal and modal logic, In Handbook of Theoretical Computer Science, Formal Models and Semantics (B), Jan van Leeuwen (Ed.), Elsevier and MIT Press, 1990, pp. 995–1072. 
[13] I. Hodkinson, F. Wolter and M. Zakharyaschev, Decidable fragments of first-order temporal logics, Annals of Pure and Applied Logic 106 (2000), pp. 85–134. [14] A. Indrzejczak, A labelled natural deduction system for linear temporal logic, Studia Logica 75 (2003), pp. 345–376. 
[15] N. Kamide, An equivalence between sequent calculi for linear-time temporal logic, Bulletin of the Section of the Logic 35:4 (2006), pp. 187–194. 
[16] N. Kamide, Embedding linear-time temporal logic into infinitary logic: application to cut-elimination for multi-agent infinitary epistemic linear-time temporal logic, Proceedeings of the 9th International Workshop on Computational Logic in Multi-Agent systems (CLIMA-9), Lecture Notes in Artificial Intelligence 5405 (2009), pp. 57–76. 
[17] N. Kamide and H. Wansing, Combining linear-time temporal logic with constructiveness and parconsistency, Journal of Applied Logic 8 (2010), pp. 33–61. [18] H. Kawai, Sequential calculus for a first order infinitary temporal logic, Zeitschrift fu¨r Mathematische Logik und Grundlagen der Mathematik 33 (1987), pp. 423–432. [
19] IK-Soon Kim, K. Yi and C. Calcagno, A polymorphic modal type system for Lisplike multi-staged languages, Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’06), 2006, pp. 257–268. 
[20] F. Kr¨oger, LAR: a logic of algorithmic reasoning, Acta Informatica 8 (1977), pp. 243–266. 
[21] E. Moggi, W. Taha, Z. El-Abidine Benaissa and T. Sheard, An idealized MetaML: simpler, and more expressive, Lecture Notes in Computer Science 1576 (1999), pp. 193–207. 
[22] A. Nanevski, Meta-programming with names and necessity, Proceedings of the 7th ACM SIGPLAN International Conference on Functional Programming (ICFP’02), 2002, pp. 206–217. 
[23] B. Paech, Gentzen-systems for propositional temporal logics, Lecture Notes in Computer Science 385 (1988), pp. 240–253. 
[24] R. Pliuˇskeviˇcius, Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus, Lecture Notes in Computer Science 502 (1991), pp. 504–528. 
[25] A. Pnueli, The temporal logic of programs, Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, 1977, pp. 46–57. 
[26] M.E. Szabo, A sequent calculus for Kr¨oger logic, Lecture Notes in Computer Science 148 (1980), pp. 295–303.
[27] A. Sza las, Concerning the semantic consequence relation in first-order temporal logic, Theoretical Computer Science 47:3 (1986), pp. 329–334.
[28] W. Taha and T. Sheard, Multi-stage programming with explicit annotations, Proceedings of Partial Evaluation and Semantics-Based Program Manipulation (PEPM’97), 1997, pp. 203–217.
[29] D. Wijesekera and A. Nerode, Tableaux for constructive concurrent dynamic logic, Annals of Pure and Applied Logic 135 (2005), pp. 1–72.
[30] Y. Yuse and A. Igarashi, A modal type system for multi-level generating extensions with persistent code, Proceedings of the 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2006), 2006, pp. 201– 212.

Czasopismo ukazuje się w sposób ciągły on-line.
Pierwotną formą czasopisma jest wersja elektroniczna.