Tetrapod-2018.md

layout: page
title: Modular Knowledge

Workshop on Modular Knowledge (Tetrapod)
Oxford, July 13, 2018
at the Federated Logic Conference 2018
affiliated with the Third International Conference on Formal Structures for Computation and Deduction

Description

Mathematics, logics, and computer science support a rich ecosystem of formal knowledge. This involves many interrelated human activities such as modeling phenomena and formulating conjectures, proofs, and computations, and organizing, interconnecting, visualizing, and applying this knowledge. To handle the ever increasing body of knowledge, practitioners employ a rapidly expanding set of representation languages and computer-based tools centered around the four fundamental paradigms of formal deduction, computation, datasets, and informal narration.

Modularity has been recognized in all FLoC-related communities as a critical method for designing scalable representation languages and building large corpora of knowledge. It is also extremely valuable for comparing and exchanging knowledge across communities, corpora, and tools - a challenge that is both pressing and difficult.

Expanding on the Tetrapod workshop at the conference on intelligent computer mathematics (CICM) 2016, this workshop brings together researchers from a diverse set of research areas in order to create a universal understanding of the challenges and solutions regarding highly structured knowledge bases.

Of particular interest are

• foundational principles such as theory graphs and colimits
• interchange languages and module systems
• languages and tools for representing, reasoning, computing, managing, and documenting modular knowledge bases

Organizers

• Jacques Carette, McMaster University (carette@mcmaster.ca)
• Dennis Müller, FAU Erlangen-Nürnberg (d.mueller@kwarc.info)
• Florian Rabe, Jacobs University Bremen (f.rabe@jacobs-university.de)

Location

Federated Logic Conference 2018, Oxford, July 13.

Format

• There will be 8 invited speakers, each of which will be asked to present a specific topic.
• Each speaker will give a 15-minute presentation on that topic that is followed by a 30-minute discussion session.
• There will not be a call for papers or other contributions. However, there will be a call for participation that will include the invited speakers and their topics.

Invited speakers and topics

Speaker	Modularity in...
Catherine Dubois	Proof Checking
Georges Gonthier	Large Proofs
Till Mossakowski	Ontologies
Natarajan Shankar	Proof Assistants
Doug Smith	Software Synthesis
Nicolas M. Thiery	Mathematical Computation

Procedures for selecting papers

The organizers will select invited speakers and topics. No selection of submissions is needed.

Dissemination

A report will be written after the workshop that includes abstracts of the invited talks and the highlights of the discussions during the workshop.