Invited Talk: Terms, proofs and refinement (at LICS 1994)
Authors: Rod BurstallAbstract
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 Burstall}, title = {Terms, proofs and refinement}, booktitle = {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994}, year = 1994, editor = {Samson Abramsky}, month = {July}, pages = {2--7}, location = {Paris, France}, note = {Invited Talk}, publisher = {IEEE Computer Society Press} }