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!
Category theory, logical relations, term realizability and even plain set theory seem far more prevalent? Probably depends on what you're interested in doing
But many others know far more than me here
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.
As a result, there is a coherence space model for a variant of MLTT originally by Miquel, but it never gained traction.
Last updated: Jun 05 2023 at 10:01 UTC