Logic Based Program Synthesis and Transformation: 13th International Symposium LOPSTR 2003, Uppsala, Sweden, August 25-27, 2003, Revised Selected Papers (Lecture Notes in Computer Science, 3018)

Table of Contents
Invited Talk
	Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce
Specification and Synthesis
	Predicate Synthesis from Inductive Proof Attempt of Faulty Conjectures
	Correct OO Systems in Computational Logic
	Specification and Synthesis of Hybrid Automata for Physics-Based Animation
	Adding Concrete Syntax to a Prolog-Based Program Synthesis System (Extended Abstract)
Verification
	Formal Development and Verification of Approximation Algorithms Using Auxiliary Variables
	Formal Reasoning about Efficient Data Structures A Case Study in ACL2
Analysis
	A Program Transformation for Backwards Analysis of Logic Programs
	An Efficient Staging Algorithm for Binding-Time Analysis
	Proving Termination with Adornments
Transformation and Specialisation
	Constructively Characterizing Fold and Unfold
	Deterministic Higher­Order Patterns for Program Transformation
	From Interpreter to Logic Engine by Defunctionalization
	Linearization by Program Transformation
	Continuation Semantics as Horn Clauses
Constraints
	Simplification of Database Integrity Constraints Revisited: A Transformational Approach
	Integration and Optimization of Rule-Based Constraint Solvers
	Introducing ESRA, a Relational Language for Modelling Combinatorial Problems
Author Index