Logic in Computer Science (LICS 1990)

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

Authors: Wand, M. Wang, Z.-Y.

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 = 	 {Wand, M. and Wang, Z.-Y.},
    title = 	 {Conditional lambda-theories and the verification of static properties of programs },
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {321--332},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }