Functional and Logic Programming

Name: Functional and Logic Programming | 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012, Proceedings
Brand: Springer
Price: 53.49 EUR
Availability: OnlineOnly

11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012, Proceedings

Tom Schrijvers Peter Thiemann(Herausgeber*in)

Springer (Verlag)

Erschienen am 20. Mai 2012

X, 333 Seiten

E-Book

PDF mit Wasserzeichen-DRM

Systemvoraussetzungen

978-3-642-29822-6 (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

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

Systemvoraussetzungen

Als PDF speichern Als Link merken