Functional and Logic Programming
11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012, Proceedings
Published on 20. May 2012
X, 333 pages
978-3-642-29822-6 (ISBN)
Description
This book constitutes the refereed proceedings of the 11th International Symposium on Functional and Logic Programming, FLOPS 2012, held in Kobe, Japan, in May 2012.
The 19 research papers and 3 system demonstrations presented in this volume were carefully reviewed and selected from 39 submissions. They deal with declarative programming, including functional programming and logic programming.
More details
Other editions
Additional editions
Tom Schrijvers | Peter Thiemann
Functional and Logic Programming
11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012, Proceedings
Book
05/2012
1st Edition
Springer
€53.49
Shipment within 7-9 days
Content
- 7294
- Preface
- Organization
- Table of Contents
- Programming with Boolean Satisfaction
- Automated Verification of Higher-Order Functional Programs
- Dependently-Typed Programming in GHC
- Call-by-Value Solvability, Revisited
- Introduction
- The Value-Substitution Calculus
- Relation with Herbelin's and Zimmerman's ? CBV
- Confluence
- Call-by-Value Solvability
- Terms Having Stratified-weak Normal Form Are Solvable
- Solvable Terms Have Stratified-weak Normal Form
- Behavioural Equivalence and Solvability for CBV
- Conclusions and Future Work
- References
- Compiling a Functional Logic Language: The Basic Scheme
- Introduction
- The Basic Scheme
- Symbols and Expressions
- Definitional Trees
- Programs
- Computations
- Strategy
- Compilation
- Optimization
- Pull-Tabbing
- An Example
- Correctness
- Implementation
- Representation and Replacement
- Extensions
- Limitations
- Performance
- Related Work and Concluding Remarks
- References
- Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts
- Introduction
- Call-by-Need Sequent Calculus (? lv)
- A Multicut Sequent Calculus (?[lvt])
- Environment-Based Abstract Machine (?[lvt* ])
- Environment-Based CPS (?[lvt* ])
- On Variables as Values
- Conclusion
- References
- Normal Form Bisimulations for Delimited-Control Operators
- Introduction
- The Calculus S
- Syntax
- Reduction Semantics
- Contextual Equivalence
- Normal Form Bisimilarity
- Definition
- Soundness and Completeness
- Refined Bisimilarity and Up-to Techniques
- Refined Bisimilarity
- Up-to Techniques
- Examples
- Conclusion
- References
- Real-Time Persistent Queues and Deques with Logic Variables (Declarative Pearl)
- Introduction
- Real-Time Queues
- Real-Time Persistent Deques
- Discussion
- References
- Declarative Debugging of Wrong and Missing Answers for SQL Views
- Introduction
- Preliminaries
- Debugging Algorithm
- Implementation
- Conclusions
- References
- Improving the Performance of FD Constraint Solving in a CFLP System
- Introduction
- TOY(FD)
- Architecture
- Interfacing External C++ Solvers
- Communication
- Representation
- Backtracking
- Search Strategies
- Incremental and Batch Propagation
- Implementing TOY(FDg) and TOY(FDi)
- Integration of Gecode 3.7.0: TOY(FDg)
- Integration of IBM ILOG 6.8: TOY(FDi)
- Performance
- Related Work
- Conclusions and Future Work
- References
- A General Implementation Framework for Tabled CLP
- Introduction
- Tabling Background
- Tabled Evaluation
- Global Table
- Tabling Program Transformation
- Interaction between Tabling and CLP
- A General Framework for TCLP
- Constraint Global Table
- TCLP Program Transformation
- Consumer Suspension/Resumption
- Improvements to Constraint Domain Operations
- Sample Implementations
- Equality and Disequality Constraints
- Difference Constraints
- Experimental Performance Evaluation
- Ciao TCLP versus TCHR / XSB
- Timed Automata Applications
- Related Work
- Conclusions
- References
- Extending the T OY System with the ECLiPSe Solver over Sets of Integers
- Introduction
- The TOY Language
- Constraint Domains and Solvers
- The Constraint Domain FS (Finite Sets)
- Solver for FS Domain
- The Mediatorial Domain M
- Adapting the CCLNC(C) Calculus
- Implementation and Experiments
- Conclusions and Future Work
- References
- Correct Looping Arrows from Cyclic Terms
- Introduction
- Cyclic Terms
- Cyclic Data Structure
- Circuit
- Recursive Function
- Interpreting Cyclic Terms as Looping Arrows
- Variation of Arrows
- General Case
- Category-Theoretic Foundations
- Arrow Interpretation as Categorical Interpretation
- Semantics of Arrows: Freyd Categories
- Semantics of Cyclic Structures: Traced Monoidal Categories
- Key Idea: Traced Categorical Interpretation in Case of Looping Arrows
- Proof of Theorem 1
- Summary and Further Directions
- References
- A Lambda Calculus for Gö del-Dummett Logic Capturing Waitfreedom
- Introduction
- ? -GD
- Logic
- Term Assignment
- Reduction
- Properties
- Typed Waitfreedom
- Typed Input-Output Problem
- Typed Protocol
- Typed Waitfree Computation
- Characterization of Waitfreedom and ? -GD
- Related Work
- Future Work
- Conclusion
- References
- Iteratees
- Introduction
- Programming with Iteratees
- Enumerators and the Semantics of Iteratees
- Conclusions
- References
- Mutual Exclusion by Interpolation
- Introduction
- Motivation
- Applications in the Functional Setting
- Applications in the Logical Setting
- Theoretical Components
- Interpolation
- Farkas' Lemma
- The lrs-algorithm
- Inferring Interpolants for Mutual Exclusion
- Correctness
- Implementation and Experimental Results
- Related Work
- Future Work
- Conclusions
- References
- Parallel Computation Skeletons with Premature Termination Property
- Introduction
- Eden
- Skeletons with Premature Termination: The Beginning
- Map+Reduce
- Parallelisation Results
- Further Related Work
- Conclusions and Future Work
- References
- Calculational Developments of New Parallel Algorithms for Size-Constrained Maximum-Sum Segment Problems
- Introduction
- Preliminary
- BMF-Based Developments of Parallel MSS Algorithms
- Bird-Meertens Formalism
- BMF as a Parallel Programming Language
- One-Dimensional MSS
- Two-Dimensional MSS
- Sliding-Window Scan
- Deriving Parallel Algorithms for the Size-Constrained MSS
- One-Dimensional Size-Constrained MSS without Lower Bounds
- Two-Dimensional Size-Constrained MSS
- Concluding Remarks
- References
- A Data Flow Language for Hybrid Query and Programming Languages
- Introduction
- Trix
- Semantics
- Dataflow-Preserving Compilation
- Evaluation
- Conclusion
- References
- Coinductive Constraint Logic Programming
- Introduction
- Coinductive Logic Programming
- Coinductive Constraint Logic Programming
- Notation and Terminology
- Syntax
- Declarative Semantics
- Operational Semantics
- Soundness and Completeness of co-CLP
- Conclusions
- References
- A Call-by-Name CPS Hierarchy
- Introduction
- Preliminaries
- Delimited-Control Operators and a CPS Hierarchy
- The Thunk Translation
- The Calculi: Syntax and Reduction Rules
- Type System
- Type System for Call-by-Value CPS Hierarchy
- Refining the Type System
- Type System for Call-by-Name CPS Hierarchy
- Equational Theory
- Concluding Remarks
- References
- Exact Flow Analysis by Higher-Order Model Checking
- Introduction
- Review of Higher-Order Model Checking
- Source Language and CFA Problem
- Source Language S
- CFA Problem
- Reduction from CFA to HO Model Checking
- From CFA to CSA
- From CSA to HO Model Checking
- Complexity
- Extensions
- Booleans and Control Structures
- Infinite Data Domains
- Data Flow Analysis
- Experiments
- Related Work
- Conclusions
- References
- Computing in Cantor's Paradise with ?ZFC
- Introduction
- Language Tower and Terminology
- Metalanguage: First-Order Set Theory
- The Gateway to Cantor's Paradise: Infinity
- Every Set Can Be Sequenced: Well-Ordering
- Infinity's Infinity: An Inaccessible Cardinal
- ZFC's Grammar
- An Infinite Set Rule for Finite BNF Grammars
- The Grammar of Infinite, Encoded Terms
- ZFC's Big-Step Reduction Semantics
- Syntactic Sugar and a Small Set Library
- Example: The Reals from the Rationals
- Example: Computable Real Limits
- The Limit Monad
- The Computable Limit Monad
- Related Work
- Conclusions and Future Work
- References
- The Finite Domain Constraint Solver of SWI-Prolog
- Introduction
- Related Work
- Constraint Solving over Arbitrarily Large Integers
- Implementation
- Ensuring Terminating Propagation
- A Domain-Specific Language for Reification
- Extensions via Custom Propagators
- Performance Evaluation
- Conclusion and Future Work
- References
- Explicit Binds: Effortless Efficiency with and without Trees
- Introduction
- Lists
- True Lists
- Towards other Implementations of Lists
- Lists with Explicit (``Frozen'') Appends
- Church Lists
- Comparison
- From Fold to Primitive Recursion
- Leaf Trees (Free Monads)
- Leaf Trees
- Leaf Trees with Explicit Grafts
- Church Leaf Trees
- Monadic Inductive Datatypes from Parameterized Monads
- Other Generalizations
- Related Work
- Conclusion
- References
- Author Index
