the proceedings contain 18 papers. the special focus in this conference is on Applications of Declarative programming and Knowledge Management. the topics include: Facets of the PIE Environment for Proving, Interpolat...
ISBN:
(纸本)9783030467135
the proceedings contain 18 papers. the special focus in this conference is on Applications of Declarative programming and Knowledge Management. the topics include: Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order logic;KBSET – Knowledge-Based Support for Scholarly Editing and Text Processing with Declarative Markup and a Core Written in SWI-Prolog;structured Traversal of Search Trees in constraint-logic Object-Oriented programming;performance Analysis of Zippers;adding Data to Curry;free theorems Simply, via Dinaturality;Improving the Performance of the Paisley Pattern-Matching EDSL by Staged Combinatorial Compilation;ICurry;a Process Calculus for Formally Verifying Blockchain Consensus Protocols;modular Modeling and Optimized Scheduling of Building Energy Systems Based on Mixed Integer programming;finding Maximal Non-redundant Association Rules in Tennis Data;from Textual Information Sources to Linked Data in the Agatha Project;allen’s Interval Algebra Makes the Difference;exploring Properties of Icosoku by constraint Satisfaction Approach;the Regularization of Small Sub-constraint Satisfaction Problems;declarative programming for Microcontrollers - Datalog on Arduino.
the proceedings contain 11 papers. the topics discussed include: programming with multiple paradigms in Lua;constraint based strategies;termination of context-sensitive rewriting with built-in numbers and collection d...
ISBN:
(纸本)3642119980
the proceedings contain 11 papers. the topics discussed include: programming with multiple paradigms in Lua;constraint based strategies;termination of context-sensitive rewriting with built-in numbers and collection data structures;semantic labeling for proving termination of combinatory reduction systems;a taxonomy of some right-to-left string-matching algorithms;type checking and inference are equivalent in lambda calculi with existential types;fast and accurate strong termination analysis with an application to partial evaluation;new results on type systems for functionallogicprogramming;a simple region inference algorithm for a first-order functional language;and theoretical framework for the declarative debugging of functionallogic programs with lambda abstractions.
the constraintfunctionallogicprogramming system TOY has been using the SICStus Prolog finite domain (FD) constraint solver. In this work, we show how to integrate the ILOG CP FD constraint solving technology into t...
详细信息
ISBN:
(纸本)9783642119989
the constraintfunctionallogicprogramming system TOY has been using the SICStus Prolog finite domain (FD) constraint solver. In this work, we show how to integrate the ILOG CP FD constraint solving technology into this system, withthe aim of improving its application domain and performance. We describe our implementation emphasizing the synchronization between Herbrand computations in the Toy side and FD constraint solving in the ILOG CP side. Finally, performance results are reported and discussed.
Numerous computational and deductive frameworks use the notion of strategy to guide reduction and search space exploration, making the macro scale control of micro operations an explicit object of interest. In recent ...
详细信息
ISBN:
(纸本)9783642119989
Numerous computational and deductive frameworks use the notion of strategy to guide reduction and search space exploration, making the macro scale control of micro operations an explicit object of interest. In recent works, abstract strategies have been defined in extension but also intensionally. In this paper we complete these views with a new declarative approach based on constraints, which are used to model the different parts of a strategy. this procedure allows us to express elaborate strategies in a declarative and reusable way.
Type systems are widely used in programming languages as a powerful tool providing safety to programs, and forcing the programmers to write code in a clearer way. functionallogic languages have inherited Damas & ...
详细信息
ISBN:
(纸本)9783642119989
Type systems are widely used in programming languages as a powerful tool providing safety to programs, and forcing the programmers to write code in a clearer way. functionallogic languages have inherited Damas & Milner type system from their functional part due to its simplicity and popularity. In this paper we address a couple of aspects that can be subject of improvement. One is related to a problematic feature of functionallogic languages not taken under consideration by standard systems: it is known that the use of opaque HO patterns in left-hand sides of program rules may produce undesirable effects from the point of view of types. We re-examine the problem, and propose a Damas & Milner-like type system where certain uses of HO patterns (even opaque) are permitted while preserving type safety, as proved by a subject reduction result that uses HO-let-rewriting, a recently proposed reduction mechanism for HO functionallogic programs. the other aspect is the different ways in which polymorphism of local definitions can be handled. At the same time that we formalize the type system, we have made the effort of technically clarifying the overall process of type inference in a whole program.
In this paper, we extend the well-known Naish's declarative debugging scheme for diagnosing wrong computed answers in first-order lazy functional-logic programs to the higher-order setting of the simply typed A-ca...
详细信息
ISBN:
(纸本)9783642119989
In this paper, we extend the well-known Naish's declarative debugging scheme for diagnosing wrong computed answers in first-order lazy functional-logic programs to the higher-order setting of the simply typed A-calculus, where programs are presented by conditional pattern rewrite systems. Our approach generalizes and combines declarative debugging techniques previously developed for less expressive declarative programming paradigms involving applicative rewrite rules instead of A-abstractions and decidable higher-order unification. Debugging starts withthe observation of a wrong computed answer which the user regards as incorrect w.r.t. an intended model that provides a declarative description of the program's semantics. Debugging proceeds by exploring an abridged proof tree built on a higher-order rewriting logic with A-abstractions that provides a purely declarative view of the computation. Finally, debugging ends withthe detection of a defined function rule in the program that is incorrect w.r.t. the intended model. We prove the logical correctness of the debugging method for any sound goal solving system whose computed answers are logical consequences of the program.
the proceedings contain 37 papers. the topics discussed include: functional interpretations of intuitionistic linear logic;fixed-point definability and polynomial time;Kleene's amazing second recursion theorem;jum...
ISBN:
(纸本)3642040268
the proceedings contain 37 papers. the topics discussed include: functional interpretations of intuitionistic linear logic;fixed-point definability and polynomial time;Kleene's amazing second recursion theorem;jumping boxes: representing Lambda-calculus boxes by jumps;tree-width for first order formulae;algorithmic analysis of array-accessing programs;decidable relationships between consistency notions for constraint satisfaction problems;cardinality quantifiers in MLO over trees;from coinductive proofs to exact real arithmetic;on the relation between sized-types based termination and semantic labelling;expanding the realm of systematic proof theory;intersection, universally quantified, and reference types;linear game automata: decidable hierarchy problems for stripped-down alternating tree automata;enriching an effect calculus with linear types;degrees of undecidability in term rewriting;upper bounds on stream I/O using semantic interpretations;and efficient type-checking for amortised heap-space analysis.
暂无评论