• Lecturer: 穆信成 Shin-Cheng Mu

• Slides and handouts.
• Exercises
  • Exercise 0
  • Exercise 1 (Utils.ml), with solutions.
  • Exercise 2 (Caesar.ml), with completed code.
  • Exercise 3, with solutions.
  • Exercise 4, with solutions.

• 作業請寄給助教 jaiyalas(at)iis.sinica.edu.tw ，或是當面交給助教。

Part 1. Functions, Values, and Evaluation

• Values and Evaluation
  • Talking to the Interpreter
  • Evaluation and Termination
• Functions
  • Currying
  • Sectioning
  • Definitions
• Types – A Brief Start

Part 2. Induction on Datatypes

• User Defined Types
• Induction on Natural Numbers
  • Datatypes, Functions, and Proofs
  • What is a Proof, Anyway?
• Induction on Lists
  • Append, and Some of Its Properties
  • More Inductively Defined Functions
  • Other Patterns of Induction

Part 3. Simple Functional Data Structures

• On Efficiency of Operations on Lists
• Batched Queue
• Binary Search Tree

Part 4. Program Calculation

• The Unfold/Fold Transformation
  • Example: Sum of Squares
• Accumulating Parameters
  • Fast List Reversal
  • Tail Recursion and Loops
  • Being Quicker by Doing More!
  • Proof by Strengthening
• Tupling