Abstract
This paper describes a tool for generating embeddings of computer languages from denotational-style specifications of semantics. The language used to specify the semantics is based on ML with extra features for succinctly handling environments/states. The tool generates input for the HOL theorem prover in the form of files containing ML code. Three files are generated: one for defining the semantics as recursive functions, one containing proof rules that ‘evaluate’ the semantics, and one containing ML functions that simulate the semantics (if it is executable). The definitions allow reasoning about computer languages and specific language texts. The simulation functions provide a means of rapidly testing the semantics and/or the behaviour of language texts. The proof rules can be used for more rigorous simulation when that is appropriate. In this case the evaluation can be symbolic, i.e., parts of a language text can be replaced by logical variables. The proof rules are also useful when proving properties. The embedding generator exploits the notion of a monad (from work on functional programming languages and semantics) to handle environments in a regular way.
Research supported by the Engineering and Physical Sciences Research Council of Great Britain under grants GR/J42236 and GR/L14381. Much of this work was done while the author was at the University of Cambridge Computer Laboratory.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
R. Bahlke and G. Snelting. The PSG system: Prom formal language definitions to interactive programming environments. ACM Transactions on Programming Languages and Systems, 8(4):547–576, October 1986.
Y. Bertot and R. Fraer. Reasoning with executable specifications. In P. D. Mosses, M. Nielsen, and M. I. Schwartzbach, editors, Proceedings of the 6th International Joint Conference on Theory and Practice of Software Development (TAPSOFT'95), volume 915 of Lecture Notes in Computer Science, pages 531–545, Aarhus, Denmark, May 1995. Springer-Verlag.
L. Birkedal and M. Welinder. Partial evaluation of Standard ML. DIKU-report 93/22, DIKU, Department of Computer Science, University of Copenhagen, October 1993.
R. J. Boulton. Syn: A single language for specifying abstract syntax trees, lexical analysis, parsing and pretty-printing. Technical Report 390, University of Cambridge Computer Laboratory, March 1996.
R. J. Boulton. A tool to support formal reasoning about computer languages. In E. Brinksma, editor, Proceedings of the Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'97), volume 1217 of Lecture Notes in Computer Science, pages 81–95, Enschede, The Netherlands, April 1997. Springer.
G. Collins and D. Syme. A theory of finite maps. In Schubert et al. [15], pages 122–137.
E. L. Gunter. A broader class of trees for recursive type definitions for HOL. In J. J. Joyce and C.-J. H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and its Applications (HUG '93), volume 780 of Lecture Notes in Computer Science, pages 141–154, Vancouver, B.C., Canada, August 1993. Springer-Verlag, 1994.
R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, July 1991.
L. Paulson. A higher-order implementation of rewriting. Science of Computer Programming, 3:119–149, 1983.
M. Pettersson and P. Pritzson. DML — a meta-language and system for the generation of practical and efficient compilers from denotational specifications. In Proceedings of the 4th International Conference on Computer Languages (ICCL'92), pages 127–136. IEEE, April 1992.
R. Reetz. Deep embedding VHDL. In Schubert et al. [15]., pages 277–292.
R. Reetz and T. Kropf. Simplifying deep embedding: A formalised code generator. In T. F. Melham and J. Camilleri, editors, Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and Its Applications, volume 859 of Lecture Notes in Computer Science, pages 378–390, Valletta, Malta, September 1994. Springer-Verlag.
F. Regensburger. HOLCF: Higher order logic of computable functions. In Schubert et al. [15]., pages 293–307.
E. T. Schubert, P. J. Windley, and J. Alves-Foss, editors. Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, volume 971 of Lecture Notes in Computer Science, Aspen Grove, UT, USA, September 1995. Springer-Verlag.
K. Slind. Function definition in higher-order logic. In J. von Wright, J. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'96), volume 1125 of Lecture Notes in Computer Science, pages 381–397, Turku, Finland, August 1996. Springer.
P. Wadler. The essence of functional programming. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1–14, Albuquerque, New Mexico, USA, January 1992.
M. Welinder. Very efficient conversions. In Schubert et al. [15], pages 340–352.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boulton, R.J. (1998). Generating embeddings from denotational descriptions. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055130
Download citation
DOI: https://doi.org/10.1007/BFb0055130
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64987-8
Online ISBN: 978-3-540-49801-8
eBook Packages: Springer Book Archive