The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Thanks Yves, but being in English is also a requisite ;-)

And thanks Assia and Stéphane.  I'm looking for a type system for CIC
with open terms and its meta-theory.  The lmcs article is still a nice
reference.

Cheers,
Beta

On Wed, Jan 21, 2015 at 10:34 AM, Stéphane Graham-Lengrand
<lengrand AT lix.polytechnique.fr>
 wrote:
> 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
>>