The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

Dear Beta,

may be not exactly what you're looking for, but close enough I think and
including the relevant bibliography:

S. Lengrand, R. Dyckhoff, and J. McKinna. A focused sequent calculus framework
for proof search in Pure Type Systems. Logical Methods in Computer Science,
7(1), 2011.

http://www.lmcs-online.org/ojs/viewarticle.php?id=566&layout=abstract

Best,

assia

Le 21/01/2015 08:18, bertot a écrit :
> 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