Paper: Conditional lambda-theories and the verification of static properties of programs (at LICS 1990)

Authors: Mitchell Wand Zheng-Yu Wang

Abstract

A proof that a simple compiler correctly uses the static properties in its symbol table is presented. This is done by regarding the target code produced by the compiler as a syntactic variant of a λ-term. In general, this λ-term C may not be equal to the semantics S of the source program: they need to equal only when information in the symbol table is valid. Rules of inference for conditional λ-judgements are presented, and their soundness is proven. These rules are then used to prove the correctness of a simple compiler that relies on a symbol table. The form of the proof suggests that such proofs may be largely mechanizable

BibTeX

  @InProceedings{WandWang-Conditionallambdath,
    author = 	 {Mitchell Wand and Zheng-Yu Wang},
    title = 	 {Conditional lambda-theories and the verification of static properties of programs },
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {321--332},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }