let's look at Programing Language Theory (PLT) according to wiki, an outline
alanzo's chruch and kleene's lambda calculus noam chomsky's hierarchy landin secd machine and it's relation to lambda calculus landin j operator (for continuations) landin iswim strachey introduces terms parametric and ad hoc polymorphism hoare's hoare logic (a form of axiomatic semantics) howards's natural deduction -> curry-howard correspondence scott's deontational semantics logic programming (proog) reynolds and girards (system F) sussman and Steele's scheme language milner's hindley miler type inference algoirthm plotkin (structured operational semantics) kahn (natural semantics) kay's smalltalk process calculi lazy evaluation moggi and wadler's monads
subfields formal semantics type theory program analysis & transformation generic & meta programming domain specific languages compiler construction
outline
lambda calculus
operational semantics (good lead into compiler construction?)
axiomatic semantics -hoare logic +loop invariant +forward vs backward assignment
denotational semantics -fixed points
first order logic and model theory -logic programming -horn clause -herbrand model
maybe these different types relate to different programming paradigms hoare logic for imperative? herbrand for logic? dentotational for functional? ? for object oriented?