Stream: Miscellaneous

Topic: Content about System F (Polymorphic Lambda Calculus))

view this post on Zulip Gabriel Mazieri (Jan 29 2023 at 16:29):

Hello again, I'm struggling to find kind of a beginner friendly content about System F, does anyone know any System F content to share with me? I'm also wanting to implement an interpreter of System F with OCaml later, that's why I'm asking for content. And of course I'll write articles about what I've learned.

view this post on Zulip Karl Palmskog (Jan 29 2023 at 16:48):

there are tons of formalizations of System Fsub out there, since it was part of POPLMark. Two examples: https://github.com/plclub/metalib (Fsub directory) and https://github.com/coq-community/autosubst (POPLmark.v in examples directory)

view this post on Zulip Ali Caglayan (Jan 29 2023 at 16:49):

If you want a book explaining System F and related things I can recommend "Lecutres on the Curry-Howard Isomorphism" by Sorensen and Urzyczyn.

view this post on Zulip Paolo Giarrusso (Jan 29 2023 at 17:31):

Let me add two book recommendations: Benjamin Pierce's "Types and Programming Languages" and Robert Harper's "Practical Foundations for Programming Languages" (full "preview" version from the author: https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf)

view this post on Zulip Paolo Giarrusso (Jan 29 2023 at 17:33):

For a beginner, I'd probably recommend learning about simply-typed lambda calculus first, and that's also covered by Software Foundations in Coq

view this post on Zulip Patrick Nicodemus (Jan 29 2023 at 18:10):

system F is also described in "Proofs and Types" by Girard.

view this post on Zulip Paolo Giarrusso (Jan 29 2023 at 20:32):

True; but would you rank that as "beginner-friendly"? Personally I wouldn't.

view this post on Zulip Gabriel Mazieri (Jan 30 2023 at 12:09):

@Paolo Giarrusso With Software Foundation you mean the Logical Foundation Course in Coq?

view this post on Zulip Ali Caglayan (Jan 30 2023 at 12:59):

This one: https://softwarefoundations.cis.upenn.edu/

view this post on Zulip Paolo Giarrusso (Jan 30 2023 at 13:02):

Yep thanks! Lots of relevant content is in volume 2; Logical Foundations is just volume 1.

view this post on Zulip Patrick Nicodemus (Feb 01 2023 at 02:57):

Paolo Giarrusso said:

True; but would you rank that as "beginner-friendly"? Personally I wouldn't.

I do. I found it accessible as a beginner. But it is a matter of taste. It also depends on the background - a beginner may have knowledge in adjacent areas which is transferable.
I second the recommendation of "Lectures on the Curry Howard Isomorphism."

Last updated: Apr 18 2024 at 14:02 UTC