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 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 metaprogramming 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. Key words: Meta-programming, Meta-language, Equality types

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Tim Sheard, Emir Pasalic
• Keywords: ENTCS 2008, Practical Programming Language, Programming Language, Type System