We present a type inference system for Horn clause logic programs, based on a bottom-up abstract interpretation technique. Through the definition of suitable abstract operators, we obtain an abstract immediate consequence operator map associated with the program to analyze. The least fixpoint of such an operator gives an approximated description, by means of types, of the success set of the program. By changing the abstract domain of types, we easily obtain different type inference systems. This is useful to make the inference appropriate for different purposes. Due to the semantic basis, the system declaratively handles type union and parametric polymorphism.

A Bottom-Up Polymorphic Type Inference in Logic Programming

GIACOBAZZI, Roberto
1992

Abstract

We present a type inference system for Horn clause logic programs, based on a bottom-up abstract interpretation technique. Through the definition of suitable abstract operators, we obtain an abstract immediate consequence operator map associated with the program to analyze. The least fixpoint of such an operator gives an approximated description, by means of types, of the success set of the program. By changing the abstract domain of types, we easily obtain different type inference systems. This is useful to make the inference appropriate for different purposes. Due to the semantic basis, the system declaratively handles type union and parametric polymorphism.
Type; inference; abstract interpretation; semantics
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11562/438152
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 26
  • ???jsp.display-item.citation.isi??? 12
social impact