Mycroft, Alan; Jones, Neil D. 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. Cited in 9 Documents MSC: 68P05 Data structures 68Q60 Specification and verification (program logics, model checking, etc.) Keywords:higher types; Abstract interpretation; denotational metalanguage translation; power domains Citations:Zbl 0578.00007 × Cite Format Result Cite Review PDF