[TYPES] Implementations using explicit substitutions

[Avik Chaudhuri]

This is perhaps a non-standard application of explicit substitutions:  
in the following paper we show how to formalize and enforce a data- 
flow security property using explicit substitutions to track taints in  
the underlying language.
(The language is intended to provide an abstract model of a particular  
operating system's security environment.)

http://portal.acm.org/citation.cfm?doid=1513443.1513447

-Avik.

On Jan 6, 2010, at 8:13 AM, 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
>