Meta-programming With Built-in Type Equality (Extended Abstract)
We report our experience with exploring a new point in the design space for formal reasoning systems: the development of the programming language mega. mega is intended as both a practical programming language and a logic. The main goal of mega 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 mega by developing an interesting meta-programming example. First, we show how to encode a set of well-typed simply typed �-calculus terms as an mega data-type. Then, we show how to implement a substitution operation on these terms that is guaranteed by the mega type system to preserve their well-typedness.