Mathematics of Program Construction

Name: Mathematics of Program Construction | 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings

Graham Hutton(Herausgeber*in)

Springer (Verlag)

Erschienen am 19. Oktober 2019

VIII, 467 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-030-33636-3 (ISBN)

53,49 €inkl. 7% MwSt.

Systemvoraussetzungen

für PDF mit Wasserzeichen-DRM

E-Book Einzellizenz

Als Download verfügbar

Beschreibung

Weitere Details

Weitere Ausgaben

Inhalt

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

Systemvoraussetzungen

Als PDF speichern Als Link merken