<p>This thesis presents several module systems, in particular Mei and DMei, designed for mechanized mathematics systems. Mei is a λ-calculus style module system that supports higher-order functors in a natural way. The semantics of functor application is based on substitution. A novel coercion mechanism integrates a parameter passing mechanism based on theory interpretations with simple λ-calculus style higher-order functors. DMei extends Mei by supporting dependent functor types. Mei is the first module system that successfully supports both higher-order functors and a parameter passing mechanism based on theory interpretations.</p> / Thesis / Doctor of Philosophy (PhD)

<p>Effective definedness checking is crucial for an implementation of a logic with undefinedness. The objective of the MathScheme project is to develop a new approach to mechanized mathematics that seeks to combine the capabilities of computer algebra systems and computer theorem proving systems. Chiron, the underlying logic of MathScheme, is a logic with undefinedness. Therefore, it is important to automate, to the greatest extent possible, the process of checking the definedness of Chiron expressions for the MathScheme project. This thesis provides an overview of information useful for checking definedness of Chiron expressions and presents the design and implementation of an AND/OR tree-based approach for automated definedness checking based on ideas from artificial intelligence. The theorems for definedness checking are outlined first, and then a three-valued AND/OR tree is presented, and finally, the algorithm for reducing Chiron definedness problems using AND/OR trees is illustrated. An implementation of the definedness checking system is provided that is based on the theorems and algorithm. The ultimate goal of this system is to provide a powerful mechanism to automatically reduce a definedness problem to simpler definedness problems that can be easily, or perhaps automatically, checked.</p> / Master of Science (MSc)