Here is something that programming semanticists may find surprising and is not well known. And, as far as I know, hasn't been published.

Very few programming languages can be interpreted in the category of sets (types are sets, programs are functions). A notorious example where this *is* possible is Goedel's System T.

However, the set-theoretical model of System T is not fully abstract. A while ago a wrote a note explaining this, which gives credit to Kreisel:

https://www.cs.bham.ac.uk/~mhe/papers/tfullabs.pdf

Perhaps I should put this in the arxiv. I am not sure it is publishable, though, because, essentially, Kreisel did the work.

But it is worth noting that my exposition of the result uses the searchability of ℕ∞, the set of decreasing binary sequences, which, in topological models, is the one-point compactification of the discrete space of natural numbers.

Additionally, related to the above proof, the model of system T in which types are interpreted as compactly generated topological spaces and programs as continuous maps *is* fully abstract.

The proof of the failure uses that system T can detect non-continuity (using searchability) but everything definable in T is continuous.

The reason for the success is Kleene-Kreisel's density theorem, which implies that T can define a dense sequence of every topological space interpreting a type. We have to combine this with Hyland's characterization of the Kleene-Kreisel continuous functionals as maps of certain compactly generated spaces.

So the failure of full abstracttion of the domain theoretic model of PCF (which can be considered as an extension of T) has nothing to do with continuity.

@agdakx I think the most concise description of the SProp situation is: strengthening in the presence of SProp is undecidable because it depends on inhabitation.

Unification depends on strengthening in many places (e.g. occurrence checking) so we can't hope for completeness even in the simplest pattern fragment.

writing emails to professors like

"Dear Sir Prof. Dr. Dr. rer. nat. Lastname, it is with the utmost discomfort that I find the audacity to demand your invaluable attention for such a benign matter; unfortunately though, tackling this issue necessitates skill and experience far beyond the abilities of my humble self. Thus, I plead to your mercy and kindly ask for your assistance, if it is not too much trouble."

and getting replies like

"np here u go, cya"

Registration is now open for HoTT/UF '23: https://hott-uf.github.io/2023/

If you want to opine on interaction point boundaries do it soon (https://github.com/agda/agda/pull/6529) or forever hold your peace

... Or play around with it and submit issue reports, of course. I've tested it pretty extensively but I'm sure I'm missing something :D

Student of homotopy type theory and (higher) category theory (this account adheres to the implicit ∞-category convention).

I help maintain Agda Γ ⊢ 🐔, maintain the 1Lab 🧊🔬, and very occasionally write on my blog 👩🏫✍️

Joined Jan 2022