Use of eCommons for rapid dissemination of COVID-19 research
In order to maximize the discoverability of COVID-19 research, and to conform with repository best practices and the requirements of publishers and research funders, we provide special guidance for COVID-19 submissions.
A Formal Account of Notational Definition
|dc.contributor.author||Griffin, Timothy G.||en_US|
|dc.description.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. This paper presents a formal account that is intended to model the practice of introducing and using notational (abbreviative) 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 $\lambda$-calculus is used to represent expressions of a given object language. A new type of equation, called a $\Delta$-equation, is introduced to model conventional definitional equations.||en_US|
|dc.title||A Formal Account of Notational Definition||en_US|