1. What is a dependent type 1. ADT -- the simplest dependent-type 2. Singleton types 3. Branding: type proxies 2. Lightweight static capabilities 1. Abstract and Introduction 2. Formalization and proofs 3. Accompanying source code 3. The question of verification 4. Genuine Dependent-type systems This is a joint work with Chung-chieh Shan. We describe several approaches to lightweight dependent-type programming, letting us gain experience with dependent types on existing programming language systems All these lightweight approaches rely on type-level proxies for values, so we can statically express properties (e.g., equality, inequality) of the values that are not generally known until the run time. ``This much is clear: many programmers are already finding practical uses for the approximants to dependent types which mainstream functional languages (especially Haskell) admit, by hook or by crook.''
mini languages which demonstrate various techniques in design and implementation of programming languages. The languages are implemented in Objective Caml. I teach Theory of Programming Languages at University of Ljubljana. For the course I implemented languages which demonstrate basic concepts such as parsing, type checking, type inference, dynamic types, evaluation strategies, and compilation. They are deliberately very simple, as each language introduces only one or two new basic ideas. You should find the source code useful if you want to learn how things are done. calc, miniml, boa, levy