Two-Level Semantics and Abstract Interpretation

Publication: Research - peer-reviewJournal article – Annual report year: 1989

View graph of relations

Two-level semantics is a variant of Scott/Strachey denotational semantics in which the concept of binding time is treated explicitly. This is done by formally distinguishing between those computations that take place at run-time and those that take place at compile-time. Abstract interpretation is concerned with the (preferably automatic) analysis of programs. The main purpose of these analyses is to find information that may assist in the efficient implementation of the programs. Abstract interpretation is thus related to data flow analysis, partial evaluation and other program analysis methods. Its unique flavour is the insistence on formal proofs of correctness and the methods used to establish these. This paper develops a theory of abstract interpretation for two-level denotational definitions. There are three ingredients in this. First a framework for proving the correctness of analyses is developed. This may also be used to compare the precision of various analyses. Next it is shown that, given a choice of properties of programs, one may specify a most precise analysis (or best induced analysis). This may also be used to investigate the collecting semantics (or static semantics). Finally, it is shown how to modify the most precise analysis in order to obtain an implementable analysis where one trades off precision for implementability
Original languageEnglish
JournalTheoretical Computer Science -- Fundamental Studies
Publication date1989
Volume69
Journal number2
Pages117-242
ISSN0304-3975
StatePublished
Download as:
Download as PDF
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBEHarvardMLAStandardVancouverShortLong
Word

ID: 2704743