Meta-programming With Built-in Type Equality
We report our experience with exploring a new point in the design space for formal reasoning systems: the development of the programming language @Wmega. @Wmega is intended as both a practical programming language and a logic. The main goal of @Wmega is to allow programmers to describe and reason about semantic properties of programs from within the programming language itself, mainly by using a powerful type system. We illustrate the main features of @Wmega by developing an interesting meta-programming example. First, we show how to encode a set of well-typed simply typed @l-calculus terms as an @Wmega data-type. Then, we show how to implement a substitution operation on these terms that is guaranteed by the @Wmega type system to preserve their well-typedness.