Tan Yee Jian (Feb 11 2023 at 02:45): Tan Yee Jian (Feb 11 2023 at 02:45):Hi all! I was reading Chapter 8 of Proof and Types by Girard, which was on Coherence Spaces as a model of Type Theory. Is this still the prevalent/updated/mainstream semantics model, compared to other models, say Scott's? Just wondering how relevant it is to the most recent theory. Thanks in advance!
Paolo Giarrusso (Feb 11 2023 at 03:36):Category theory, logical relations, term realizability and even plain set theory seem far more prevalent? Probably depends on what you're interested in doing
Paolo Giarrusso (Feb 11 2023 at 03:38):But many others know far more than me here
Pierre-Marie Pédrot (Feb 11 2023 at 10:02):I'd say that this really depends on what you call type theory. Scott domains (and from there coherence spaces) are designed to handle the one tricky point of λ-calculus, i.e. the non-termination effect / arbitrary fixpoints. In general the type system considered for these models is dumb, usually some flavour of simple types. Contrastingly this whole fixpoint issue is irrelevant in MLTT because there one (almost) only cares about SN systems. There the complexity comes from the very intricate type system with dependent types, large elimination and whatnot.
Pierre-Marie Pédrot (Feb 11 2023 at 10:04):As a result, there is a coherence space model for a variant of MLTT originally by Miquel, but it never gained traction.
Last updated: Apr 16 2024 at 18:02 UTC