The Coq mailing list

[Stéphane Graham-Lengrand <lengrand AT lix.polytechnique.fr>]

On 21/01/2015 09:53, Assia Mahboubi wrote:
> 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

Yes, it's for Pure Type Systems, in particular CoC, so it doesn't deal
with inductive types.

There's one big Figure with all the rules (p. 21).
Note that the system aims at describing the completion of open proofs
into complete proofs (which is probably the activity for which you want
open proof-terms), rather than type-checking open proof-terms.
But I don't know which one you are interested in.
Anyway, the theorem is that, if you manage to complete your proof using
the inference system with open proof-terms, then you can extract from it
a closed proof-term that is necessarily well-typed. So in theory, no
need to type-check at QED.

Best,

Stéphane



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