Combining Deep and Shallow Embeddings

This paper presents an approach for verifying translator correctness when the source language has formal semantics. Instead of verifying the translator implementation, a novel language mechanization combination is devised to reduce total complexity involved. A deep embedding is defined to serve as a baseline for specification meaning. For each specification, an equivalence proof is constructed and conducted to ensure that the translated shallow representation is semantically equivalent to the deep representation. Structure of an equivalence proof is systematic and can be derived from specification structure mechanically. The use of two embeddings also affects the embeddings favourably by enabling them to be defined in a simpler manner.