Abstract Interpretation for Declarative Languages

Project: Research

Project Details


  • Fixpoint Methods: This topic is concerned with a uniform
    treatment of fixpoint specification and solution which exploits the best
    aspects of ideas used in the current fragmentary views seen in
    imperative, logic and functional language groups.

  • Compilation and Optimisation: New issues in compilation and
    optimisation guided by abstract interpretation will be investigated:
    interaction and integration of the compiler and the static analyser,
    modularity of the analysis and new source-to-source program
    transformations, in particular, transformations yielding superlinear

  • Analysis of ``full'' Prolog and CLP: Frameworks providing a
    complete treatment of existing built-ins inside new abstract domains
    incorporating information about the search rule such as sure execution
    of cuts, determinacy of procedures, number of solutions, will be
    developed and implemented. They will be extended to practical CLP

  • Analysis of Functional Logic Programs: New analysis
    frameworks adequate to the specific operational semantics of functional
    logic programs will be developed.

  • Concurrency: This topic includes methods and tools generally
    applicable to the analysis of concurrent systems. Application of these
    methods and tools to cc(FD) will be deeply investigated.

Effective start/end date1/01/9531/12/98


  • abstract interpretation
  • declarative languages
  • fixpoint
  • logic programming
  • optimisation
  • constraint logic programming