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 by July 10. (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)
### Abstracts
#### Modularity in Proof Checking (Catherine Dubois)
The essence of (automated) proof checking is to check proofs for
correctness. A proof checker takes a proposition and a presumed proof
and merely verifies the proof, checking it for correctness. It is
much simpler to verify a proof than finding it.
Proof checking can be done in a batch way or interactively, as part of
an interactive theorem prover. For example it is triggered in Coq by
the keyword that ends a proof script (e.g. Qed or Defined). Moving
proof checking outside of theorem provers is explored and implemented
for example within the Dedukti system. Proof checking may also include
some proof reconstruction.
We may wonder why we need proof checking. First publications in
mathematics or computer science may contain errors. Second automated
theorem provers as complex software are buggy and thus verifying their
answers and proofs is very important. Proof assistants are also complex
software and having some independent proof checkers - off the shelves -
may also help to reduce the trusted base instead of proving the code of
proof assistants (which is an impossible task). Proof checkers are simpler
software than interactive or automated proof tools. Their code can be
reasonably
checked by crossed-reviews for example.
Type theory reduces the problem of proof checking to the problem of
type-checking in a programming language. Thus a proof is a
lambda-term, it is a correct proof of a formula if its type is
exactly the formula to be proven, thanks to the proofs-as-programs
analogy. In our
presentation, we'll focus on that definition/dimension of proof
checking.
Modular systems in computer science are divided into components or
modules with
well-defined interfaces and dependencies as small as
possible. Modularity requires also mechanisms to
compose/compile/assemble the
components together to obtain an executable software.
There is no doubt that proof checkers are modular software according to
the previous
definition. Let us go further and apply the feature of components/modules to
proofs. We can distinguish internal modularity and external
modularity. Internal modularity provides mechanisms to structure large
proofs (e.g. modules, inheritance) while external modularity provides
mechanisms to interface proofs having different origins and build
'composite proofs'. I will illustrate external modularity with
Dedukti and a proof of Erathostenes sieves made of a Coq component and
a HOL component verified by the Dedukti proof checker.
#### Modularity for specification, ontologies, and model-driven engineering (Till Mossakowski) (CANCELED)
Within the fields of software specification, ontologies,
model-driven engineering, and others, different notions of modularity
have been studied. It turns out that a semantics of these
artefacts can be both given in terms of logical theories, as well
as in terms of model classes.
Our central hypothesis is that a good support for modularity
should one the hand support both the model-theoretic and
theory-based point of view. On the other hand, it should be
applicable to a wide variety of (logical) languages.
The Distributed Ontology, Modeling and Specification
Language (DOL), standardised by the OMG, aims at providing a
unified metalanguage for meeting these criteria.
#### What is a Module? (Natarajan Shankar)
A module is a functional subsystem with an interface through which it
interacts with other subsystems. A module could be a body of
knowledge or a theory (e.g., vector spaces), a biological subsystem
(e.g., the nervous system), an organizational unit (e.g., accounting),
a physical component (e.g., steering wheel), or a software component
(e.g., compiler). In computing, modules appear in specification
languages like Z and PVS; modeling languages like B, TLA+, and SAL;
and programming languages like Ada and ML. Module mechanisms serve
several different purposes: packaging and reuse of related
functionality, abstraction and encapsulation of state and internal
representations, separate compilation, and composition. We discuss
some of the principles underpinning the design of module systems and
accompanying composition and reasoning principles.
#### Modular Knowledge in Software Synthesis (Doug Smith)
Software synthesis tools support the translation of requirements into acceptable software de-
signs. The requirements may be expressed logically, with a deductive design process, or the
requirements may come in the form of datasets, with an inductive design process. This session
focuses on modularity in software synthesis, and in particular on modular knowledge about re-
quirements, software design, and the structure of the design process. We briefly outline some of
the key forms of modularization that arise in these aspects of software synthesis.
1 - Requirements
For applications where mathematical correctness is important, requirements and high-level
designs can be structured using formal logical specifications as finite presentations of theo-
ries, which are composed using specification morphisms and colimits. For machine learning
applications, the requirements come in form of structured data sets.
2 - Software Design Knowledge
Representations of software design knowledge allow developers to guide an automated synthe-
sis system so that it can effectively translate requirement-level specifications into acceptable
high-level designs. Transformations (replace specification or code patterns by other code
patterns) and inference rules that relate logical goals with program structure (e.g. deduc-
tive synthesis rules) provide some of the basic design knowledge modules for any synthesis
