Meta-circular interpreter for a strongly typed language

A functional language is introduced, whose type system is defined by its meta-circular interpreter. The functional language is an extension of λ-calculus augmented with the rule for conditional terms that allows the condition of a conditional term to be used for reducing its branches. This makes it possible to deduce the well-typing of terms with dependent types including the meta-circular interpreter. In the type system built by the interpreter, types are represented by ordinary terms, which reflects the recent object-oriented programming languages, in which classes are manipulated as ordinary objects. The paper first discusses the untyped system of the functional language and its consistency, then develops the representation of types and the representation of terms, and define a meta-circular interpreter, by which the well-typing of the language is defined and also discusses the extensibility of the interpreter and the type system