Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2015 | Buch

Exploring an Interface Model for CKA Kapitel lesen Erstes Kapitel lesen

Mathematics of Program Construction

12th International Conference, MPC 2015, Königswinter, Germany, June 29 – July 1, 2015. Proceedings

herausgegeben von: Ralf Hinze, Janis Voigtländer

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 12th International Conference on Mathematics of Program Construction, MPC 2015, held in Königswinter, Germany, in June/July 2015. The 15 revised full papers presented together with two invited talks were carefully reviewed and selected from 20 submissions. The papers are about mathematical methods and tools put to use in program construction. They range from algorithmics to support for program construction in programming languages and systems. Some typical areas are type systems, program analysis and transformation, programming-language semantics, security, and program logics.

Inhaltsverzeichnis

Frontmatter
Exploring an Interface Model for CKA
Abstract
Concurrent Kleene Algebras (CKAs) serve to describe general concurrent systems in a unified way at an abstract algebraic level. Recently, a graph-based model for CKA has been defined in which the incoming and outgoing edges of a graph define its input/output interface. The present paper provides a simplification and a significant extension of the original model to cover notions of states, predicates and assertions in the vein of algebraic treatments using modal semirings. Moreover, it uses the extension to set up a variant of the temporal logic \(\mathsf {CTL}^*\) for the interface model.
Bernhard Möller, Tony Hoare
On Rely-Guarantee Reasoning
Abstract
Many semantic models of rely-guarantee have been proposed in the literature. This paper proposes a new classification of the approaches into two groups based on their treatment of guarantee conditions. To allow a meaningful comparison, it constructs an abstract model for each group in a unified setting. The first model uses a weaker judgement and supports more general rules for atomic commands and disjunction. However, the stronger judgement of the second model permits the elegant separation of the rely from the guarantee due to Hayes et al. and allows refinement-style reasoning. The generalisation to models that use binary relations for postconditions is also investigated. An operational semantics is derived and both models are shown to be sound with respect to execution. All proofs have been checked with Isabelle/HOL and are available online.
Stephan van Staden
A Relation-Algebraic Approach to Multirelations and Predicate Transformers
Abstract
The correspondence between up-closed multirelations and isotone predicate transformers is well known. Less known is that multirelations have also been used for modelling topological contact, not only computations. We investigate how properties from these two lines of research translate to predicate transformers. To this end, we express the correspondence of multirelations and predicate transformers using relation algebras. It turns out to be similar to the correspondence between contact relations and closure operations. Many results generalise from up-closed to arbitrary multirelations.
Rudolf Berghammer, Walter Guttmann
Preference Decomposition and the Expressiveness of Preference Query Languages
Abstract
Preferences in the scope of relational databases allow modeling user wishes by queries with soft constraints. There are different frameworks for database preferences including commercially available systems. They slightly vary in semantics and expressiveness but have in common that preferences induce strict partial orders on a given data set. In the present paper we study the expressiveness of preference operators in the available implementations. Particularly, we search for decompositions of strict partial orders into fundamental preference constructs. We study which preference operators and operands are necessary to express any strict partial order. Finally, we present two decomposition algorithms and show their correctness.
Patrick Roocks
Hierarchy in Generic Programming Libraries
Abstract
Generic programming (GP) is a form of abstraction in programming languages that serves to reduce code duplication by exploiting the regular structure of algebraic datatypes. Several different approaches to GP in Haskell have surfaced, giving rise to the problem of code duplication across GP libraries. Given the original goals of GP, this is a rather unfortunate turn of events. Fortunately, we can convert between the different representations of each approach, which allows us to “borrow” generic functions from different approaches, avoiding the need to reimplement every generic function in every single GP library.
In previous work we have shown how existing GP libraries relate to each other. In this paper we go one step further and advocate “hierarchical GP”: through proper design of different GP approaches, each library can fit neatly in a hierarchy, greatly minimizing the amount of supporting infrastructure necessary for each approach, and allowing each library to be specific and concise, while eliminating code duplication overall. We introduce a new library for GP in Haskell intended to sit at the top of the “GP hierarchy”. This library contains a lot of structural information, and is not intended to be used directly. Instead, it is a good starting point for generating generic representations for other libraries. This approach is also suitable for being the only library with native compiler support; all other approaches can be obtained from this one by simple conversion of representations in plain Haskell code.
José Pedro Magalhães, Andres Löh
Polynomial Functors Constrained by Regular Expressions
Abstract
We show that every regular language, via some DFA which accepts it, gives rise to a homomorphism from the semiring of polynomial functors to the semiring of \(n \times n\) matrices over polynomial functors. Given some polynomial functor and a regular language, this homomorphism can be used to automatically derive a functor whose values have the same shape as those of the original functor, but whose sequences of leaf types correspond to strings in the language.
The primary interest of this result lies in the fact that certain regular languages correspond to previously studied derivative-like operations on polynomial functors, which have proven useful in program construction. For example, the regular language \(a^*ha^*\) yields the derivative of a polynomial functor, and \(b^*ha^*\) its dissection. Using our framework, we are able to unify and lend new perspective on this previous work. For example, it turns out that dissection of polynomial functors corresponds to taking divided differences of real or complex functions, and, guided by this parallel, we show how to generalize binary dissection to \(n\)-ary dissection.
Dan Piponi, Brent A. Yorgey
A Program Construction and Verification Tool for Separation Logic
Abstract
An algebraic approach to the design of program construction and verification tools is applied to separation logic. The control-flow level is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data domain is captured by concrete store-heap models. These are linked to the separation algebra by soundness proofs. Verification conditions and transformation or refinement laws are derived by equational reasoning within the predicate transformer quantale. This separation of concerns makes an implementation in the Isabelle/HOL proof assistant simple and highly automatic. The resulting tool is itself correct by construction; it is explained on three simple examples.
Brijesh Dongol, Victor B. F. Gomes, Georg Struth
Calculating Certified Compilers for Non-deterministic Languages
Abstract
Reasoning about programming languages with non-deterministic semantics entails many difficulties. For instance, to prove correctness of a compiler for such a language, one typically has to split the correctness property into a soundness and a completeness part, and then prove these two parts separately. In this paper, we present a set of proof rules to prove compiler correctness by a single proof in calculational style. The key observation that led to our proof rules is the fact that the soundness and completeness proof follow a similar pattern with only small differences. We condensed these differences into a single side condition for one of our proof rules. This side condition, however, is easily discharged automatically by a very simple form of proof search. We implemented this calculation framework in the Coq proof assistant. Apart from verifying a given compiler, our proof technique can also be used to formally derive – from the semantics of the source language – a compiler that is correct by construction. For such a derivation to succeed it is crucial that the underlying correctness argument proceeds as a single calculation, as opposed to separate calculations of the two directions of the correctness property. We demonstrate our technique by deriving a compiler for a simple language with interrupts.
Patrick Bahr
Notions of Bidirectional Computation and Entangled State Monads
Abstract
Bidirectional transformations (bx) support principled consistency maintenance between data sources. Each data source corresponds to one perspective on a composite system, manifested by operations to ‘get’ and ‘set’ a view of the whole from that particular perspective. Bx are important in a wide range of settings, including databases, interactive applications, and model-driven development. We show that bx are naturally modelled in terms of mutable state; in particular, the ‘set’ operations are stateful functions. This leads naturally to considering bx that exploit other computational effects too, such as I/O, nondeterminism, and failure, all largely ignored in the bx literature to date. We present a semantic foundation for symmetric bidirectional transformations with effects. We build on the mature theory of monadic encapsulation of effects in functional programming, develop the equational theory and important combinators for effectful bx, and provide a prototype implementation in Haskell along with several illustrative examples.
Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, Perdita Stevens
A Clear Picture of Lens Laws
Functional Pearl
Abstract
A lens is an optical device which refracts light. Properly adjusted, it can be used to project sharp images of objects onto a screen—a principle underlying photography as well as human vision. Striving for clarity, we shift our focus to lenses as abstractions for bidirectional programming. By means of standard mathematical terminology as well as intuitive properties of bidirectional programs, we observe different ways to characterize lenses and show exactly how their laws interact. Like proper adjustment of optical lenses is essential for taking clear pictures, proper organization of lens laws is essential for forming a clear picture of different lens classes. Incidentally, the process of understanding bidirectional lenses clearly is quite similar to the process of taking a good picture.
By showing that it is exactly the backward computation which defines lenses of a certain standard class, we provide an unusual perspective, as contemporary research tends to focus on the forward computation.
Sebastian Fischer, Zhenjiang Hu, Hugo Pacheco
Regular Varieties of Automata and Coequations
Abstract
In this paper we use a duality result between equations and coequations for automata, proved by Ballester-Bolinches, Cosme-Llópez, and Rutten to characterize nonempty classes of deterministic automata that are closed under products, subautomata, homomorphic images, and sums. One characterization is as classes of automata defined by regular equations and the second one is as classes of automata satisfying sets of coequations called varieties of languages. We show how our results are related to Birkhoff’s theorem for regular varieties.
J. Salamanca, A. Ballester-Bolinches, M. M. Bonsangue, E. Cosme-Llópez, J. J. M. M. Rutten
Column-Wise Extendible Vector Expressions and the Relational Computation of Sets of Sets
Abstract
We present a technique for the relational computation of sets of sets. It is based on specific vector expressions, which form the syntactical counterparts of B. Kehden’s vector predicates. Compared with the technique that directly solves a posed problem by the development of a vector expression of type \({2^X}\,\leftrightarrow \,{\mathbf{1}\!\!\!\mathbf{1}}\) from a formal logical problem description, we reduce the solution to the development of inclusions between vector expressions of type \({X}\,\leftrightarrow \,{\mathbf{1}\!\!\!\mathbf{1}}\). Frequently, this is a lot simpler. The transition from the inclusions to the desired vector expression of type \({2^X}\,\leftrightarrow \,{\mathbf{1}\!\!\!\mathbf{1}}\) is then immediately possible by means of a general result. We apply the technique to some examples from different areas and show how the solutions behave with regard to running time if implemented and evaluated by the Kiel RelView tool.
Rudolf Berghammer
Turing-Completeness Totally Free
Abstract
In this paper, I show that general recursive definitions can be represented in the free monad which supports the ‘effect’ of making a recursive call, without saying how these calls should be executed. Diverse semantics can be given within a total framework by suitable monad morphisms. The Bove-Capretta construction of the domain of a general recursive function can be presented datatype-generically as an instance of this technique. The paper is literate Agda, but its key ideas are more broadly transferable.
Conor McBride
Auto in Agda
Programming Proof Search Using Reflection
Abstract
As proofs in type theory become increasingly complex, there is a growing need to provide better proof automation. This paper shows how to implement a Prolog-style resolution procedure in the dependently typed programming language Agda. Connecting this resolution procedure to Agda’s reflection mechanism provides a first-class proof search tactic for first-order Agda terms. As a result, writing proof automation tactics need not be different from writing any other program.
Wen Kokke, Wouter Swierstra
Fusion for Free
Efficient Algebraic Effect Handlers
Abstract
Algebraic effect handlers are a recently popular approach for modelling side-effects that separates the syntax and semantics of effectful operations. The shape of syntax is captured by functors, and free monads over these functors denote syntax trees. The semantics is captured by algebras, and effect handlers pass these over the syntax trees to interpret them into a semantic domain.
This approach is inherently modular: different functors can be composed to make trees with richer structure. Such trees are interpreted by applying several handlers in sequence, each removing the syntactic constructs it recognizes. Unfortunately, the construction and traversal of intermediate trees is painfully inefficient and has hindered the adoption of the handler approach.
This paper explains how a sequence of handlers can be fused into one, so that multiple tree traversals can be reduced to a single one and no intermediate trees need to be allocated. At the heart of this optimization is keeping the notion of a free monad abstract, thus enabling a change of representation that opens up the possibility of fusion. We demonstrate how the ensuing code can be inlined at compile time to produce efficient handlers.
Nicolas Wu, Tom Schrijvers
Backmatter
Metadaten
Titel
Mathematics of Program Construction
herausgegeben von
Ralf Hinze
Janis Voigtländer
Copyright-Jahr
2015
Verlag
Springer International Publishing
Electronic ISBN
978-3-319-19797-5
Print ISBN
978-3-319-19796-8
DOI
https://doi.org/10.1007/978-3-319-19797-5

Premium Partner

    Bildnachweise