The Coq mailing list

[Ali Assaf <ali.assaf AT inria.fr>]

Hi,

The description of Matita's kernel implementation in "A compact kernel for 
the calculus of inductive constructions" contains a type system in the 
appendix that includes metavariables, although it is not commented.

Best,

Ali

----- Original Message -----
> From: "Beta Ziliani" 
> <beta AT mpi-sws.org>
> To: "Coq Club" 
> <coq-club AT inria.fr>
> Cc: "Assia Mahboubi" 
> <Assia.Mahboubi AT inria.fr>
> Sent: Wednesday, January 21, 2015 7:16:08 PM
> Subject: Re: [Coq-Club] CIC with open terms
> 
> 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
> >>
>