Workshop on Logic, Algebra and Category Theory: LAC 2018

Melbourne, February 12–16, 2018

Co-organized by the Institute of Mathematics for Industry at Kyushu University and La Trobe University

Aims and scope

The workshop aims at bringing together researchers and practitioners with interests in logic, algebra, category theory and their applications in computing science.

Abstract

Modern specification languages are based on logic. For any such language there exists a specific logical system underlying the language's features and constructions. The logic-based approach has great advantages for formal software verification, since it guarantees precision and clarity in the process of software development. On the other hand, it resulted in a proliferation of logical systems in specification theory, each tailor-made for a particular language. Essentially the same arguments and results had to be used for each of these systems, just to fit a different language. To avoid such redundancies, a unifying framework is clearly needed. One could then prove logical results in an abstract way and then apply them to concrete specification languages. Such a framework would also contribute to a deeper understanding of the causality relations between logic properties which are often hindered by the unnecessary details of concrete logics.

Category theory suggests itself as a general supporting structure, since it focuses on relations between objects rather than the precise way the objects are built. On the other hand, universal algebra plays an important role in defining the semantics of algebraic specification languages. Therefore, there exists a strong connection between logic, category theory and algebraic structures, especially in the context of formal methods, where mathematically grounded techniques are developed for modeling and verifying complex systems in various fields of computing science.

Invited speakers

Tutorials

Distributed Ontology Language

given by Oliver Kutz

There is a diversity of ontology languages in use, among them OWL, RDF, OBO, Common Logic, and F-logic. Related languages such as UML class diagrams, entityrelationship diagrams and object role modelling provide bridges from ontology modelling to applications, e.g. in software engineering and databases. Also in model-driven engineering, there is a diversity of diagrams: UML consists of 15 different diagram types, and SysML provides further types. Finally, in software and hardware specifcation, a variety of formalisms are in use, like Z, VDM, first-order logic, temporal logic etc. Another diversity appears at the level of ontology, model and specification modularity and relations among ontologies, specifications and models. There is ontology matching and alignment, module extraction, interpolation, ontologies linked by bridges, interpretation and refinement, and combination of ontologies, models and specifications. The Distributed Ontology, Modeling and Specification Language (DOL) aims at providing a unified metalanguage for handling this diversity. In particular, DOL provides constructs for

  • "as-is" use of ontologies, models and specifications (OMS) formulated (as a logical theory) in a specific ontology, modelling or specification language,
  • OMS formalised in heterogeneous logics,
  • modular OMS,
  • mappings between OMS,
  • networks of OMS, and
  • queries.
The final DOL specification was submitted as a standard to the Object Management Group (OMG) in early 2015. This course will introduce syntax and semantics of the DOL language, discuss a number of modelling and interoperability problems that can be addressed with DOL, and introduce to the use of available DOL tools.

An Introduction to Coalgebraic Logic

given by Dirk Pattinson

The tutorial gives an overview of modal logic at the intersection of computer science, philosophy, logic, and artificial intelligence. The emphasis is on the broad spectrum of semantic and syntactic variation found in modal logics, and on unifying perspectives on this variety. The basic duality between algebra and coalgebra, and therfore coalgebraic logic, plays a key role. The course is targeted at graduate students, assuming basic familiarity with naive set theory and propositional logic.

We understand modal logics as extensions of propositional logic with additional operators. The course discusses a number of examples and focus on duality as bridge between the syntactic and the semantic viewpoint. We then present the basic decision problems in modal logic and discuss backwards proof search in sequent calculi. We then elaborate on the combination of modal logics, extensions of modal logics with nominals, the global modality, and fixpoints, and embed modal logic into the wider context of the philosophical, logical and computational landscape.

Institutions: an abstract framework for foundations of software specification and logic

given by Andrzej Tarlecki

One goal of this series of talks is to show some examples where the use of category theory, via the theory of institutions, led to beautiful, general and generic results, applicable in many different contexts, and to a better understanding of some standard classical results and ideas from the theory of specifications and from mathematical logic.

The concept of an institutions uses the language of category theory to offer a simple formalization of the notion of a logical system, where sentences and semantic structures are abstract objects linked by a satisfaction relation, classified by (abstract) signatures. The key idea is to endow the collection of signatures with a structure of a category, together with (covariant) translations of sentences and (contravariant) reducts of semantic structures induced by signature morphisms in a way that preserves satisfaction. Nearly all (if not quite all) logical systems fit such an institutional mould.

An ambitious research programme, going back to the original development of the notion of institution in the 1980s, is to mimic developments that classically concern or rely on a particular logical system within an arbitrary institution, perhaps subject to some further requirements. In this way, we arrive at general results that apply to many logical systems and capture a better understanding of the essence of many classical results and ideas.

In this series of talks I will present some bits and pieces of the theory of institutions, starting from the basics, and going on to sample ideas and results from institutional foundations of software specification and abstract model theory.

Programme

Tutorial sessions

Monday to Friday from 10:00 to 13:00

10:00–10:50
Andrzej Tarlecki, Institutions: an abstract framework for foundations of software specification and logic
11:00–11:50
Dirk Pattinson, An Introduction to Coalgebraic Logic
12:00–12:50
Oliver Kutz, Distributed Ontology Language
13:00–14:30
Lunch break

Presentations

Monday

14:00–14:40
Jennifer Seberry, Recent Thoughts on Computer Construction of Hadamard Matrices
14:50–15:30
Marcel Jackson, The algebraic method for Constraint Satisfaction Problems

Tuesday

14:30–15:20
Yde Venema, Dualities in algebraic logic
15:30–16:10
Hiroakira Ono, Cut elimination and semi-completeness

Wednesday

Please note the temporary change of venue. The presentations will be in the TLC (Teaching and Learning Commons) building, near the Agora, level 2, room 213.
Maps of the campus can be found here and here.

14:30–15:10
Richard Garner, Catalan families in categories
15:20–16:00
Yoshihiro Mizoguchi, Relational T-algebra and the category of topological spaces

Thursday

14:30–15:10
José Fiadeiro, An algebraic semantics and logic for Actor Networks
15:20–16:00
Ionuț Țuțu, A resolution-based approach to graph transformation

Friday

14:30–15:30
Maria Keet, Designing an appropriate logic for conceptual modeling languages
15:40–16:20
Adrián Riesco, Program analysis parameterized by the semantics in Maude
18:30
Social Dinner
at the Italian restaurant Mercadante
123 Lygon Street, Carlton (a map is available here, and also here)

Registration

There are three registration options:

  1. Ordinary registration: A$ 125.
  2. Registration for AustMS/AMSI members: A$ 100.
  3. Student registration: no registration fee.
  4. Retirees and unemployed: no registration fee.

To register for LAC 2018, please fill in the following form.

Venue

The workshop will be held at La Trobe’s Institute of Advanced Studies.
For Wednesday, 14th of February, there will be a temporary change of venue: the presentations will take place in the TLC (Teaching and Learning Commons) building, near the Agora, level 2, room 213.

Maps and details about the location can be found here.

If you use public transport, we recommend tram 86, or buses 250, 350. It is just a 5-minutes walk from tram stop 61 to the Institute, and about a 10-minutes walk from the main bus stop on campus. Timetables for trams and buses can be found here.

Accommodation

Accommodation options nearby include:

Organizers

  • Mihai Mihai Codescu
    Institute of Mathematics of the Romanian Academy
    Romania
  • Daniel Daniel Găină
    Institute of Mathematics for Industry
    Kyushu University
    Japan
  • Tomasz Tomasz Kowalski
    Department of Mathematics and Statistics
    La Trobe University
    Australia
  • Wenny Wenny Rahayu
    Head of School of Engineering and Mathematical Sciences
    La Trobe University
    Australia
  • Asha Asha Rao
    Department of Mathematical Sciences
    RMIT University
    Australia

Contact

If you have any questions or inquiries about LAC 2018 you can contact us via e-mail at lac2018 [at] imi.kyushu-u.ac.jp