A type system for the language of effective definitions (LED)
This work develops the Language of Effective Definition (LED), a functional programming language. The syntax, semantics, and type system are defined. This work defines a small-step reduction semantic for LED, so that an approach that is commonly used the type system community could be used to prove the main theorem. A static type system is defined and implemented for LED. The type system requires explicit type declarations, and allows polymorphic functions such as map and fold to be defined checked by the type system. Additionally, type rules which allow programmers to create their own data types are supported. The main theorem of this work is that LED is type safe under the type system described. Intuitively, a language type safe, if its type system can be used to guarantee that a certain errors called a run-time type errors will not occur during evaluation. The practical advantages of a static type are that errors can be detected and corrected as early as possible in development.