Paper Info
Title
Generating Embeddings from Denotational Descriptions
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.
Year
DOI
Venue
1998
10.1007/BFb0055130
TPHOLs
Keywords
Field
DocType
denotational descriptions,generating embeddings,functional programming language,theorem prover,specification language
Formal semantics (linguistics),Operational semantics,Programming language,Computer science,Computational semantics,Denotational semantics,Action semantics,Algorithm,Theoretical computer science,Failure semantics,Well-founded semantics,Semantics (computer science)
Conference
Volume
ISSN
ISBN
1479
0302-9743
3-540-64987-5
Citations 
PageRank 
References 
3
0.45
14
Authors
1
Name
Order
Citations
PageRank
Richard J. Boulton125523.64