[TYPES] Types for Open Terms ?

[Andrea Asperti]

Dear Jacques,
if I understood what you are looking for, you could also be interested 
in recent
paper (under submission) by myself, Ricciotti, Sacerdoti Coen and Tassi, 
entitled
"A bidirectional refinement algorithm for the Calculus of (Co)Inductive 
Constructions".
I'll send you a copy by email.
Best.
-- andrea

Herman Geuvers wrote:
> [ The Types Forum, 
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> 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
>>
>
>