A categorical model of predicate linear logic

• Autorzy: Demeterová E. , Mihályi D. , Novitzká V.

Identyfikatory

DOI

10.17512/jamcm.2015.1.03

• Języki publikacji: EN

Abstrakty

EN

Linear logic is one of the logical systems with special properties suitable for describing real processes used in computer science. It enables one to specify dynamics, non determinism, consecutive processes and important resources as memory and time on syntactic level. Moreover, its deduction system enables one to verify specified properties. Constructing an appropriate model based on categories can serve for modeling various program systems in the wide spectrum of computer science. Mainly, propositional linear logic is used for these purposes. The expression power of linear logic significantly grows by extending propositional logic with predicates and quantifiers. Our paper concerns itself with defining predicate linear logic together with its deduction system and our main aim is to construct a categorical model of predicate linear logic as a symmetric monoidal closed category.

Słowa kluczowe

EN

linear type theory; predicate linear logic; symmetric monoidal closed category

• Wydawca: Wydawnictwo Politechniki Częstochowskiej
• Czasopismo: Journal of Applied Mathematics and Computational Mechanics
• Rocznik: 2015
• Tom: Vol. 14, nr 1
• Strony: 27--42
• Opis fizyczny: Bibliogr. 22 poz., rys.

Twórcy

autor

Demeterová E.

• Department of Computers and Informatics, Faculty of Electrical Engineering and Informatics Technical University of Košice Košice, Slovak Republic

autor

Mihályi D.

• Department of Computers and Informatics, Faculty of Electrical Engineering and Informatics Technical University of Košice Košice, Slovak Republic

autor

Novitzká V.

• Department of Computers and Informatics, Faculty of Electrical Engineering and Informatics Technical University of Košice Košice, Slovak Republic

Bibliografia

• [1] Girard J.-Y., Linear logic, Theoretical Computer Science 1987, 50, 1-102.
• [2] Novitzká V., Mihályi D., Slodičák V., Categorical models of logical systems in the mathematical theory of programming, P. U. M. A 2006, 17, 3-4, 367-378.
• [3] Novitzká V., Mihályi D., Resource-oriented programming based on linear logic, Acta Polytechnica Hungarica 2007, 4(2), 157-166.
• [4] Mihályi D., Novitzká V., Prazňák P., Popovec P., Network routing modelled by game semantics, Studia Universitatis Babes-Bolyai, Informatica 2012, 57, 4, 19-29.
• [5] Mihályi D., Novitzká V., Towards the knowledge in coalgebraic model of IDS, Computing and Informatics 2014, 33, 1, 61-78.
• [6] Steingartner W., Novitzká V., Benčková M., Prazňák P., Considerations and ideas in component programming - towards to formal specification, Proc. of 25th Central European Conference on Information and Intelligent Systems CECIIS, Varaždin, Sept. 17-19, 2014, 332-339.
• [7] Mihályi D., Novitzká V., What about linear logic in computer science? Department of Computers and Informatics, Technical University of Košice, Acta Polytechnica Hungarica 2013, 10, 4.
• [8] Lincoln P., Linear Logic, SRI and Stanford University, 1992.
• [9] Novitzká V., Mihályi D., Slodičák V., Linear logical reasoning on programming, Acta Electrotechnica et Informatica 2006, 3, 6.
• [10] Girard J.-Y., Linear Logic: Its Syntax and Semantics, Cambridge University Press, 2003.
• [11] Yetter D.N., Quantales and (noncommutative) linear logic, Journal of Symbolic Logic 1990, 55(1), 41-64.
• [12] Girard J.-Y., Taylor P., Lafont Y., Proofs and Types, Cambridge University Press, New York 1989.
• [13] Girard J.-Y., On the Meaning of Logical Rules I: Syntax vs. Semantics, Institut de Mathematiques de Luminy, UPR 9016- CNRS 163, Avenue de Luminy, Case 930, F-13288 Marseille Cedex 09, 1998.
• [14] Ambler S.J., First order linear logic in symmetric monoidal closed categories, PhD. Thesis, University of Edinburgh, 1991.
• [15] Abramsky S., Computational interpretations of linear logic, Technical Report 90/20, Department of Computing, Imperial College, 1990, 1-15.
• [16] Hasegawa M., Categorical Glueing and Logical Predicates for Models of Linear Logic, Kyoto University, Research Institute for Mathematical Sciences, 1999.
• [17] Novitzká V., Slodičák V., Kategorické štruktúry a ich aplikácie v informatike 2010, ISBN 978- 80-89284-67-2.
• [18] de Paiva V., Categorical Semantics of Linear Logic for All, Palo Alto Research Center, Palo Alto 2006.
• [19] Barr M., Wells Ch., Category Theory for Computing Science, Prentice Hall International Ltd., Hertfordshire 1990.
• [20] Melliès P.-A., Categorical Semantics of Linear Logic, Panoramas et Syntheses 27, Citeseer, 2009.
• [21] Mihályi D., Novitzká V., Ľaľová M., Intrusion detection system episteme, Central European Journal of Computer Science 2012, 2, 3, 214-220.
• [22] Slodičák V., Some Useful Structures for Categorical Approach for Program Behavior, Journal of Information and Organizational Sciences 2011, 35, 1, 99-109.