[TYPES] Implementations using explicit substitutions

[Michael Norrish]

Carsten Schuermann wrote:
> We are currently writing a paper on explicit substitution calculi, and we
> would like to include references to implementations of proof
> assistants, theorem provers, and programming languages that use them.  

> If you are aware of any such system please send us an email. 

Bruno Barras implemented an explicit substitution mechanism for the HOL4 
kernel.  This, and its advantages, are described in

@InProceedings{Barras:2000:HOL-EVAL,
  author =       {Bruno Barras},
  title =        {Programming and Computing in {HOL}},
  crossref =  {tphols2000},
  pages =     {17--37},
  year =      2000,
  doi = {10.1007/3-540-44659-1_2},
}

Bruno's code is still part of the system.

Michael.