Invited Paper: Terms, proofs and refinement (at LICS 1994)

Authors: Rod M. Burstall

Abstract

We give a simple account of the connection between lambda terms and natural deduction proofs, showing how the terms can be rearranged into a form close to conventional proofs, and also to less conventional “top down” proofs. Creating proofs interactively by refinement can be seen as just keying in a lambda expression one symbol at a time in response to prompts from the machine. The aim is to convey some basic ideas to the uninitiated without technical or pragmatic detail

BibTeX

  @InProceedings{Burstall-Termsproofsandrefin,
    author = 	 {Rod M. Burstall},
    title = 	 {Terms, proofs and refinement},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {2--7},
    location =   {Paris, France}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }