[TYPES] Types for Open Terms ?

[Jacques Carette]

I have been looking to find relevant work on types for open terms, i.e. 
types for terms with free variables which are *not* in an environment.

I have been able to find some work by Westbrook [1], Geuvers and Jojgov 
[2], Geuvers, Krebbers, McKinna and Wiedijk [3] directly on this, as 
well as depply inside Sacerdoti Coen's thesis [4].  It appears that and 
Nanevski, Pfenning and Pientka [5]'s contextual modal type theory is 
"related" (but scary in its complexity...), as compared say with 
Rhiger's much simpler system [6] which seems to offer similar benefits 
as far as my needs go.

What have I missed?

Jacques

[1] http://www.divms.uiowa.edu/~astump/papers/tfp06-free-var-types.pdf
[2] http://www.cs.ru.nl/~herman/PUBS/openlogic.pdf
[3] http://arxiv.org/abs/1009.2792v1
[4] http://www.cs.unibo.it/~sacerdot/tesidott/thesis.ps.gz
[5] http://dl.acm.org/citation.cfm?id=1352591
[6] http://akira.ruc.dk/~mir/Reports/tfp05-revised.pdf