zbMATH — the first resource for mathematics

A relational framework for abstract interpretation. (English) Zbl 0585.68032
Programs as data objects, Proc. Workshop, Copenhagen/Den. 1985, Lect. Notes Comput. Sci. 217, 156-171 (1986).
Summary: [For the entire collection see Zbl 0578.00007.]
Abstract interpretation is a very general framework for proving certain properties of programs. This is done by interpreting the symbols of the program, or the symbols of a denotational metalanguage translation, in two different ways (the standard interpretation and the abstract interpretation) and relating them. We set up a new framework for abstract interpretation based on relations (with the intent of inclusive or logical relations). This avoids problems with power domains and enables certain higher-order frameworks to be proved correct. As an example we show how the Hindley/Milner type system can be viewed as a special case of our system and is thus automatically correct.

68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)