Unification of Types and Multi-Level Modeling

UNIFICATION OF TYPES AND MULTI-LEVEL MODELING

Workshop at King’s College London

13 March 2024, 10:15am-5pm

Waterloo Campus, Franklin-Wilkins Building 2.46

This workshop explores links between unification of types in logic and multi-level modeling in information systems.

In some formal systems, such as second-order logic and type theory, distinctions between types of entities are expressed syntactically (e.g. different kinds of expressions are used to speak of different types of entities). These theories have expressive limitations that can be overcome in first-order theories, which express the relevant distinctions without relying on syntax. This allows a unified description of all entities in the domain.  An important set of logical methods can be used to convert, under certain conditions, typed approaches into more unified type-free approaches, a conversion Quine called "unification of universes".

Multi-level modeling recognises that higher-order types are needed for most computer applications and investigates how to implement these types. One barrier is that the syntax of most databases and programming languages is effectively first-order, supporting just schema and data. A common implementation builds the higher-order type structure in the single data domain. This appears analogous to a "unification of universes". A prime aim of the workshop is to explore this analogy and to see what two relevant communities, logic and information systems, can learn from one another.

The workshop is supported by the AHRC Research Grant H/V015516/1 “Properties, Paradox, and Circularity. A New, Type-Free Account” awarded to Salvatore Florio (CoI) and Carlo Nicolai (PI), and by the ERC Advanced Grant “Construction in the Formal Sciences” (project number 101054836) awarded to Øystein Linnebo. 

REGISTRATION

Attendance is free but registration is required. If you would like to attend, please email both Salvatore Florio ([email protected]) and Carlo Nicolai ([email protected]) by 29 February. 

SCHEDULE 

Morning session

10:15-10:45 Salvatore Florio (Oslo) and Chris Partridge (BORO Solutions and University of Westminster), Introduction 

11-11:50 Salvatore Florio and Øystein Linnebo (Oslo), “Lifting the Veil of Type Distinctions”

12-12:50 Carlo Nicolai (King’s College London), “Modelling Types and Sets within Circular Properties”

Afternoon session 

14-14:50 Chris Partridge, “Why Form, and so Unification of Types, Is Important?”

15:10-16 Al Cook (Critical Insight), “Formal Structures Meet a Data Engineer - My Experiences”

16:10-17 Sergio de Cesare (University of Westminster), “Implementing a Unification of Types in a Low-Code Environment”