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} }