Categorical semantics for F_\omega

I've been having trouble finding papers on giving a categorical semantics to F or F_\omega. I know the book "Categorical Logic and Type Theory" gets into this material a bit, but I'm presuming there's been papers on the subject that I'm just entirely ignorant of. Does anyone have pointers?


Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

You can read Bart Jacobs'

You can read Bart Jacobs' PhD thesis. He's the author of that book. I also highly recommend the Prospectus for the book here. It gives an overview of the various parts and is relatively readable. The thesis is very difficult to read.

Andrew Pitts Categorical Logic is probably also useful but not directly related.

Googling for "categorical semantics" and "polymorphic lambda calculus" should turn up plenty of papers to look through.

That was the problem!

Believe it or not, but searching for "categorical semantics" and "polymorphic lambda calculus" works orders of magnitude better than "categorical semantics" and "system f".

Thanks, Derek.