Paper: Notational definition-a formal account (at LICS 1988)
Authors: Timothy GriffinAbstract
In the course of developing a mathematical theory or proof it is a common practice to introduce new notation to represent notation that is previously understood. The author presents a formal account that is intended to model the practice of introducing and using notational (abbreviate) definitions. The aim of this work is a pragmatic one: to provide a framework useful in the design and implementation of secure proof system interfaces which accommodate, as much as possible, conventional mathematical practice. A typed λ-calculus is used to represent expressions of a given object language. A Δ-equation is introduced to model conventional definition equations
BibTeX
@InProceedings{Griffin-Notationaldefinitio, author = {Timothy Griffin}, title = {Notational definition-a formal account}, booktitle = {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988}, year = 1988, editor = {Yuri Gurevich}, month = {July}, pages = {372--383}, location = {Edinburgh, Scotland, UK}, publisher = {IEEE Computer Society Press} }