Home
Scholarly Works
Theory Morphisms in Church’s Type Theory with...
Conference

Theory Morphisms in Church’s Type Theory with Quotation and Evaluation

Abstract

Abstract$${\textsc {ctt}}_\mathrm{qe}$$ is a version of Church’s type theory with global quotation and evaluation operators that is engineered to reason about the interplay of syntax and semantics and to formalize syntax-based mathematical algorithms. $${\textsc {ctt}}_\mathrm{uqe}$$ is a variant of $${\textsc {ctt}}_\mathrm{qe}$$ that admits undefined expressions, partial functions, and multiple base types of individuals. It is better suited than $${\textsc {ctt}}_\mathrm{qe}$$ as a logic for building networks of theories connected by theory morphisms. This paper presents the syntax and semantics of $${\textsc {ctt}}_\mathrm{uqe}$$, defines a notion of a theory morphism from one $${\textsc {ctt}}_\mathrm{uqe}$$ theory to another, and gives two simple examples involving monoids that illustrate the use of theory morphisms in $${\textsc {ctt}}_\mathrm{uqe}$$.

Authors

Farmer WM

Series

Lecture Notes in Computer Science

Volume

10383

Pagination

pp. 147-162

Publisher

Springer Nature

Publication Date

January 1, 2017

DOI

10.1007/978-3-319-62075-6_11

Conference proceedings

Lecture Notes in Computer Science

ISSN

0302-9743

Labels

View published work (Non-McMaster Users)

Contact the Experts team