Ch.1. Introduction
1.1 Types in Computer Science
Formal methods (정형기법) in software engineering
- Some powerful frameworks:
- hoare logic, algebraic specification languages, modal logics, denotational semantics
- Lightweight formal methods:
- model checkers, run-time monitoring, type systems
Type system
- a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute
Type system (or type theory)
- A much broader field of study in logic, mathematics, philosophy, and computer science
- Firstly formalized in the early 1900s as ways of avoiding the logical paradoxes, such as Russel's (러셀의 패러독스)
Type systems within computer science
- Applications to programming languages (The topic of this lecture!!)
- Connections between programs and logics via the Curry-Howard correspondence (Ch.9)
Type systems in the perspective of applications to programming languages
- A type system can be regarded as calculating a kind of static approximation to the certain run-time behaviors of the terms in a program.
- static approximation : compile-time analysis
- (bad) run-time behaviors : runtime type errors, modularity
- the safety (or soundness) property of a type system
- Type checking vs. type inference
1.2 What Type Systems Are Good For
- Detecting errors
- Abstraction (e.g., module interfaces)
- Documentation
- Language safety
- Efficiency
- and more
- proof-carrying code
- automated theorem proving : Coq
- XML/JSON type systems in database community
1.3 Type Systems and Language Design
Programming language design go hand in hand with type-system design
- The type system itself is often taken as the foundation of the design and the organizing principle in typed programming languages.
Trade-off between explicit type annotation vs. automatic type inference
1.4 Capsule History
Refer to the textbook.