Denotational semantics Equational reasoning Program derivation Category theory The Curry–Howard isomorphism fix and recursion
