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
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
- Jacques Carette, McMaster University (email@example.com)
- Dennis Müller, FAU Erlangen-Nürnberg (firstname.lastname@example.org)
- Florian Rabe, Jacobs University Bremen (email@example.com)
Federated Logic Conference 2018, Oxford, July 13.
- 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
|Catherine Dubois||Proof Checking|
|Georges Gonthier||Large Proofs|
|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.
A report will be written after the workshop that includes abstracts of the invited talks and the highlights of the discussions during the workshop.