Melbourne, February 12–16, 2018
Co-organized by the Institute of Mathematics for Industry at Kyushu University and La Trobe University
The workshop aims at bringing together researchers and practitioners with interests in logic, algebra, category theory and their applications in computing science.
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.
José Luiz Fiadeiro Royal Holloway University of London United Kingdom Abstract |
Richard Garner Macquarie University Australia Abstract |
Marcel Jackson La Trobe University Australia Abstract |
Maria Keet University of Cape Town South Africa Abstract |
Oliver Kutz University of Bozen-Bolzano Italy Abstract |
Yoshihiro Mizoguchi Kyushu University Japan Abstract |
Hiroakira Ono Japan Advanced Institute of Science and Technology Japan Abstract |
Dirk Pattinson The Australian National University Australia Abstract |
Adrián Riesco Rodríguez Complutense University of Madrid Spain Abstract |
Jennifer Seberry University of Wollongong Australia Abstract |
Andrzej Tarlecki University of Warsaw Poland Abstract |
Ionuț Țuțu Royal Holloway University of London United Kingdom Abstract |
Yde Venema University of Amsterdam Netherlands Abstract |
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
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.
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.
Monday to Friday from 10:00 to 13:00
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.
There are three registration options:
To register for LAC 2018, please fill in the following form.
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 options nearby include:
Mihai Codescu Institute of Mathematics of the Romanian Academy Romania |
Daniel Găină Institute of Mathematics for Industry Kyushu University Japan |
Tomasz Kowalski Department of Mathematics and Statistics La Trobe University Australia |
Wenny Rahayu Head of School of Engineering and Mathematical Sciences La Trobe University Australia |
Asha Rao Department of Mathematical Sciences RMIT University Australia |
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