[TYPES] Types for Open Terms ?

[Anthony de Almeida Lopes]

"A Typed Context Calculus" -
www.pllab.riec.tohoku.ac.jp/~ohori/research/contcalc.pdf

These are possibly less related but they both develop similar open-term systems:
http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.48.4045
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.25.4514&rank=1

I beleive that this is the final product of the above two:
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.139.346&rank=1

At one time Conor McBride gave me quite a good list to follow up which
I don't have it on me right now, but I think the main author was
actually Jojgov. It looks like he may have more to offer for you:
http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/j/Jojgov:Gueorgui_I=.html

Good luck,
- Anthony

2011/10/13 Jacques Carette <carette at mcmaster.ca>:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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
>
>
>