Traditional imperative synchronous programming languages heavily rely on a strict separation between data memory and communication signals. Signals can be shared between computational units but cannot be overwritten within a synchronous reaction cycle. Memory can be destructively updated but cannot be shared between concurrent threads. This incoherence makes traditional imperative synchronous languages cumbersome for the programmer. The recent definition of sequentially constructive synchronous languages offers an improvement. It removes the separation between data memory and communication signals and unifies both through the notion of clock synchronized shared memory . However, it still depends on global causality analyses, which precludes black-box procedural abstraction. This complicates reuse and composition of software components. This article shows how black-box procedural abstraction can be accommodated inside the sequentially constructive model of computation. We present the Sequentially Constructive Procedural Language ( SCoPL ) and its semantic theory of policy-constructive synchronous processes. SCoPL supports black-box procedural abstractions using policy interfaces to ensure that procedure calls are memory-safe and wait-free and their scheduling is determinate and causal. At the same time, a policy interface constrains the level of freedom for the implementation and subsequent refactoring of a procedure. As a result, policies enable separate compilation and composition of procedures. We present our extensions abstractly as a formal semantics for SCoPL and motivate it concretely in the context of the open-source, embedded, real-time language Blech .

Machine learning based image classification algorithms, such as deep neural network approaches, will be increasingly employed in critical settings such as quality control in industry, where transparency and comprehensibility of decisions are crucial. Therefore, we aim to extend the defect detection task towards an interactive human-in-the-loop approach that allows us to integrate rich background knowledge and the inference of complex relationships going beyond traditional purely data-driven approaches. We propose an approach for an interactive support system for classifications in an industrial quality control setting that combines the advantages of both (explainable) knowledge-driven and data-driven machine learning methods, in particular inductive logic programming and convolutional neural networks, with human expertise and control. The resulting system can assist domain experts with decisions, provide transparent explanations for results, and integrate feedback from users; thus reducing workload for humans while both respecting their expertise and without removing their agency or accountability.

Traditional imperative synchronous programming languages heavily rely on a strict separation between data memory and communication signals. Signals can be shared between computational units but cannot be overwritten within a synchronous reaction cycle. Memory can be destructively updated but cannot be shared between concurrent threads. This incoherence makes traditional imperative synchronous languages cumbersome for the programmer. The recent definition of sequentially constructive synchronous languages offers an improvement. It removes the separation between data memory and communication signals and unifies both through the notion of clock synchronised shared memory. However, it still depends on global causality analyses which precludes procedural abstraction. This complicates reuse and composition of software components. This paper shows how procedural abstraction can be accommodated inside the sequentially constructive model of computation. We present the Sequentially Constructive Procedural Language (SCPL) and its semantic theory of policy-constructive synchronous processes. SCPL supports procedural abstractions using policy interfaces to ensure that procedure calls are memory safe, wait-free and their scheduling is determinate and causal. At the same time, a policy interface constrains the level of freedom for the implementation and subsequent refactoring of a procedure. As a result, policies enable separate compilation and composition of procedures. We present our extensions abstractly as a formal semantics for SCPL and motivate it concretely in the context of the open-source, embedded, real-time language Blech.

We aim to establish the multi-modal logic CK n as a baseline for a constructive correspondence theory of constructive modal logics. Just like many classical multi-modal logics may be studied as theories of the basic system K obtained by model-theoretic specialisation, we envisage constructive modal logics to be derived as proof-theoretic enrichments of CK n . The system CK n would then act as a core system for constructive contextual reasoning with controlled information flow. In this paper, as a first step towards this goal, we study CK n as a type theory and introduce its computational λ-calculus, λCK n . Extending previous work on CK n , we present a cut-free contextual sequent system in the spirit of Masini's two-dimensional generalisation of natural deduction and Brünnler's nested sequents and give a computational interpretation for CK n following the Curry-Howard Correspondence. The associated modal type theory λCK n permits an interpretation for both the modalities □ and ◊ of CK n as type operators with simple and independent constructors and destructors, which has been missing in the literature. It is shown that the calculus satisfies subject reduction, strong normalisation and confluence. Since normal forms can be characterised by way of a Gentzen-style typing system with sub-formula property, λCK n is suitable for proof search in CK n . At the same time, λCK n enjoys natural deduction style typing which is important for programming applications. In contrast to most existing modal type theories, which are obtained as theories of the constructive modal logic S4, CK n is not bound to a particular contextual interpretation. Thus, λCK n constitutes the core of a functional language which provides static type checking of information processing to support safe contextual navigation in relational structures like those treated by description logics. We review some existing work on modal type theories and discuss their relation to λCK n .