Strong normalization of a typed lambda calculus for intuitionistic bounded linear - time temporal logic

• Autorzy: Kamide N.
• Języki publikacji: EN

Abstrakty

EN

Abstract. 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 A-calculus λAB[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 I. The strong normalization theorem for AB[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 framework 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.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2012
• Tom: Vol. 47
• Strony: 29--61
• Opis fizyczny: Bibliogr. 30 poz.

Twórcy

autor

Kamide N.

• Cyber University, Faculty of Information Technology and Business, Japan Cyber Educational Institute, Ltd. 4F, 1-11 Kitayamabushi-cho, Shinjuku-ku, Tokyo 162-0853, JAPAN

Bibliografia

• [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, Pro-ceedeings 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 fiir 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 Lisp-like multi-staged languages, Proceedings of ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'06), 2006, pp. 257-268.
• [20] F. Kroger, LAR: a logic of algorithmic reasoning, Acta Informática 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-programmmg 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. Pliuskevicius, 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 Kroger logic, Lecture Notes in Computer Science 148 (1980), pp. 295-303.
• [27] A. Szalas, 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.