[TYPES] Types for Open Terms ?

[Herman Geuvers]

Dear Jacques Carette,

Apart from this there is also the PhD thesis og Jojgov, that I can't 
find on-line anywhere.

Georgi Jojgov,
Incomplete proofs and terms and their use in interactive theorem proving 
(PhD thesis, Eindhoven 2004)

I will send you a copy of it via surface mail and I'll contact Jojgov 
whether he has it in electronic form somewhere.

Best

Herman Geuvers

> [ 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
>


-- 
Herman Geuvers
Professor of Computer Science
Intelligent Systems, iCIS
Faculty of Science
Radboud University Nijmegen, NL