type safety propositions as types System F Resources Books Practical Foundations for Programming Languages Types and Programming Languages Related logic