coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] CIC with open terms

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] CIC with open terms
Date: Tue, 20 Jan 2015 13:30:35 +0100

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

[Coq-Club] CIC with open terms, Beta Ziliani, 01/20/2015
- Re: [Coq-Club] CIC with open terms, bertot, 01/21/2015
  - Re: [Coq-Club] CIC with open terms, Assia Mahboubi, 01/21/2015
    - Re: [Coq-Club] CIC with open terms, Stéphane Graham-Lengrand, 01/21/2015
      - Re: [Coq-Club] CIC with open terms, Beta Ziliani, 01/21/2015
        
        Re: [Coq-Club] CIC with open terms, Ali Assaf, 01/21/2015
        
        Re: [Coq-Club] CIC with open terms, Enrico Tassi, 01/21/2015
        
        Re: [Coq-Club] CIC with open terms, Beta Ziliani, 01/23/2015