IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

First Annual IEEE Symposium on

Logic in Computer Science (LICS 1986)

Paper: Proof of Translation in Natural Semantics (at LICS 1986)

Authors: Joëlle Despeyroux


We have retained the purely 'formal system' part of the structural operational semantics 'a la Plotkin', and have named that view of it 'natural semantics'. Numerous examples written in this semantics have been entered in our meta-compiler Mentor + Typol. We show here that natural semantics enables us in a single formalism, to define dynamic semantics and translation of languages and to prove the correctness of a translation. Our criterion of correctness is the validity of two inference rules in a theory. Proofs are made by induction on the length of the proof. We illustrate the method on an example, treated in full: translation from Mini-ML into CAM (Categorical Abstract Machine).


    author = 	 {Joëlle Despeyroux},
    title = 	 {Proof of Translation in Natural Semantics},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {193--205},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2017-04-0512:37
Andrzej Murawski