Paper: Notational definition-a formal account (at LICS 1988)

Authors: Timothy G. Griffin

Abstract

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 G. Griffin},
    title = 	 {Notational definition-a formal account},
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {372--383},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }