Abstract
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.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Abramsky, S. Strictness analysis based on logical relations. Unpublished manuscript, 1985.
Burn, G., Hankin, C. and Abramsky, S. The theory and practice of strictness analysis for higher order functions. Imperial college report DoC 85/6, 1985. To appear in Science of Computer Programming.
Cousot, P. and Cousot, R. Abstract interpretation: a unified lattice model for static analysis of programs by construction and approximation of fixpoints. Proc. ACM symp. on Principles of Programming Languages, 1977.
Damas, L. and Milner, R. Principal type schemes for functional programs. Proc. ACM symp. on Principles of Programming Languages, 1980.
Donzeau-Gouge, V. Utilisation de la sémantique dénotationelle pour l'étude d'interprétations non-standard. INRIA rapport 273, 1978.
Dybjer, P. Domain Algebras. Lecture Notes in Computer Science: Proc. 11th ICALP, vol. 172, Springer-Verlag, 1984.
Jones, N.D. and Mycroft, A. Dataflow of applicative programs using minimal function graphs. Proc. ACM symp. on Principles of Programming Languages, 1986.
Gordon, M. Models of pure LISP. Ph.D. thesis, Dept. of Artificial Intelligence, Edinburgh University, 1973.
Hindley, J.R. The principal type scheme of an object in combinatory logic. Transactions of the Amer. Math. Soc., vol 146, pp 29–60, 1969.
Milner, R. A theory of type polymorphism in programming. JCSS 1978.
Mulmuley, K. A mechanisible theory for existence proofs of inclusive predicates. CMU computer science report CMU-CS-85-149, 1985.
Mycroft, A. The theory and practice of transforming call-by-need into call-by-value. Lecture Notes in Computer Science: Proc. 4th intl. symp. on programming, vol. 83, Springer-Verlag, 1980.
Mycroft, A. Abstract Interpretation and Optimising Transformations of Applicative Programs. Ph.D. thesis, Edinburgh University, 1981. Available as computer science report CST-15-81.
Mycroft, A. and Nielson, F. Strong abstract interpretation using power domains. Lecture Notes in Computer Science: Proc. 10th ICALP, vol. 154, Springer-Verlag, 1983.
Nielson, F. Abstract interpretation using domain theory. Ph.D. thesis, Edinburgh University, 1984. Available as computer science report CST-31-84.
Plotkin, G. Lambda definability in the full type hierarchy. In [18].
Reynolds, J.C. Types, abstraction and parametric polymorphism. IFIP 83, (ed) R.E.A. Mason, North-Holland, 1983.
Seldin, J.P., and Hindley, J.R. To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism. Academic Press, 1980.
Stoy, J. Denotational semantics: the Scott-Strachey approach to programming language theory. MIT press, 1977.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mycroft, A., Jones, N.D. (1986). A relational framework for abstract interpretation. In: Ganzinger, H., Jones, N.D. (eds) Programs as Data Objects. Lecture Notes in Computer Science, vol 217. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16446-4_9
Download citation
DOI: https://doi.org/10.1007/3-540-16446-4_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16446-3
Online ISBN: 978-3-540-39786-1
eBook Packages: Springer Book Archive