Wed 7 Nov 2018 20:17 - 20:19 at Georgian - Poster & SRC
In this research, we introduce a metalanguage, METACO that we engineered, as a specification language of type systems based on simply typed lambda calculus, extended with coercive subtyping and overloaded function symbols. A metalanguage here refers to a formal language that stipulates an object programming language or an aspect of it. METACO is a metalanguage that stipulates the type system of an object language.
Such a specification in METACO is called a METACO script, and each METACO script stipulates a type universe with a coercive subtyping relation on it, as well as a set of overloaded function symbols. METACO is implemented as a source code generator which, when given a METACO script, generates a type checker function that checks a source term in language $\lambda^{\rightarrow}{\mu \text{co}}$, which may contain subterms that only type checks when the subtying relation is regarded and overloading resolution needed. When such a source term type checks, the type checker returns a well typed term in a simply typed language $\lambda^{\rightarrow}{\mu}$.
