[TYPES] Implementations using explicit substitutions

[Alan Jeffrey]

Back in the mists of time (when the design of OO languages with generics 
were the new new thing) I ran a course on design of OO languages.  The 
interpreter used explicit substitutions as the model of variable 
binding, which provides a nice bridge between the formal model of 
substitution and an interpreter based on dictionaries.

The course description, including the sources (you'd be after 
hobbes.transform.Substitution) is at:

    http://fpl.cs.depaul.edu/ajeffrey/se580/

or you can just run the applet (yes, an applet, did I mention the class 
was a while back?) at:

    http://fpl.cs.depaul.edu/ajeffrey/se580/applet/

which shows explicit substitutions in action.

Alan Jeffrey.

Carsten Schuermann wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> 
> ------------------------------------------------------------------------
> 
> Dear colleagues,
> 
> 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. 
> 
> Best regards,
> -- Anders Schack-Nielsen and Carsten Schuermann
>