Functional and Logic Programming

Name: Functional and Logic Programming | 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings

John P. Gallagher Martin Sulzmann(Editor)

Springer (Publisher)

Published on 1. May 2018

XVI, 281 pages

E-Book

PDF with digital watermarking

System requirements

978-3-319-90686-7 (ISBN)

€53.49incl. 7% vat

System requirements

for PDF with digital watermarking

E-Book Single Licence

Available for download

Description

More details

Other editions

Content

Intro
Preface
Organization
Abstracts of Invited Talks
Can Programming Be Liberated from Unidirectional Style?
miniKanren: A Family of Languages for Relational Programming
Building Verified Cryptographic Components Using F*
Contents
Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name
1 Introduction
2 -Calculus and Call-by-Name Evaluation
3 Ariola and Felleisen's Call-by-Need -Calculus
4 Outline of Our Standardization-Based Proof
5 Formalization in Coq
6 Related Work
7 Conclusion
References
Direct Encodings of NP-Complete Problems into Horn Sequents of Multiplicative Linear Logic
1 Introduction
2 Intuitionistic Multiplicative Linear Logic, Horn Sequents, and MLL
2.1 Intuitionistic Multiplicative Linear Logic and Horn Sequents
2.2 Multiplicative Linear Logic
2.3 MLL Proof Nets
3 The Encoding of 3D MATCHING
3.1 Preliminaries
3.2 The Encoding into a Horn Sequent
3.3 The Correctness Proof
4 The Encoding of PARTITION
4.1 Preliminaries
4.2 The Encoding into a Horn Sequent
4.3 The Correctness Proof
5 Concluding Remarks
References
to SKI, Semantically
1 Introduction
2 Lambda- and SKI-calculi and the Bracket Abstraction
3 Semantic Translation
3.1 Lazy Weakening
4 OCaml Implementation
4.1 The Eta-Optimization
5 Compiling Real Programs
6 Linear algorithm
7 Related Work
8 Conclusions
References
Program Extraction for Mutable Arrays
1 Introduction
2 Finite Types and Finite Functions in Coq
2.1 A Finite Type Library-fintype
2.2 A Finite Function Library-finfun
3 Representing Mutable Arrays in Coq
3.1 Program Extraction for the Array State Monad
3.2 Small Example: Swap Two Elements
4 Optimizations by an Improved Extraction Plugin
4.1 Destructing Large Records
4.2 -expansion on Case Analysis
5 Case Studies
5.1 The Union-find Data Structure
5.2 The Quicksort Algorithm
6 Related Work
7 Conclusion
References
Functional Pearl: Folding Polynomials of Polynomials
1 Introduction
2 Univariate and Multivariate Polynomials
2.1 Univariate Polynomial and Its Semantics
2.2 Bivariate Polynomials
2.3 Multivariate Polynomials
3 Operations on Polynomials
3.1 Rotation
3.2 Substitution
3.3 Expansion
4 Compiling Polynomials
5 Conclusions and Related Work
References
A Functional Perspective on Machine Learning via Programmable Induction and Abduction
1 A Principled Functional Language for Machine Learning
2 Deduction, Induction, Abduction
2.1 Proofs-as-Programs for Induction
2.2 Proofs-as-Programs for Abduction
3 Programming with Induction-Abduction
4 The Abductive Calculus
5 DecML, A Functional Language for Machine Learning
6 Related and Further Work
References
Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance Validation
1 Introduction
1.1 Example: Confluence of the Computational -Calculus
1.2 Critical Pair Checking Using the Tool PolySOL
2 Polymorphic Computation Rules
3 Type Inference for Polymorphic Computation Rules
4 Confluence of Polymorphic Computation Systems
5 Example: Confluence of the Call-by-Need -Calculus
6 Summary and Related Work
6.1 Summary
6.2 Related Work
References
Confluence Modulo Equivalence with Invariants in Constraint Handling Rules
1 Introduction
2 Preliminaries
2.1 Confluence Modulo Equivalence
2.2 Constraint Handling Rules
2.3 Confluence of CHR Programs
3 Compatibility of Equivalence Relations
4 Confluence Modulo Equivalence w.r.t. an Invariant
5 Discussion and Related Work
6 Conclusion and Future Work
References
On Probabilistic Term Rewriting
1 Introduction
2 Related Work
3 Probabilistic Abstract Reduction Systems
3.1 Notions of Probabilistic Termination
3.2 Probabilistic Ranking Functions
3.3 Relation to Formulation by Bournez and Garnier
4 Probabilistic Term Rewrite Systems
4.1 Interpretation Methods for Proving SAST
4.2 Barycentric Algebras
5 Conclusion
References
Equivalence Checking of Non-deterministic Operations
1 Motivation
2 Functional Logic Programming and Curry
3 Equivalent Operations
4 Refined Equivalence Criteria
5 Property-Based Checking
6 Related Work
7 Conclusions
References
Optimizing Declarative Parallel Distributed Graph Processing by Using Constraint Solvers
1 Introduction
2 Fregel: Functional VcGP Language
2.1 Pregel
2.2 Fregel
3 Optimizing Fregel Programs
3.1 Reducing Communication
3.2 Inactivating Vertices
3.3 Removing Barriers
3.4 Prioritized Execution
3.5 Limitation and Generalization
4 Implementation and Evaluation
4.1 Implementation
4.2 Setup of Experiments
4.3 Results
5 Related Work
6 Conclusion and Future Work
References
Breaking Symmetries with Lex Implications
1 Introduction
2 Preliminaries
3 Removing Redundant Constraints
4 Generating Compact and Complete Symmetry Breaks for Graphs
5 An Application: Computing Ramsey Colorings (4,4
n)
6 Conclusion
References
Model Checking Parameterized by the Semantics in Maude
1 Introduction
2 Preliminaries
2.1 Implementing Semantics in Maude
2.2 Shared-Memory Semantics
2.3 Message-Passing Semantics
2.4 Maude Metalevel and Loop Mode
3 Model Checking Shared-Memory Languages
4 Model Checking Message-Passing Languages
5 Concluding Remarks and Ongoing Work
References
Automated Amortised Resource Analysis for Term Rewrite Systems
1 Introduction
2 Preliminaries
3 Resource Annotations
4 Implementation
5 Experimental Evaluation
6 Conclusion
References
A Common Framework Using Expected Types for Several Type Debugging Approaches
1 Introduction
2 Language and Principal Typing Tree (PTT)
3 Expected Typings and Type Debugging Information Tree
3.1 How to Obtain Expected Types
3.2 Inferring Expected Typings
3.3 Type Annotations/Signatures
3.4 Why Obtain Expected Typings from Principal Typings?
3.5 Expected Typings in the Presence of Multiple Type Errors
4 Using the Type Debugging Information Tree
4.1 Enumeration of Type Error Messages
4.2 Type Error Slicing
4.3 Improved Interactive Type Error Debugging
5 Evaluation
6 Related Work
7 Conclusion
References
CauDEr: A Causal-Consistent Reversible Debugger for Erlang
1 Introduction
2 The Language
3 Causal-Consistent Reversible Debugging
4 CauDEr: A Causal-Consistent Reversible Debugger
4.1 The CauDEr Workflow
4.2 Finding Concurrency Bugs with CauDEr
5 Related Work
6 Discussion
References
Cheap Remarks About Concurrent Programs
1 Introduction
2 Key Concerns of Observing Concurrent Programs
3 An Illustrative Example
4 How CoCo Works
4.1 Representing and Generating Expression Schemas
4.2 Evaluating Most General Terms
4.3 Property Discovery and Schema Pruning
5 Case Studies
5.1 Concurrent Stacks
5.2 Semaphores
6 Related Work
7 Conclusions and Evaluation
References
Author Index

System requirements

Save as PDF Copy link into clipboard

Schweitzer Fachinformationen

Functional and Logic Programming

Description

More details

Other editions

Additional editions

Content

System requirements