Why formal type systems Many typed languages have informal descriptions of the type systems (e.g.,in language reference manuals) A fair amount of careful analysis is required to avoid false claims of type safety A formal presentation of a type system is a precise specification of the type checker And allows formal proofs of type safety
Why formal type systems • Many typed languages have informal descriptions of the type systems (e.g., in language reference manuals) • A fair amount of careful analysis is required to avoid false claims of type safety • A formal presentation of a type system is a precise specification of the type checker • And allows formal proofs of type safety
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
Simply-typed A-calculus(STLC) base type (e.g.int,bool) function type (Types)t,o=T|o→t An infinite number of types: int-→int,int→(int→int),(int->int)>int, →is right-associative:t→t→tist→(t→t)
Simply-typed -calculus (STLC) (Types) , ::= T | → base type (e.g. int, bool) function type An infinite number of types: int → int, int → (int → int), (int → int) → int, … → is right-associative: → → is → ( → )
Simply-typed A-calculus(STLC) (Types)t,o=T|o→t (Terms)M,N ::xx t.M MN
Simply-typed -calculus (STLC) (Terms) M, N ::= x | x : . M | M N (Types) , ::= T | →
Reduction rules (x:t.M)N→M[N/x] (β) M→M' MN→M'N Same as untyped A-calculus N→N' MN→MN' M→M' X:t.M→λx:t.M1
Reduction rules λ𝑥: 𝜏. 𝑀 𝑁 → 𝑀[𝑁/𝑥] 𝑀 → 𝑀′ 𝑀 𝑁 → 𝑀′𝑁 𝑀 → 𝑀′ λ𝑥: 𝜏. 𝑀 → λ𝑥: 𝜏. 𝑀′ 𝑁 → 𝑁′ 𝑀 𝑁 → 𝑀 𝑁′ Same as untyped -calculus ()