“Types and Programming Languages” by Benjamin Pierce is a good textbook for learning about
typesystems in general (both theory and implementation). While it doesn’t cover dependent types in
detail (it only goes as far as F_Omega in that direction), it provides a solid background for
further reading.
Software Foundations in particular looks highly apposite, and in a useful format, to boot.
TaPL was indeed one of the books I was considering reading. (Hesitating between that and Lambda Calculus and Combinators: an Introduction.) Gave it another point in my mental ranking.
Based on the little I understood of MIRI’s papers (the first of which also prompted me to read their paper on Vingean Reflection), they seem interesting, but currently inaccessible to me. Added an edit/update to my post.
“Types and Programming Languages” by Benjamin Pierce is a good textbook for learning about typesystems in general (both theory and implementation). While it doesn’t cover dependent types in detail (it only goes as far as F_Omega in that direction), it provides a solid background for further reading.
“Software Foundations” (available at https://softwarefoundations.cis.upenn.edu/) is about proving programs correct in Coq (with embeddings of various Hoare logics). VST (https://vst.cs.princeton.edu/) shows that the methodology in Software Foundation extends to proving properties about actual C programs.
MIRI’s papers “Proof-Producing Reflection for HOL” (https://intelligence.org/files/ProofProducingReflection.pdf) and “Definability of Truth in Probabilistic Logic” (https://intelligence.org/files/DefinabilityTruthDraft.pdf) are partial positive results on side-stepping some problems of self-reference in formal logic (the former via stratification of the logic, the latter via generalizing truth values to probabilities).
Thanks for the suggestions!
Software Foundations in particular looks highly apposite, and in a useful format, to boot.
TaPL was indeed one of the books I was considering reading. (Hesitating between that and Lambda Calculus and Combinators: an Introduction.) Gave it another point in my mental ranking.
Based on the little I understood of MIRI’s papers (the first of which also prompted me to read their paper on Vingean Reflection), they seem interesting, but currently inaccessible to me. Added an edit/update to my post.