
Mathematics of Program Construction
Description
Alles über E-Books | Antworten auf Fragen rund um E-Books, Kopierschutz und Dateiformate finden Sie in unserem Info- & Hilfebereich.
This book constitutes the refereed proceedings of the 13th International Conference on Mathematics of Program Construction, MPC 2019, held in Porto, Portugal, in October 2019.
The 15 revised full papers presented together with an invited paper were carefully reviewed and selected from 22 submissions. The papers deal with mathematical principles and techniques for constructing computer programs. 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.
More details
Other editions
Additional editions

Content
- Intro
- Preface
- Organization
- Contents
- Experiments in Information Flow Analysis
- 1 Introduction
- 2 Review of Quantitative Information Flow
- 3 Experiment (I): When Is a Leak Not a (Useful) Leak?
- 4 Experiment (II): Comparing Designs
- 5 Experiment (III): Properties of the Modelling Language
- 6 Experiments with Kuifje
- 7 Related Work
- 8 Conclusions and Discussion
- References
- Handling Local State with Global State
- 1 Introduction
- 2 Background
- 2.1 Monads, Nondeterminism and State
- 2.2 Combining Effects
- 3 Motivation
- 3.1 Example: The n-Queens Problem
- 3.2 Transforming Between Local State and Global State
- 4 Non-determinism with Global State
- 4.1 The Global State Law
- 4.2 Chaining Using Non-deterministic Choice
- 4.3 State-Restoring Operations
- 5 Laws and Translation for Global State Monad
- 5.1 Programs and Contexts
- 5.2 Laws for Global State Semantics
- 5.3 An Implementation of the Semantic Domain
- 5.4 Contextual Equivalence
- 5.5 Simulating Local-State Semantics
- 5.6 Backtracking with a Global State Monad
- 6 Related Work
- 6.1 Prolog
- 6.2 Reasoning About Side Effects
- 7 Conclusions
- References
- Certification of Breadth-First Algorithms by Extraction
- 1 Introduction
- 2 Preliminaries
- 2.1 Certification by Extraction
- 2.2 Verification, Certification and the Trusted Computing Base
- 2.3 Extraction of Simple Interleaving with Existing Tools
- 2.4 Recursion on Measures
- 2.5 Back to Simple Interleaving
- 3 Traversal of Binary Trees
- 3.1 Binary Trees
- 3.2 Ordering Branches of Trees
- 3.3 Breadth-First Traversal, a Naive Approach
- 4 Breadth-First Traversal of a Forest
- 4.1 Equational Characterization of Breadth-First Traversal
- 4.2 Direct Implementation of Breadth-First Traversal
- 4.3 Properties of Breadth-First Traversal
- 4.4 Discussion
- 5 FIFO-Based Breadth-First Algorithms
- 5.1 Axiomatization of FIFOs
- 5.2 Breadth-First Traversal
- 5.3 Breadth-First Numbering
- 5.4 Breadth-First Reconstruction
- 6 Numbering by Levels
- 7 Efficient Functional FIFOs
- 7.1 FIFOs Based on Two Lists
- 7.2 FIFOs Based on Three Lazy Lists
- 7.3 Some Remarks About Practical Complexity
- 8 Final Remarks
- A Code Correspondence
- References
- Verified Self-Explaining Computation
- 1 Introduction
- 2 Overview
- 2.1 Imp Slicing by Example
- 2.2 A Galois Connection Approach to Program Slicing
- 3 Dynamic Program Slicing
- 3.1 Tracing Semantics
- 3.2 Forward Slicing
- 3.3 Backward Slicing
- 3.4 An Extended Example of Backward Slicing
- 4 Formalisation
- 4.1 Lattices and Galois Connections
- 4.2 Imp Syntax and Semantics
- 4.3 Program State
- 4.4 Slicing Functions
- 5 Related and Future Work
- 6 Summary
- References
- Self-certifying Railroad Diagrams
- 1 Introduction
- 2 Railroad Diagrams
- 3 Interlude: Regular Algebras and Regular Expressions
- 4 Finite Automata with e-Transitions
- 5 Interlude: The Regular Algebra of Diagrams
- 6 Construction of Finite Automata with -Transitions
- 7 Finite Automata Without e-Transitions
- 8 Related Work
- 9 Conclusion
- References
- How to Calculate with Nondeterministic Functions
- 1 Introduction
- 2 Nondeterminism and Refinement
- 3 An Axiomatic Basis
- 4 A Denotational Semantics
- 5 Summary
- References
- Setoid Type Theory-A Syntactic Translation
- 1 Introduction
- 1.1 Related Work
- 2 MLTTProp
- 3 From Model to Translation
- 3.1 Standard Model
- 3.2 Graph Model
- 4 The Setoid Model as a Translation
- 4.1 The Setoid Model
- 4.2 Specification of the Translation
- 4.3 Implementation of the Translation
- 4.4 Extensions
- 5 Setoid Type Theory
- 6 Conclusions and Further Work
- A Full Syntax of MLTTProp
- B Complete Implementation of the Setoid Translation
- B.1 Specification
- B.2 Implementation
- B.3 Extensions
- C Justification of the Rules of Setoid Type Theory
- References
- Cylindric Kleene Lattices for Program Construction
- 1 Introduction
- 2 L-Monoids and Kleene Lattices
- 3 Relation Kleene Lattices
- 4 Cylindric L-Monoids and Kleene Lattices
- 5 Relational Cylindrification
- 6 Generalised Cylindrification
- 7 Propositional Refinement Calculus
- 8 Variable Frames
- 9 Local Variable Blocks
- 10 Synchronous Cylindrification
- 11 Diagonals and Substitution
- 12 Assignments
- 13 Beyond Cylindrification: Liberation Algebras
- 14 Conclusion
- A Construction of Weak Kleene Lattices
- B Construction of Weak Liberation Kleene Lattices
- References
- A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning
- 1 Introduction
- 2 Build a Hierarchy of Algebraic Laws on Top of the Theory of Monads
- 2.1 Basic Layers: Theories of Functors and Monads
- 2.2 Extensions: Specific Monads as Combined Theories
- 3 More Monads from Our Hierarchy of Effects
- 3.1 The Exception Monad
- 3.2 The State Monad and Derived Structures
- 3.3 The State-Trace Monad
- 3.4 The Probability Monad
- 3.5 Other Monads in the Hierarchy of Effects
- 4 Monadic Equational Reasoning
- 4.1 Motivating Example: The Fast Product
- 4.2 Basics of Equational Reasoning with Packed Classes
- 4.3 Rewriting Under Function Abstractions
- 4.4 Mechanization of Existing Pencil-and-Paper Proofs
- 5 Properties Proved Using Syntax
- 5.1 The Commutativity of State and Nondeterminism
- 5.2 Equivalence Between Operational and Denotation Semantics
- 6 Models of Monads
- 6.1 Models of State Monads
- 6.2 A Model of the Probability Monad
- 7 Technical Aspects of Formalization in Coq
- 8 Related Work
- 9 Conclusions and Future Work
- A The Choice Monad
- B Generic Algebraic Laws
- C Summary of Monads and Their Algebraic Laws
- D Details About the Imperative Language from Sect.5.2
- References
- System F in Agda, for Fun and Profit
- 1 Introduction
- 1.1 For Fun and Profit
- 1.2 Contributions
- 1.3 Overview
- 2 Intrinsically Typed Syntax of System F
- 2.1 Kinds
- 2.2 Type Contexts
- 2.3 Type Variables
- 2.4 Types
- 2.5 Type Renaming
- 2.6 Type Substitution
- 2.7 Type Equality
- 2.8 Term Contexts
- 2.9 Term Variables
- 2.10 Terms
- 3 Algorithmic Rules
- 3.1 Normal Types
- 3.2 Type Normalisation Algorithm
- 3.3 Completeness of Type Normalisation
- 3.4 Soundness of Type Normalisation
- 3.5 Stability of Type Normalisation
- 3.6 Normality Preserving Type Substitution
- 3.7 Terms with Normal Types
- 4 Correspondence Between Declarative and Algorithmic Type Systems
- 4.1 Soundness of Typing
- 4.2 Completeness of Typing
- 4.3 Erasure
- 5 Operational Semantics
- 5.1 Renaming for Terms
- 5.2 Substitution
- 5.3 Reduction
- 5.4 Progress and Preservation
- 5.5 Erasure
- 6 Execution
- 6.1 Erasure
- 7 Examples
- 8 Scaling up from System F to Plutus Core
- 8.1 Higher Kinded Recursive Types
- 8.2 Integers, Bytestrings and Cryptographic Operations
- 8.3 Using Our Implementation for Testing
- References
- An Analysis of Repeated Graph Search
- 1 Introduction
- 2 Relation Algebra
- 3 Repeated Search and Delegates
- 3.1 Delegate Function
- 3.2 Assigning Delegates
- 3.3 Incremental Computation
- 3.4 Injective Choice
- 3.5 Summary and Discussion
- 4 Strongly Connected Components
- 5 Conclusion
- References
- Shallow Embedding of Type Theory is Morally Correct
- 1 Introduction
- 1.1 Technical Challenges of Deep Embeddings
- 1.2 Reflecting Definitional Equality
- 1.3 Contributions
- 1.4 Related Work
- 2 The Involved Theories
- 2.1 Agda
- 2.2 The External Metatheory
- 2.3 The Object Type Theory
- 3 The Standard Model and Shallow Embedding
- 3.1 The Standard Model
- 3.2 Shallow Embedding
- 3.3 An External View of the Standard Model
- 4 The Termification of a Model
- 5 The Injectivity Result
- 6 Wrapped Standard Model
- 7 Case Studies
- 7.1 Parametricity
- 7.2 Canonicity
- 7.3 Termification and Injectivity
- 8 Discussion
- 8.1 Range of Embeddable Object Theories
- 8.2 Recursors and Eliminators for the Embedded Syntax
- 8.3 Ergonomics
- 9 Conclusions
- A The injectivity displayed model
- References
- En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad
- 1 Introduction
- 2 Syntax of o
- 2.1 Types
- 2.2 Terms
- 2.3 Term Equivalences
- 3 Delay Monad
- 3.1 Finite Products and Coproducts
- 3.2 Partial Isomorphisms
- 4 Elgot Iteration
- 4.1 Trace
- 4.2 Dagger Trace
- 5 Soundness
- 6 Conclusions
- References
- Completeness and Incompleteness of Synchronous Kleene Algebra
- 1 Introduction
- 2 Preliminaries
- 3 Synchronous Kleene Algebra
- 3.1 A Language Model for SKA
- 4 Incompleteness of SKA
- 5 A New Axiomatisation
- 5.1 Partial Derivatives
- 5.2 Normal Form
- 6 A Fundamental Theorem for SF1
- 7 Completeness of SF1
- 8 Related Work
- 9 Conclusions and Further Work
- A Appendix
- References
- Unraveling Recursion: Compiling an IR with Recursion to System F
- 1 Introduction
- 2 Datatype Encodings
- 3 Syntax and Type System of System F and FIR
- 3.1 Recursive Types
- 3.2 Datatypes
- 3.3 Let
- 4 Compilation
- 4.1 Non-recursive Term and Type Bindings
- 4.2 Recursive Term Bindings
- 4.3 Non-recursive Datatype Bindings
- 4.4 Recursive Datatype Bindings
- 5 Compiler Implementation in Agda
- 6 Optimization
- 6.1 Dead Binding Elimination
- 6.2 Case-of-Known-Constructor
- 7 Why Not Support These Features Natively?
- 8 Related Work
- 8.1 Encoding Recursive Datatypes
- 8.2 Encoding Recursive Terms
- 8.3 Intermediate Representations
- 9 Conclusion
- References
- Coding with Asymmetric Numeral Systems
- 1 Introduction
- 2 Origami Programming
- 3 Arithmetic Coding
- 4 Correctness of Arithmetic Coding
- 5 From Fractions to Integers
- 6 Bounded Precision
- 7 Streaming
- 8 Conclusion
- References
- Author Index
System requirements
File format: PDF
Copy protection: Watermark-DRM (Digital Rights Management)
System requirements:
- Computer (Windows; MacOS X; Linux): Use the free software Adobe Reader, Adobe Digital Editions, or any other PDF viewer of your choice (see eBook Help).
- Tablet/Smartphone (Android; iOS): Install the free app Adobe Digital Editions or another reading app for eBooks, e.g., PocketBook (see eBook Help).
- E-reader: Bookeen, Kobo, Pocketbook, Sony, Tolino and many more (only limited: Kindle).
The file format PDF always displays a book page identically on any hardware. This makes PDF suitable for complex layouts such as those used in textbooks and reference books (images, tables, columns, footnotes). Unfortunately, on the small screens of e-readers or smartphones, PDFs are rather annoying, requiring too much scrolling.
This eBook uses Watermark-DRM, a „soft” copy protection. This means that there are no technical restrictions to prevent illegal distribution. However, there is a personalised watermark embedded in the eBook that can be used to identify the purchaser of the eBook in the event of misuse and to provide evidence for legal purposes.
For more information, see our eBook Help page.