Phase Semantics and Self-Validating Compilers

    Abstract:
   We introduce phase semantics which allows one to specify
   formally the semantics of real, non-toy, programming languages.
   Phase semantics can be considered as an executable specification
   on data structures, called certificates. If one has a compiler
   that produces a certificate, phase semantics can be used to
   check automatically that the certificate conforms to the
   semantics, and hence to validate the result of the compilation.

   We will describe the main features of phase semantics and its
   applications, such as

   * self-validating compilers
   * compiler debugging
   * formal specification of programming languages
   * formal design of programming languages
   * multi-paradigm compilation
   * programming language standardisation