K.U.Leuven
  Search for Staff Students Organisational chart Search matrix Keywords

Research topics in Analysis group


Implementation

The basic execution mechanism of logic languages is well understood. However, the state of the art in this field can still be pushed further, both at the level of performance (space and time) and at the level of the usefulness of the language.

Two alleys have been taken by our group, both sharing a common basic compiler of Prolog-like source language to abstract machine code:
  • The first has led to the development of ilProlog, a logic inference machine dedicated to inductive learning. This tool is crucial in the deployment of the spin-off PharmaDM as well as for the machine learning activities within the group. The current research topics in this area include dynamic (incremental) compilation, intelligent backtracking techniques for queries, tabling in ILP, and analysis techniques for boosting performance of ILP execution.
  • The other alley resulted in hProlog, which is meant to provide an alternative back-end for HAL, a new constraint logic programming language developed at the Melbourne and Monash universities. Work related to analysis (frameworks), optimisation, constraint solving techniques and memory management all fit in this picture.
  • The first versions of the K.U.Leuven Constraint Handling Rules system were developed in the context of hProlog. For more on this topic, see the Constraint Handling Rules section.
Program Transformation and Specialisation

To make program components reliable, reusable, and maintainable, they are often written in a very general manner. This is because a program is either designed to handle a very broad range of different inputs or composed in a straightforward way from a set of reliable components. However, such a general and straightforward coding style imposes a runtime performance penalty, which can be compensated for by program transformation.

  • One focus of our research is program specialisation for logic programs, an area known as partial deduction.
  • Another is in the area of embedded systems for multi-media applications that manipulate large multi-dimensional arrays. The Data Transfer and Storage Exploration method converts programs into a declarative form. Various transformations can then be applied to reduce memory size and power consumption and to increase performance.
Constraint Handling Rules

Constraint Handling Rules (CHR) is a multi-headed rule-based language conceived in the early nineties. CHR is a highly expressive language at the intersection of rewriting systems and constraint logic programming, that is well-suited for the implementation of constraint solvers and many other reasoning and rewriting tasks.

Our group has addressed a wide range of topics in the context of CHR:
  • The study of CHR implementation and compilation has led to a number of CHR systems:
    • The K.U.Leuven CHR system is a state-of-the-art and widely used CHR system bundled with many Prolog systems: SWI-Prolog, SICStus, Yap, Ciao Prolog and XSB (where CHR is integrated with tabulation).
    • The K.U.Leuven JCHR and CCHR systems bring CHR to the world of imperative programming: Java and C, respectively. These are the fastest CHR implementations available today.
    • The latest development is the CHRRP system for Prolog, which offers a new form of declarative control flow based on rule priorities.
  • We have proposed a number of language extensions for increasing the expressivity of CHR: aggregates, negation, entailment checking, ...
  • We have made a number of contributions to the optimized compilation of CHR, such as compile-time memory management, program transformations and indexing datastructures. An important factor in this work is the development of a program analysis framework for CHR based on abstract interpretation
  • Our study of the computational properties of CHR has led to a general result of optimality: all algorithms can be implemented in CHR with optimal time and space complexity. This proven theorem is illustrated by various elegant implementations of well-known algorithms.

Type Systems
Our current research is aimed at two goals:
  • The inference of type definitions and type signatures for untyped declarative languages such as Prolog.
  • Expressive extensions of the type system of the well-know functional language Haskell: we have contributed towards open type functions, which are implemented in the Glasgow Haskell compiler.
Memory Management

Modern programming languages take the burden of memory management out of the hands of programmers: explicit memory management is indeed error prone and tedious. That is why languages like Java do not provide pointers and consequently rely on garbage collection for recycling garbage, i.e., memory cells with data that are no longer useful for the computation.

Declarative languages even abandon destructive assignment and the resulting referential transparency makes reasoning and analysis of programs automatable because of the cleaner semantics. However, a straightforward implementation of this semantics leads to an often substantial increase in memory usage and garbage production.

There are essentially two ways to deal with this problem:
  • Invocation of a traditional garbage collector at run time whenever memory becomes scarce. Run time garbage collection remains an important and active field of research in all modern programming language implementations.
  • Compile-time analysis can find out at which program points particular memory cells contain useless data, and can be used to produce code that reuses those cells without invoking a global garbage collector. This can happen at a fine grained level and then the technique is known as compile-time garbage collection. Region-based memory management is a related analysis-based technique that works at a coarser and more global level.
  • Hybrid forms recently get more and more attention.

Termination Analysis

Among all the properties a correct program should have, termination for all inputs is a prominent one. Ideally it should be proven for every program. In practice few programs are formally proven to terminate. The use of a declarative language with a clean semantics makes it feasible that the compiler proves termination for a large fraction of programs.

 

K.U.Leuven - CWIS Copyright © Katholieke Universiteit Leuven | Comments on the content: dtaiwww team
Production: dtaiwww | Most recent update: January 23, 2006 | Disclaimer
URL: http://www.cs.kuleuven.be/~dtai/