View: session overviewtalk overviewside by side with other conferences

09:00-10:30 Session 83L
Location: Maths L6
Modularity in Software Synthesis

ABSTRACT. 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

ABSTRACT. Modularity in Mathematical Computation

10:30-11:00Coffee Break
11:00-12:30 Session 86M
Location: Maths L6
Modularity in Proof Assistants

ABSTRACT. Modularity in Proof Assistants

Discussion 1

ABSTRACT. Discussions on the previous talks.

12:30-14:00Lunch Break
14:00-15:30 Session 87M
Location: Maths L6
Modularity in Proof Checking

ABSTRACT. Modularity in Proof Checking

Modularity in Large Proofs

ABSTRACT. Modularity in Large Proofs

15:30-16:00Coffee Break
16:00-16:45 Session 88J
Location: Maths L6
Discussion 2

ABSTRACT. Discussions on the previous talks

19:00-21:30 Workshops dinner at Keble College

Workshops dinner at Keble College. Drinks reception from 7pm, to be seated by 7:30 (pre-booking via FLoC registration system required; guests welcome).

Location: Keble College