Timeline for Proof-theoretic comparison table?
Current License: CC BY-SA 4.0
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 1, 2023 at 2:50 | comment | added | user21820 | @Loïc: It's been a while. Any updates? =) | |
| May 27, 2022 at 9:53 | comment | added | user21820 | @Loïc: Is there any chance that you have written down those core rules for CIC yet? =) | |
| Apr 20, 2022 at 7:32 | comment | added | user21820 | @MarioCarneiro: Thank you! Can I ask you about your thesis in detail in chat? | |
| Apr 20, 2022 at 5:12 | comment | added | Mario Carneiro | @user21820 You might find my masters thesis on the type theory of Lean illuminating. I wrote the first chapter specifically to address your concern: a single reference for a full and relatively compact specification of the logical foundation of Lean. (It is similar in spirit to Coq's foundation but it doesn't have quite as many epicycles, owing in part to its shorter history and a conscious attempt to avoid soundness issues that have plagued Coq in the past.) | |
| Mar 30, 2022 at 16:43 | comment | added | user21820 | If you would write down those rules, I would greatly appreciate it. Also, impracticality is not a big issue, because we can always plaster on some reflection mechanism on top of any system to make it practically as convenient as any equally strong system, right? =) | |
| Mar 30, 2022 at 16:37 | comment | added | Loïc Pujet | Since I am interested in normalization proofs right now, I think I could certainly write down two or three pages of typing rules for what I consider to be the "core" of CIC with respect to proof-theoretical strength. It would be terribly impractical for a proof assistant though, and other people might not agree with that core — which is why most theory papers will define their own version of the system. | |
| Mar 30, 2022 at 16:13 | comment | added | user21820 | It's alright. But could you confirm which case is it? Namely, when you speak of CIC do you have a 100% precise system in mind, which at its core (omitting redundant parts) can be described in a page or so? Or is it actually vague (like when people talk about C++)? Thanks! | |
| Mar 30, 2022 at 16:10 | comment | added | Loïc Pujet | Then I am afraid I don't know anything that fulfills these criteria, sorry! | |
| Mar 30, 2022 at 15:45 | comment | added | user21820 | No, it's terribly unsatisfactory. By "precise" I really mean that you can pass it to a good programmer and he/she can turn it into an actual proof verifier within a few days of work, without having to keep asking questions about details that simply are not stated. I find such verbose (at ≈50 pages!) and intentionally imprecise documentation really prohibitive for trying to understand what exactly makes up CIC. | |
| Mar 30, 2022 at 15:37 | comment | added | Loïc Pujet | Is the page from the Coq reference manual not satisfactory? coq.github.io/doc/v8.9/refman/language/cic.html | |
| Mar 30, 2022 at 15:27 | history | edited | Loïc Pujet | CC BY-SA 4.0 |
Make a clear distinction between what is called MLTT and what is called CC/CIC
|
| Mar 30, 2022 at 15:20 | comment | added | user21820 | Yes, sorry, I misread your CIC as predicative. But the situation you describe in your last comment is a major reason behind my question. If there is a sufficiently simple axiomatization of CIC that requires just a page or so of rules, I want to see it (and I don't care if it is missing all the 'user-friendly bells and whistles' in Coq). If not, then I'm afraid I don't see how everyone can be even sure that they are referring to the same CIC... | |
| Mar 30, 2022 at 15:16 | comment | added | Loïc Pujet | Maybe I was not clear enough in my answer: MLTT is predicative, and the CIC is impredicative (I describe it as an extension of CCω, which is impredicative, with inductive types). I don't believe I mention CIC before talking about impredicativity, so it would help me if you could point out what made you think that. | |
| Mar 30, 2022 at 15:13 | comment | added | Loïc Pujet | Other than that, there is a description in the Coq reference manual (with all the options, including SProp, coinduction, and several notions of polymorphism — but the complexity of this version means that its meta-theory is not completely clear), in Timany and Sozeau's "Consistency of the pCuIC" (but this system does not have any kind of inductive types inside of Prop, which means there is much less functions on the inductive natural numbers), and in the various formalizations of the system, such as MetaCoq. | |
| Mar 30, 2022 at 15:12 | comment | added | user21820 | No, the one in my cited PDF is impredicative, but the one in your post seems to be predicative, because you talk later about adding impredicative universes. If there is fuzziness everywhere in the literature, can you please list out explicitly all the rules in the CIC that your post is supposedly about? Thanks! | |
| Mar 30, 2022 at 15:07 | comment | added | Loïc Pujet | Like MLTT, CIC is used for several closely related systems — they all feature dependent types, an impredicative universe and inductive types, but there is some fuzziness surrounding the specifics of the (co)inductive types and the predicative universes (polymorphism, cumulativity...). I think my use of the word roughly matches the introduction of C. Paulin-Mohring, though. | |
| Mar 30, 2022 at 12:56 | comment | added | user21820 | Thank you very much. Can you provide a precise reference for CIC, that lists all the rules in one place precisely? I am not comfortable with the references I can find, which mix precise type-theory syntax with a lot of verbose English phrases. In particular, it seems that the CIC in your post is actually not the same as the CIC in the introduction I cited... | |
| Mar 30, 2022 at 2:00 | history | edited | Loïc Pujet | CC BY-SA 4.0 |
typo
|
| Mar 30, 2022 at 1:54 | history | answered | Loïc Pujet | CC BY-SA 4.0 |