Paper Info
Title
Meta-programming With Built-in Type Equality
Abstract
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.
Year
DOI
Venue
2008
10.1016/j.entcs.2007.11.012
Electr. Notes Theor. Comput. Sci.
Keywords
Field
DocType
practical programming language,equality types,main feature,powerful type system,formal reasoning system,built-in type equality,wmega data-type,design space,interesting meta-programming example,main goal,meta-language,programming language,wmega type system,meta-programming,type system,data type,meta language,meta programming
Functional logic programming,Programming language specification,Programming language,Programming paradigm,Computer science,Inductive programming,Theoretical computer science,Very high-level programming language,First-generation programming language,Programming language theory,Programming domain
Journal
Volume
ISSN
Citations 
199,
Electronic Notes in Theoretical Computer Science
21
PageRank 
References 
Authors
1.12
10
2
Name
Order
Citations
PageRank
Tim Sheard11691460.87
Emir Pasalic219255.42