The Coq mailing list

[bertot <Yves.Bertot AT inria.fr>]

On 20/1/15 1:30 PM, Beta Ziliani wrote:
> Dear Coq-club,
>
> In Chapter 4 of the reference manual there is a description of CIC on
> _closed terms_.  However, when one is doing a proof interactively, one
> is working with _open terms_.  Is there a good reference for CIC with
> open terms?  The only one I know is in Chapter 10 of Sacerdoti Coen's
> thesis, are there any others?  (In particular, I'm looking for one
> with the entire calculus in one page, instead of scattered in
> different chapters).
>
> Thanks,
> Beta
Hello, I am just thinking out loud.  My memories of the work are not so 
clear, but maybe this is also described in David Delahaye's thesis.  
Maybe he will confirm or refute my suggestion, maybe you can contact him 
through an easy internet search.

Yves