From 9cbb9fa11efcd873b2eff9ba178adfdd11e98df8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dennis=20M=C3=BCller?= <d.mueller@jacobs-university.de> Date: Thu, 12 Jul 2018 23:52:55 +0200 Subject: [PATCH] abstracts --- events/Tetrapod-2018.md | 155 +++++++++++++++++++++++++++++++++++----- 1 file changed, 138 insertions(+), 17 deletions(-) diff --git a/events/Tetrapod-2018.md b/events/Tetrapod-2018.md index 90305c3..38f6739 100644 --- a/events/Tetrapod-2018.md +++ b/events/Tetrapod-2018.md @@ -46,26 +46,147 @@ Of particular interest are #### 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 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 +system. Larger grain modules can capture reusable higher-level design knowledge: algorithm +design theories, datatype specifications and refinements, formalized design patterns, and +architectural patterns. These are used with deductive/refinement techniques to generate ini- +tial designs from requirement-level specifications. Machine learning applications also exploit +larger-grain patterns, such as linear regression models and neural networks. These provide a +computation pattern (with parameters to-be-learned and chosen hyperparameters) that can +be instantiated using methods for fitting models to the given data. More ad-hoc forms of de- +sign knowledge include sketches, program templates, and schemata. These are used with (1) +deductive/refinement techniques to generate instantiations from logical specifications, or (2) +inductive generalization techniques that search a space of instances given concrete examples. + +3 - Derivations + +A software synthesis process that generates interesting software usually involves the compo- +sition of many kinds of design knowledge and so it is relevant to consider the structuring of +that composition, called a derivation. Derivations can be a sequence (or tree) of specifications +where each is derived from its predecessor by applying a module of design knowledge. Typ- +ically, the early knowledge applications in a derivation introduce the overall algorithmic or +architectural structure and then many more knowledge applications are applied to improve +performance and to fit the design to the target computational substrate. + +#### Modularity in Mathematical Computation +Over the last decades, a huge amount of computational software was +developed for pure mathematics, in particular to support research and +education. As for any complex ecosystem of software components, the +ability to compose them has a multiplier effect on the expressive +power, flexibility, and range of applications. + +The purpose of this session is to share experience on the many +barriers to composability in computational mathematics, and how they +are being tackled in various communities. Of particular interest will +be the exploitation of knowledge to leverage some of the barriers. +feedback from neighbor fields (proofs, data, knowledge) will be most +welcome. -- GitLab