Changing page name because the acronym “CLF” is used for “Concurrent Logical Framework”.
]]>It seems that subtyping variance rules are derivable after all, without having to add more primitive rules.
]]>Finished filling in the sections on logical frameworks.
]]>Filled in the LF= section. Improved the reference to Andromeda. (There’s now also an arXiv link.)
]]>atmacen, are you Matt Oliveri?
]]>Finally put stuff in “PER theory”, although it’s not the material I was originally planning to put there. For now, it explains refinement-style quotients.
]]>I probably ought to split this page up. Also, a lot of the stuff on logical frameworks should probably be on logical framework.
]]>Finally started adding stuff about logical frameworks.
]]>Cleaned up and slightly expanded the explanation about nonadmissibility of strengthening.
]]>Added section about how “constructive”, “intuitionistic”, and classical propositions are represented in CLF (and also Nuprl), along with discussion of the difference between constructive and intuitionistic in this sense.
]]>Expanded the “Idea/Method” subsection with explanation of how checking proof terms relates to tactic engines.
]]>Noting that on-the-fly realizer extraction, aka dependent proof refinement, is also implemented in RedPRL, and is apparently a style of elaboration.
]]>Greatly expanded “Idea” section, with more discussion about the “why” and “how” of CLF, gist of the expected proof system, and connection to Cedille. Also, an extra reference, about proof checking.
]]>Probably depends on what you’re trying to do.
]]>The problem with large types (if my expectations are correct) is the universes. Nuprl-style universes are different from ETT universes. I’m wondering if that’s really a problem though, since neither kind of universe is univalent. They’re both arbitrary ways of coding for the “real” types, from a univalent perspective. Are ETT universes somehow preferable anyway?
]]>Hmm. One does generally want to prove things about large types too.
]]>Maybe my grammar was too weird. There are generally three categories involved: the syntactic category of an ETT, the syntactic category of a Nuprl-style system, and a full subcategory of small ETT types. The translation functor I have in mind is only an embedding of the small types.
]]>I’m not sure what you mean when talking about universes, but aside from that, yes I think if the syntactic category of one theory embeds full-faithfully in another one then that would be sufficient.
]]>I’ve been too vague about what I want the result to actually say. I don’t want to commit to a precise formulation because I don’t know what features are needed from ETT to get anywhere.
I think a way to say the gist of what I expect is that the full subcategory corresponding to the small types, of the syntactic category of ETT embeds into the syntactic category of an appropriate Nuprl-style system. The small types are the ETT types in the bottom universe, if the ETT has universes, otherwise it’s all of them.
So there’s a syntactic translation from ETT terms to Nuprl-style terms. That part is clear once all the required type constructors are available on the Nuprl side. (Although it’s not shown (yet?), you can construct sigmas and coproducts in CLF.) So I think the translation, along with a proof that it preserves typing, is a functor, and the conservativity result makes it full and faithful.
]]>I don’t immediately see any counterexamples, but I haven’t really looked. A conservativity result might resolve the semantic problem, though it might depend on the precise form of the result.
]]>It occurred to me that curly braces was an awful choice of notation for squash, since set theory uses that for singleton sets. BTW, singleton types are ambiguous: you also need to specify equality. But still.
]]>If you think there should be a conservativity result, the onus is on you to prove it.
Of course. I was wondering two things: