Skip to main content
SpringerLink
Log in

Using domain algebras to prove the correctness of a compiler

  • Conference paper
  • First Online:
Book cover STACS 85 (STACS 1985)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 182))

Included in the following conference series:

Abstract

Domain algebras are proposed as a tool for structuring compiler correctness proofs which are based on denotational semantics of the source and target language. The correctness of a compiler for a small imperative language is proved as an illustration.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • ADJ (= Goguen, J.A., Thatcher, J.W., Wagner, E.G.), An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types, in Current Trends in Programming Methodology, R. Yeh Ed., (Prentice-Hall, 1978) 80–149.

    Google Scholar 

  • ADJ (= Thatcher, J.W., Wagner, E.G., Wright, J.B.), More on Advice on Structuring Compilers and Proving them Correct, Theoretical Computer Science 15, (1981) 223–249.

    Google Scholar 

  • Berry, G., Modèles complètement adéquats et stables des lambda-calculs typés, Thèse de doctorat d'etat ès sciences mathematiques, l'université Paris VII (1979).

    Google Scholar 

  • Berry, G., Some Syntactic and Categorical Constructions of Lambda-Calculus Models, Rapport INRIA 80 (1981).

    Google Scholar 

  • Burstall, R.M. and Landin, P.J., Programs and their Proofs: An Algebraic Approach, Machine Intelligence 4, (Edinburgh University Press, 1969) 17–44.

    Google Scholar 

  • Cohn, A.J., High Level Proofs in LCF, Report CSR-35-78, Department of Computer Science, University of Edinburgh (1978).

    Google Scholar 

  • Curien, P.L., Combinateurs categoriques, algorithmes sequentiels et programmation applicative, Thèse de doctorat d'etat ès sciences mathematiques, l'université Paris VII (1983).

    Google Scholar 

  • Dybjer, P., Category-Theoretic Logics and Algebras of Programs, Ph.D. thesis, Chalmers University of Technology, Göteborg (1983).

    Google Scholar 

  • Dybjer, P., Domain Algebras, in Proceedings 11th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science 172 (Springer-Verlag, Berlin, 1984) 138–150.

    Google Scholar 

  • Gordon, M., The Denotational Description of Programming Languages, (Springer-Verlag, Berlin, 1979).

    Google Scholar 

  • Gordon, M., Milner, R., Wadsworth, C.P., Edinburgh LCF, Lecture Notes in Computer Science 78, (Springer-Verlag, 1979).

    Google Scholar 

  • Lambek, J. (1972), Deductive Systems and Categories III, in Proceedings Dalhousie Conference on Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, (Springer-Verlag, 1972) 57–82.

    Google Scholar 

  • Lehmann, D.J. and Smyth, M.B., Algebraic Specification of Data Types: A Synthetic Approach, Mathematical Systems Theory 14, (1981) 79–139.

    Google Scholar 

  • McCarthy, J. and Painter, J.A., Correctness of a Compiler for Arithmetical Expressions, in J.T. Schwartz (ed.), in Proceedings of a Symposium in Applied Mathematics, 19, Mathematical Aspects of Computer Science, (American Mathematical Society, New York, 1967).

    Google Scholar 

  • Milner, R., Morris, L., Newey, M., A Logic for Computable Functions with Reflexive and Polymorphic Types, in Proceedings Conference on Proving and Improving Programs, Arc-et-Senans (1975).

    Google Scholar 

  • Morris, F.L., Advice on Structuring Compilers and Proving them Correct, in Proceedings ACM Symposium on Principles of Programming Languages, Boston (1973) 144–152.

    Google Scholar 

  • Plotkin, G.D., Domains, Edinburgh CS Dept., lecture notes (1980).

    Google Scholar 

  • Poigne, A., On Semantic Algebras Higher-Order Structures, Forschungsbericht bericht 156, Abt. Informatik, Universität Dortmund (1983).

    Google Scholar 

  • Russel, B., Implementation Correctness Involving a Language with GOTO Statements, SIAM Journal on Computing 6, (1977).

    Google Scholar 

  • Scott, D.S., Relating Theories of the Lambda-Calculus, in J.P. Seldin and J.R. Hindley (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, (Academic Press, 1980), 404–450.

    Google Scholar 

  • Scott, D.S., Domains for Denotational Semantics, in Proceedings 9th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, (Springer-Verlag, 1982) 577–613.

    Google Scholar 

  • Smyth, M.B. and Plotkin, G.D., The Category-Theoretic Solution of Recursive Domain Equations, SIAM Journal on Computing 11 (1982).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programming Methodology Group Department of Computer Sciences, Chalmers University of Technology, S-412 96, Göteborg, Sweden

    Peter Dybjer

Authors
  1. Peter Dybjer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

K. Mehlhorn

Rights and permissions

Reprints and permissions

Copyright information

© 1984 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Dybjer, P. (1984). Using domain algebras to prove the correctness of a compiler. In: Mehlhorn, K. (eds) STACS 85. STACS 1985. Lecture Notes in Computer Science, vol 182. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023999

Download citation

  • DOI: https://doi.org/10.1007/BFb0023999

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-13912-6

  • Online ISBN: 978-3-540-39136-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation