[TAPL] Lecture 1. Introduction

Ch.1. Introduction

1.1 Types in Computer Science

Formal methods (정형기법) in software engineering

  1. Some powerful frameworks:
    • hoare logic, algebraic specification languages, modal logics, denotational semantics
  2. 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.


Leave a Reply

Your email address will not be published. Required fields are marked *