UNIVERSAL LOGIC METHODS IN COMPUTER SCIENCE

project PN-II-ID-PCE-2011-3-0439, funded by UEFISCDI under contract 29/5.10.2011


Domain PE.Mathematics, Physical Sciences, Information and Communication, Engineering, Universe and Earth Sciences
Subdomain Mathematical foundations: all areas of mathematics, pure and applied, plus mathematical foundations of computer science, mathematical physics and statistics

Project summary

Universal logic is a body of general theories of logical structures that respond to the recent big multiplicity of logical systems from mathematical logic and from computer science. It represents the most modern trend in mathematical logic and it is also deeply rooted in computer science. One of the major universal logic sub-areas, namely the institution theory of Goguen and Burstall, originates from algebraic specification where it has gained a paramount foundational status, with its role being spread to other logic-based computer science areas. In this project we develop a number of institution theoretic methods in formal specification and verification applicable also to other logic-based computer science areas. These include (1) a new general foundational approach to structuring and modularity of specification and programs that unifies the existing ones at a higher level of abstraction, (2) a logic-independent development of formal verification methodologies providing solid foundations for formal verifications applicable to a wide variety of specification formalisms, and (3) an institution theoretic approach to logical heterogeneity and combination of logical systems and of logic translations that addresses combination both at the syntactic and the semantic level and which constitutes foundations for combinations of logic-based computing paradigms. The significance of (3) extends into the heart of one of the hot issues in logic.

▲

Members

Răzvan Diaconescu
CS1, project director (Simion Stoilow Institute of Mathematics of the Romanian Academy – IMAR)
Ionuț Țuțu
PhD student (Royal Holloway University of London)
Andrei Sipoș
PhD student (University of Bucharest)
▲

Publications


    PHASE 6 (2016)

  1. R. Diaconescu: Institution Theory, Internet Encyclopedia of Philosophy (2016).
  2. I. Țuțu, J.L. Fiadeiro: Foundations of Graph Transformation as a Logic-Programming Language, in  23rd International Workshop on Algebraic Development Techniques (WADT 2016),  (2016).
  3. I. Țuțu, R. Diaconescu: A pushout-style approach to parameterised behavioural specifications, Theoretical Computer Science, Elsevier (submitted).

    4. PHASE 5 (2015)

  4. R. Diaconescu: Structuring of Specification Modules (extended), Computer Science Journal of Moldova 23(2):135-152), (2015).
  5. R. Diaconescu: Structuring of Specification Modules, in S. Cojocaru and C. Gaindric (Eds.): Workshop on Foundations of Informatics 2015, 4-13, Institute of Mathematics and Computer Science, Academy of Sciences of Moldova volume 9463 of Lecture Notes in Computer Science
  6. I. Țuțu, J.L. Fiadeiro: Revisiting the Institutional Approach to Herbrand’s Theorem, in L.S. Moss and P. Sobocinski (Eds.): CALCO 2015, Leibniz International Proceedings in Informatics, 35:304-319, Schloss Dagstuhl (2015).
  7. R. Diaconescu: Functorial Semantics of First-Order Views, Theoretical Computer Science, Elsevier  http://dx.doi.org/10.1016/j.tcs.2016.09.009.
  8. R. Diaconescu: Implicit Kripke Semantics and Ultraproducts in Stratified Institutions, J. Logic and Computation, DOI:10.1093/logcom/exw018, Oxford Univ. Press.
  9. M. Codescu, R. Diaconescu, I. Țuțu (Eds.): Recent Trends in Algebraic Development Techniques – 22nd International Workshop, WADT 2014, revised selected papers, volume 9463 of Lecture Notes in Computer Science, Springer (2015).

    10. PHASE 4 (2014)

  10. I. Țuțu, J. Fiadeiro: From conventional to institution-independent logic programming, J. Logic and Computation DOI:10.1093/logcom/exv021, Oxford University Press (2015). IF2014 = 0.512 RIS2014 = 1.186
  11. I. Țuțu, J. Fiadeiro: Service-Oriented Logic Programming, Logical Methods in Computer Science, 11(3:3), (2015). IF2014 = 0.443 RIS2014 = 1.011
  12. R. Diaconescu: The Algebra of Opposition (and universal logic interpretations), in A. Koslow and A. Buchsbaum (eds.): The Road to Universal Logic, pages  127-143, Springer Basel (2015).
  13. R. Diaconescu: On the Existence of Translations of Structured Specifications, Information Processing Letters 115(1):15–22, Elsevier (2015). IF2013 = 0.479 RIS2013 = 1.060
  14. R. Diaconescu: From Universal Logic to Computer Science, and back, in G. Ciobanu and D. Mery (Eds.): ICTAC 2014, Lecture Notes in Computer Science 8687:1-16, Springer (2014).

    15. PHASE 3 (2013)

  15. R. Diaconescu, T. Mossakowski, A. Tarlecki: The institution theoretic scope of logic theorems, Logica Universalis 8(3-4), Springer (2014).
  16. R. Diaconescu: Graded consequence: an institution theoretic study, Soft Computing 18(7):1247--1267, Springer (2014). IF2013 = 1.304 RIS2013 = 0.850
  17. I. Țuțu: Comorphisms of structured institutions, Information Processing Letters 113:894–900, Elsevier (2013). IF2013 = 0.479 RIS2013 = 1.060
  18. I. Țuțu: Logical foundations of services, in A.V. Jones and N. Ng (Eds.): 2013 Imperial College Computing Student Workshop (ICCSW’13), OpenAccess Series in Informatics Dagstuhl 35:111--118, Dagstuhl Publishing (2013).
  19. I. Țuțu, J. L. Fiadeiro: A Logic-Programming Semantics of Services, in R. Heckel and S. Milius (Eds.): CALCO 2013, Lecture Notes in Computer Science 8089:299-313, Springer (2013).

    20. PHASE 2 (2012)

  20. R. Diaconescu, I. Țuțu: Foundations for structuring behavioural specifications, J. Logical and Algebraic Methods in Programming, 83(3-4):319-338, Elsevier (2014). IF2013 = 0.383 RIS2013 = 0.661
  21. R. Diaconescu, A. Madeira: Encoding hybridized institutions into first order logic, Mathematical Structures in Computer Science 26:745-788, Cambridge University Press (2016). IF2014 = 0.45 RIS2013 = 0.986
  22. I. Țuțu: Parameterisation for abstract structured specifications, Theoretical Computer Science 517:102–142, Elsevier (2014). IF2013 = 0.516 RIS2013 = 1.063
  23. R. Diaconescu: Institutional semantics for many-valued logics, Fuzzy Sets and Systems 218:32–52, Elsevier (2013). IF2013 = 1.880 RIS2013 = 1.268
  24. R. Diaconescu: An axiomatic approach to structuring specifications, Theoretical Computer Science 433:20–42, Elsevier (2012). IF2012 = 0.489 RIS2012 = 1.021

    25. PHASE 1 (2011)

  25. R. Diaconescu: Quasi-varieties and initial semantics for hybridized institutions, J. Logic and Computation  26(5):855-891, Oxford University Press (2016). IF2013 = 0.504 RIS2013 = 1.287

Note: The average publication cycle in journals of the research area of the project, from submission to actual publication, is between 1–5 years.

▲

Presentations in conferences (with participation funded by the project)

    PHASE 4 (2014)

  1. R. Diaconescu: Composition of specification modules: recent developments, presentation given at the 2014 Conferenceon Computational Intelligence and Software Engineering (CiSE 2014), Beijing, China, July 2014.

    2. PHASE 3 (2013)

  2. R. Diaconescu: The institution theoretic scope of logic theorems, presentation given at the 4th World Congress on Universal Logic, Rio de Janeiro, Brazil, April 2013.
  3. R. Diaconescu: Theory of Institutions, tutorial given at the 4th World School on Universal Logic, Rio de Janeiro, Brazil, March/April 2013.

    4. PHASE 2 (2012)

  4. R. Diaconescu: A module algebra for behavioural specifications, presentation given at the 21th Workshop on Algebraic Development Techniques, Salamanca, Spain, June 2012.
▲

Other dissemination activities/presentations of project's results

  1. I. Țuțu, J. Fiadeiro: Foundations of Graph Transformation as a Logic-Programming Language, 23rd International Workshop on Algebraic Development Techniques (WADT 2016), Nijmegen, Netherlands, June 2015.
  2. R. Diaconescu: Structuring of Specification Modules, invited talk at Workshop on Foundations of Informatics, Chișinău, Moldova, August 2015.
  3. I. Țuțu: Institution-independent Logic Programming, PhD thesis defense, Royal Holloway Univ. of London, England, July 2015.
  4. R. Diaconescu: Composition of specification modules: recent developments, Workhsop of the THALES project Algebraic modeling of topological and computational structures, Athens, Greece, July 2015.
  5. I. Țuțu, J. Fiadeiro: Revisiting the Institutional Approach to Herbrand's Theorem, 6th Conference on Algebra and Coalgebra in Computer Science, Nijmegen, Netherlands, June 2015.
  6. R. Diaconescu: From universal logic to computer science, and back, invited talk at 11th International Colloquium on Theoretical Aspects of Computing, Bucharest, Romania, September 2014.
  7. I. Țuțu: Solving Queries over Modular Logic Programs, 22nd International Workshop on Algebraic Development Techniques, Sinaia, Romania, September 2014.
  8. I. Vissani, C. G. Lopez Pombo, I. Țuțu, J. Fiadeiro: A Full Operational Semantics of Asynchronous Relational Networks, 22nd International Workshop on Algebraic Development Techniques, Sinaia, Romania, September 2014.
  9. I. Țuțu: What is a logic-programming language?, 14th Computer Science Postgraduate Research Colloquium, Egham, United Kingdom, June 2014.
  10. R. Diaconescu: Institution theory and Applications, habilitation defense, IMAR, Romania, May 2014.
  11. I. Țuțu, J. Fiadeiro: An Institution-Independent Approach to Logic Programming, IFIP WG1.3 Meeting , Theddingworth near Leicester, January 2014.
  12. I. Țuțu: Logical foundations of services, 2013 Imperial College Computing Student Workshop, London, United Kingdom, September 2013.
  13. I. Țuțu: A logic-programming semantics of services, 5th Conference on Algebra and Coalgebra in Computer Science, Warsaw, Poland, September 2013.
  14. R. Diaconescu: Thoughts on graded consequence, Mondrian Workshop, Aveiro, Portugal, July 2013.
  15. I. Țuțu: From service-oriented computing to logic programming and back, Seminar on Logic in Computer Science, Faculty of Mathematics and Computer Science, University of Bucharest, April 2013.
  16. R. Diaconescu: Institution theory: internal logic, Logic Seminar, Institute of Mathematics of the Romanian Academy, March 2013.
  17. R. Diaconescu: Institution theory: introduction, Logic Seminar, Institute of Mathematics of the Romanian Academy, March 2013.
  18. I. Țuțu: On the instantiation of parameterized specifications, 21th International Workshop on Algebraic Development Techniques, Salamanca, Spain, June 2012.
  19. R. Diaconescu: Towards Automated Structural Induction: an institution-independent methodology, Third Romanian-Japanese Algebraic Specification Workshop, Sinaia, Romania, April 2012.
  20. I. Țuțu: Multiple Parameterized Specifications with Sharing, Third Romanian-Japanese Algebraic Specification Workshop, Sinaia, Romania, April 2012.
▲

Seminars and workshops organized on the theme of the project

  1. 22nd International Workshop on Algebraic Development Techniques, Sinaia, Romania, September 2014.
  2. Logic and Formal Specification (online regular project seminar).
  3. Third Romanian-Japanese Algebraic Specification Workshop, Sinaia, Romania, April 2012.
▲

Doctoral theses (emerged from the project)

  1. A. Madeira (international advisor R. Diaconescu): Foundations and Techniques for Software Reconfigurability – an institution-independent approach for specifying and reasoning about reconfigurable systems, MAP-i (joint doctoral programme in informatics of the universities Minho, Aveiro and Porto), Portugal, 2013. Winner of the IBM Scientific Award 2013.
  2. I. Țuțu: Institution-independent Logic Programming, Royal Holloway University of London, England 2015.
▲

Scientific Reports

  1. Scientific Report of the project for the period Oct.2011 - Oct.2016
  2. Scientific Report of the project for the period Dec. 2014 - Nov. 2015
  3. Scientific Report of the project for the period Nov. 2013 - Nov. 2014
  4. Scientific Report of the project for the period Oct. 2011 - Oct. 2013
▲