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

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

Call for Opinions

To improve the discussions, we invite all interested researchers (independent of whether they attend the workshop) to submit preformulated opinions, either on one of the 6 subtopics or on modularity in general.

Opinions include any valuable contribution to the discussion such as

• position statements
• strengths and weaknesses of existing solutions
• pointers to pertinent recent or ongoing work
• challenge and benchmark problems

Opinions should be brief enough that workshop participants can easily read all opinions at the beginning of each session. Typically, they will not be longer than a couple of paragraphs.

The organizers will curate the submitted opinions and publish them on the workshop website and in a post-workshop summary.

For the version circulated at the workshop, the organizers may (with the collaboration of the authors) summarize or merge individual opinions if that helps readability. The online version will list all opinions verbatim. Opinions will be listed together with the name(s) of the authors.

Opinions should be submitted at https://easychair.org/conferences/?conf=tetrapod18 (An easychair abstract without a pdf file is sufficient.)

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)