[TYPES] Implementations using explicit substitutions

[Dan Doel]

This is not a programming language or theorem prover per-se, but James 
Chapman's thesis, Type checking and normalisation*, uses a term representation 
with explicit substitutions for doing the titular activities in a (total,) 
dependently typed functional language. The thesis is written mainly in 
Epigram, but it could be translated into plenty of other languages.

Cheers,
-- Dan

* http://www.cs.ioc.ee/~james/PUBLICATION.html