Early morning thoughts... maybe wolfram's right about SK in combinatory logic being the ideal basis of proofs involving the lambda calculus.
& if so, maybe work on polymorphic type systems would be better served beginning there, rather than thru the lens of process calculi, kleisli, monads, etc
