What we will study about types ·Type system Typing rules:assign types to terms Type safety(soundness of typing rules):well-typed terms cannot go wrong Connection to constructive propositional logic ·Curry-Howard isomorphism:“Propositions are Types'”, “Proofs are Programs" What we will study about types • Type system • Typing rules: assign types to terms • Type safety (soundness of typing rules): well-typed terms cannot go wrong • Connection to constructive propositional logic • Curry-Howard isomorphism: “Propositions are Types”, “Proofs are Programs