Skip to main content
SpringerLink
Log in
Book cover

HOL Users' Group Workshop

HUG 1994: Higher Order Logic Theorem Proving and Its Applications pp 378–390Cite as

Simplifying deep embedding: A formalised code generator

  • Invited Paper
  • Conference paper
  • First Online:

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

Abstract

A tool is described, which simplifies the formalisation method “deep embedding” for a system with syntax and semantics in the following way: a formalisation of the syntax described by a context-free grammar is automatically generated and a formalisation of the complete semantics for the given syntax is simplified by automatically generating a formal code generator out of a formalised context-restricted semantics.

This work was financed by the German research society (DFG) under contract SFB 358.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. de Barros Lucena. Reasoning about petri nets in HOL. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, HOL Theorem Proving System and its Applications, pages 384–394, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA, IEEE Computer Society Press.

    Google Scholar 

  2. P. Curzon. A verified compiler for a structured assembly language. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, HOL Theorem Proving System and its Applications, pages 253–262, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA, IEEE Computer Society Press.

    Google Scholar 

  3. E. Gunter. A broader class of trees for recursive type definitions for HOL. In HUG93, HOL User's Group Workshop, Vancouver, Canada, August 1993. Springer Verlag.

    Google Scholar 

  4. J.E. Hopcroft and J.D. Ullman. Introduction to automata theory, languages, and computation. Addison Wesley, 1979.

    Google Scholar 

  5. D.F. Martin and R.J. Toal. Case studies in compiler correctness using HOL. In M. Archer, J.J. Joyce, K.N. Levitt, and P.J. Windley, editors, HOL Theorem Proving System and its Applications, pages 242–252, Davis, California, August 1991. IEEE Computer Society, ACM SIGDA, IEEE Computer Society Press.

    Google Scholar 

  6. T.F. Melham. A mechanized theory of the π-calculus in HOL. Technical Report 244, University of Cambridge, Computer Laboratory, Cambridge, England, January 1992.

    Google Scholar 

  7. R. Reetz and Th. Kropf. Formalisierung eines Flussgraphmodells in Logik hoeherer Ordnung und dessen Anwendung in der Hardware-Verifikation. In D. Monjau, editor, Rechnergestuetzter Entwurf und Architektur mikroelektronischer Systeme, pages 193–202, Oberwiesenthal, Germany, May 1994. Gesellschaft fuer Informatik e.V. (GI).

    Google Scholar 

  8. R. Ripken. Generating an intermediate-code generator in a compiler-writing system. In E. Gelenbe and D. Potier, editors, International Computing Symposium, pages 121–127. North Holland, 1975.

    Google Scholar 

  9. IEEE standard VHDL language reference manual. Std 1076, IEEE, 1987.

    Google Scholar 

  10. C. Zhang, R. Shaw, R. Olsson, K. Levitt, M. Archer, M. Heckman, and G. Benson. Mechanizing a programming logic for the concurrent programming language microSR in HOL. In HUG93, HOL User's Group Workshop, Vancouver, Canada, August 1993. Springer Verlag.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut fuer Rechnerentwurf und Fehlertoleranz, Universitaet Karlsruhe, Zirkel 2, Postfach 6980, 76128, Karlsruhe, Germany

    Ralf Reetz & Thomas Kropf

Authors
  1. Ralf Reetz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thomas Kropf
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Thomas F. Melham Juanito Camilleri

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Reetz, R., Kropf, T. (1994). Simplifying deep embedding: A formalised code generator. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_55

Download citation

  • DOI: https://doi.org/10.1007/3-540-58450-1_55

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-48803-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation