Skip to main content
3 votes

What is a model theory / category theory basis of System F-omega that corresponds to what programmers actually do?

Your description of an idealized computer is a nescient form of realizability, and there are very simple realizability models of parametric polymorphism. Take a model of computatation (an "...
Andrej Bauer's user avatar
  • 28.9k
1 vote
Accepted

Formalising Church numerals in Agda

I think your neutral-bad lemma is too general. For instance: $$f : τ ⇒ σ, x : τ ⊢ f\ x : σ$$ $σ$ does not occur in the context, but there is a neutral term with its ...
Dan Doel's user avatar
  • 1,021

Only top scored, non community-wiki answers of a minimum length are eligible