News Archive

News Archive

February 2009

• The Computational Power and Complexity of Constraint Handling Rules, J. Sneyers, T. Schrijvers, B. Demoen. Published in TOPLAS, 31(2), February 2009.
• Constraint-based Test Generation for Pointer-based Data Structures, T. Schrijvers, F. Degrave, W. Vanhoof. [draft]

January 2009

• Type Invariants for Haskell, T. Schrijvers, L.-J. Guillemette, S. Monnier. Presented at PLPV 2009. [pdf,slides] [Details] [Hide details]

  Haskell's multi-parameter type classes, together with functional dependencies, allow the specification of complex type-level operations, and the recent introduction of open type families in GHC makes such type-level programming even more accessible and flexible. But type-level code is special in that its correctness is crucial to the safety of the program; so except in those cases simple enough for the type checker to see trivially that the code is correct (or harmless), type-level programs need to come with their specification and correctness proof. In this article, we propose an extension to Haskell that allows the specification of invariants for type classes and open type families, together with accompanying evidence that those invariants hold. To accommodate the open nature of type classes and type families, the evidence itself needs to be open and every subcase of the proof can be provided independently from the others.

December 2008

• Constraint Handling Rules: A tutorial for (Prolog) programmers, T. Schrijvers. Tutorial at ICLP 2008, December 9, 2008. [slides]
• Uniting the Prolog Community, T. Schrijvers, B. Demoen. Side event at ICLP 2008, December 11, 2008.
• Automatic Generation of Test Inputs for Mercury, F. Degrave, T. Schrijvers, W. Vanhoof. LOPSTR 2008 (post-)proceedings. [pdf]
• From Monomorphic to Polymorphic Well-Typings and Beyond, T. Schrijvers, M. Bruynooghe, J. Gallagher. LOPSTR 2008 (post-)proceedings. [pdf]
• Winners of the 15th Prolog Programming Contest: Tom Schrijvers, Peter Stuckey and Marco Gavanelli won this year's contest held at the occasion of ICLP 2008 in Udine, Italy.

October 2008

• An Efficient Term Representation for CHR Indexing, B. Sarna-Starosta, T. Schrijvers. Accepted at CICLOPS 2008. [draft]

September 2008

• Type Checking with Open Type Functions, T. Schrijvers, S. Peyton Jones, M. Chakravarty, M. Sulzmann. Presented at ICFP 2008. [pdf ,slides] [Details] [Hide details]

  We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entailment checking; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.

• Unified Type Checking for Type Classes and Type Families, T. Schrijvers, M. Sulzmann. Presented at the ICFP 2008 poster session. [abstract, poster design]
• Introduction to Constraint Programming and Constraint Handling Rules, T. Schrijvers. Colloqium talk at Departement d'informatique et de recherche operationnelle, Universite de Montreal. September 18.
• Type Checking with Open Type Functions, T. Schrijvers. Presentation at McGill University, Montreal. September 11.
• Towards Typed Prolog, T. Schrijvers, V. Santos Costa, J. Wielemaker, B. Demoen. Accepted as short paper (poster) to ICLP 2008. [draft] [Details] [Hide details]

  Prolog is traditionally not statically typed. Since the benefits of static typing are huge, it was decided to grow a portable type system inside two widely used open source Prolog systems: SWI-Prolog and Yap. This requires close cooperation and agreement between the two systems. The type system is Hindley-Milner. The main characteristics of the introduction of types in SWI and Yap are that typing is not mandatory, that typed and untyped code can be mixed, and that the type checker can insert dynamic type checks at the boundaries between typed and untyped code. The basic decisions and the current status of the Typed Prolog project are described, as well as the remaining tasks and problems to be solved.

• Confluence for Non-Full Functional Dependencies, T. Schrijvers, M. Sulzmann. Accepted for the TFP 2008 post-proceedings. [full paper]
• Breaking the Complexity Barrier of Pure Functional Programs with Impure Data Structures, P. Wuille, T. Schrijvers. Presented by P. Wuille at IFL 2008. [draft]

August 2008

• Transactions in Constraint Handling Rules, T. Schrijvers, M. Sulzmann. Accepted at ICLP 2008. [draft]
• Equational Reasoning for Prolog, T. Schrijvers, B. Demoen. Accepted as short paper (poster) to ICLP 2008. [draft] [Details] [Hide details]

  Equational Reasoning is a feature of Functional Programming much envied by Logic Programmers. We argue that logic programmers should not shy away from adopting equational reasoning because of perceived pitfalls, but rather embrace it to indulge in its many benefits. We propose and illustrate two approaches: a cumbersome indirection via Haskell and a more insightful approach directly in Prolog.

July 2008

• From Monomorphic to Polymorphic Well-Typings and Beyond, T. Schrijvers, J. Gallagher, M. Bruynooghe. Presented at LOPSTR 2008. [extended abstract,slides]
• Transformation-based Indexing Techniques for CHR, B. Sarna-Starosta, T. Schrijvers. Presented at CHR 2008. [paper,slides]

June 2008

• Invited talk at CSCLP 2008 on A Taste of Constraint Handling Rules Today, T. Schrijvers. [slides]
• CHR for Imperative Host Languages, P. Van Weert, P. Wuille, T. Schrijvers, B. Demoen. Accepted for publication in the LNAI special issue on Constraint Handling Rules.
• Guard Reasoning in the Refined Operational Semantics of CHR, J. Sneyers, T. Schrijvers, B. Demoen. Accepted for publication in the LNAI special issue on Constraint Handling Rules. [Details] [Hide details]

  Constraint Handling Rules (CHR) is a high-level programming language based on multi-headed guarded rules. The original high-level operational semantics of CHR is very nondeterministic. Recently, instantiations of the high-level operational semantics have been proposed and implemented, removing sources of nondeterminism and hence allowing better execution control. Rule guards may be redundant under a more instantiated semantics while being necessary in the general high-level semantics. Expert CHR programmers tend to remove such redundant guards. Although this tends to improve the performance, it also destroys the local logical reading of CHR rules: in order to understand the meaning of a rule, the entire program and the details of the instantiated operational semantics have to be taken into account. As a solution, we propose compiler optimizations that automatically detect and remove redundant guards.

• A Flexible Search Framework for CHR, L. De Koninck, T. Schrijvers, B. Demoen. Accepted for publication in the LNAI special issue on Constraint Handling Rules. [Details] [Hide details]

  This paper introduces a framework for the specification of search strategies in CHR with disjunction (CHR^V). We support the specification of common search strategies such as depth-first, breadth-first and best-first, as well as constrained optimization by means of branch & bound search. The framework is given as an extension of CHR with rule priorities (CHR^rp) in which each branch of the search tree is assigned a branch priority. This approach leads to a uniform solution to execution control in CHR. In particular, during labeling, the rule priorities of CHR^rp can be used to determine the variable order, whereas the branch priorities can be used to determine the value order.

• Proceedings of CHR 2008, T. Schrijvers, F. Raiser, T. Fruehwirth. [proceedings]

April 2008

• The Constraint Handling Rules language, April 22, 2008. IT University, Copenhagen, Denmark. [slides]
• Restoring Confluence for Functional Dependencies, T. Schrijvers, M. Sulzmann. Accepted at TFP 2008. [full paper,abstract, slides] [Details] [Hide details]

  Haskell-style functional dependencies allow the programmer to influence the type inference process by automatically deriving type improvement rules from class and instance declarations. Previous work demands that the dependency must fully cover all type parameters of a type class to guarantee confluence. Confluence is an important property to ensure that type inference is well-behaved. We restore confluence for non-full functional dependencies by giving a novel encoding of functional dependencies in terms of type families as supported by the Glasgow Haskell Compiler. We compare our method against another alternative constraint-propagation encoding due to Claus Reinke. Our work provides new insights in the connection between functional dependencies and type families, and in the relative trade-offs of rewriting based or constraint-propagation based type inference approaches.

March 2008

• Improving Prolog programs: Refactoring for Prolog, A. Serebrenik, T. Schrijvers, B. Demoen. Theory and Practice of Logic Programming, Vol. 8(2), March 2008. [arxiv,Cambridge University Press]

January 2008

• Type inference for GADTs via Herbrand constraint abduction, M. Sulzmann, T. Schrijvers, P. J. Stuckey. Now available as a technical report. [report]
• The Constraint Handling Rules language, January 18, 2008. Computer Laboratory Programming Research Group Seminar, Cambridge University. [abstract, slides]

December 2007

• TCHR: a framework for tabled CHR, T. Schrijvers, B. Demoen and D. S. Warren. Accepted for publication in TPLP, December 2007. [arxiv.org]

November 2007

• First Class Constraint Programming in Haskell, T. Schrijvers, P. Stuckey, P. Wadler. Work in progress presented at SingHaskell, November 28, 2007. [slides] [Details] [Hide details]

  We report on our Constraint Logic Programing framework for Haskell. The core concept of the framework is the search tree, which is explored by primitive search strategies. A primitive search strategy is defined by a queue datatype and can be extended by a search transformer. Moreover, multiple search transformers can be composed to obtain quite complex behavior. Note that our framework is generic in the underlying constraint solver, and in particular works for both backtracking and copying-based solvers.

• SingHaskell 2007: Singapore Haskell meeting at National University of Singapore, organized by Martin Sulzmann and Tom Schrijvers. [website]

September 2007

• Towards Open Type Functions for Haskell, T. Schrijvers, M. Sulzmann, S. Peyton Jones, and M. Chakravarty. Presented at IFL 2007. [slides] [slides with Haskell intro] [IFL paper] [GHC Documentation] [Examples] [pptx] [Details] [Hide details]

  We present a new extension of the Haskell type system: functional programming at the type-level, with type functions. Type functions interact in interesting ways with Haskell's two other type system features: type classes and GADTs. Moreover, we show how they can be used to substitute functional dependencies. The typechecker's job now requires full-blown equational reasoning rather than simple Herbrand term unification. With some reasonable conditions on the type functions we can show that typechecking is still decidable; our algorithm constructs a strongly normalizing TRS. As a side effect of rewriting we generate proof terms, which serve as coercions for System FC. The whole system has been implemented in GHC and will be available shortly.

• LNAI special issue on Recent Advances in Constraint Handling Rules, editors: T. Fruehwirth and T. Schrijvers. [Call for Papers]
• Winners of the 14th Prolog Programming Contest: Paolo Pilozzi, Pieter Wuille and Tom Schrijvers won this year's contest held at the occasion of ICLP 2007 in Porto, Portugal.
• Transformation-based Indexing Techniques for CHR, B. Sarna-Starosta, T. Schrijvers. [Details] [Hide details] [Web page]

  Multi-headed rules are essential for the expressiveness of CHR, but incur a considerable performance penalty. Current indexing techniques are often unable to address this problem. They are effective only when matchings have a particular form, or offer good run-time complexity rather than good absolute figures. In this paper we describe three advanced indexing techniques: (1) two program transformations that make other indexing techniques more effective, (2) an index for ground terms more efficient than hash tables, and (3) a post-processing program transformation that eliminates runtime overhead of (1) and (2). We compare these techniques with the current state of the art, and give measurements of their effectiveness in K.U.Leuven CHR and CHRd.

• CCHR: the fastest CHR implementation, in C, P. Wuille, T. Schrijvers, B. Demoen. Accepted as system paper at CHR 2007. [Details] [Hide details]

  CHR is usually compiled to high-level languages (like Prolog) that make it hard or impossible to express low-level optimizations. This is a pity, because it confines CHR to be a prototyping language only, with an unacceptable performance for production quality software. This paper presents CCHR, a CHR system embedded in the C programming language, that compiles to low-level C code which is highly suitable for fine-grained performance improvements. In this way CCHR program performance comes close to matching that of native C, and easily outperforms other CHR implementations.

• Aggregates for CHR, P. Van Weert, J. Sneyers, T. Schrijvers, B. Demoen. Poster accepted at ICLP 2007. Accepted at CHR 2007. [techreport] [Details] [Hide details]

  We extend the Constraint Handling Rules language with aggregates such as sum, count, findall, and min. The proposed extension features nested aggregate expressions over guarded conjunctions of constraints, a series of predefined aggregates, and application-tailored user-defined aggregates. We formally define the operational semantics of aggregates, and show how incremental aggregate computation facilitates efficient implementations. Case studies demonstrate that language support for aggregates significantly reduces program size, thus improving readability and maintainability considerably.

• Proving termination of CHR in Prolog: A transformational approach, P. Pilozzi, T. Schrijvers, D. De Schreye. Extended abstract accepted at WST 2007. [techreport]
• CHR^rp: Constraint Handling Rules with Rule Priorities, L. De Koninck, T. Schrijvers, B. Demoen. Accepted at PPDP 2007. [techreport]
• The Correspondence Between the Logical Algorithms Language and CHR, L. De Koninck, T. Schrijvers, and B. Demoen. Accepted at ICLP 2007. [techreport]