OCaml Programming: Correct + Efficient + Beautiful

A textbook on functional programming and data structures in OCaml, with an emphasis on semantics and software engineering. This book is the textbook for CS 3110 Data Structures and Functional Programming at Cornell University. A past title of this book was “Functional Programming in OCaml”.

Syllabus

PREFACE

About This Book
Installing OCaml

INTRODUCTION

1. Better Programming Through OCaml
- 1.1. The Past of OCaml
- 1.2. The Present of OCaml
- 1.3. Look to Your Future
- 1.4. A Brief History of CS 3110
- 1.5. Summary
2. The Basics of OCaml
- 2.1. The OCaml Toplevel
- 2.2. Compiling OCaml Programs
- 2.3. Expressions
- 2.4. Functions
- 2.5. Documentation
- 2.6. Printing
- 2.7. Debugging
- 2.8. Summary
- 2.9. Exercises

OCAML PROGRAMMING

3. Data and Types
- 3.1. Lists
- 3.2. Variants
- 3.3. Unit Testing with OUnit
- 3.4. Records and Tuples
- 3.5. Advanced Pattern Matching
- 3.6. Type Synonyms
- 3.7. Options
- 3.8. Association Lists
- 3.9. Algebraic Data Types
- 3.10. Exceptions
- 3.11. Example: Trees
- 3.12. Example: Natural Numbers
- 3.13. Summary
- 3.14. Exercises
4. Higher-Order Programming
- 4.1. Higher-Order Functions
- 4.2. Map
- 4.3. Filter
- 4.4. Fold
- 4.5. Beyond Lists
- 4.6. Pipelining
- 4.7. Currying
- 4.8. Summary
- 4.9. Exercises
5. Modular Programming
- 5.1. Module Systems
- 5.2. Modules
- 5.3. Modules and the Toplevel
- 5.4. Encapsulation
- 5.5. Compilation Units
- 5.6. Functional Data Structures
- 5.7. Module Type Constraints
- 5.8. Includes
- 5.9. Functors
- 5.10. Summary
- 5.11. Exercises

CORRECTNESS AND EFFICIENCY

6. Correctness
- 6.1. Specifications
- 6.2. Function Documentation
- 6.3. Module Documentation
- 6.4. Testing and Debugging
- 6.5. Black-box and Glass-box Testing
- 6.6. Randomized Testing with QCheck
- 6.7. Proving Correctness
- 6.8. Structural Induction
- 6.9. Algebraic Specification
- 6.10. Summary
- 6.11. Exercises
7. Mutability
- 7.1. Refs
- 7.2. Mutable Fields
- 7.3. Arrays and Loops
- 7.4. Summary
- 7.5. Exercises
8. Data Structures
- 8.1. Hash Tables
- 8.2. Amortized Analysis
- 8.3. Red-Black Trees
- 8.4. Sequences
- 8.5. Memoization
- 8.6. Promises
- 8.7. Monads
- 8.8. Summary
- 8.9. Exercises

LANGUAGE IMPLEMENTATION

9. Interpreters
- 9.1. Example: Calculator
- 9.2. Parsing
- 9.3. Substitution Model
- 9.4. Environment Model
- 9.5. Type Checking
- 9.6. Type Inference
- 9.7. Summary
- 9.8. Exercises

LAGNIAPPE

The Curry-Howard Correspondence

APPENDIX

Big-Oh Notation
Virtual Machine

Taught by

Michael R. Clarkson, Robert L. Constable, Nate Foster, Michael D. George, Dan Grossman, Daniel P. Huttenlocher, Dexter Kozen, Greg Morrisett, Andrew C. Myers, Radu Rugina, and Ramin Zabih