- Programming & Computing; Information & Data
- How to Design Functions & Programs
- From Fixed-size Data to Large Data
- Designing Functions For Arbitrarily Large Data
- Design With Abstraction
- General Design With Arbitrarily Large Data
- Iterative Refinement
- Designing With Generative Recursion
- Designing With Accumulators
- Design Review
- What is a Programming Language
- Creating Programming Languages I
- Creating Programming Languages II

- Lecture 1: Data Definitions in Java
- Lecture 2: Data Definitions: Unions
- Lecture 3: Methods for simple classes
- Lecture 4: Methods for unions
- Lecture 5: Methods for self-referential lists
- Lecture 6: Accumulator methods
- Lecture 7: Accumulator methods, continued
- Lecture 8: Practice Design
- Lecture 9: Abstract classes and inheritance
- Lecture 10: Customizing constructors for correctness and convenience
- Lecture 11: Defining sameness for complex data, part 1
- Lecture 12: Defining sameness for complex data, part 2
- Lecture 13: Abstracting over behavior
- Lecture 14: Abstractions over more than one argument
- Lecture 15: Abstracting over types
- Lecture 16: Visitors
- Lecture 17: Mutation
- Lecture 18: Mutation inside structures
- Lecture 19: Mutation, aliasing and testing
- Lecture 20: Mutable data structures
- Lecture 21: ArrayLists
- Lecture 22: ArrayLists
- Lecture 23: For-each loops and Counted-for loops
- Lecture 24: While loops
- Lecture 25: Iterator and Iterable
- Lecture 26: Hashing and Equality
- Lecture 27: Introduction to Big-O Analysis
- Lecture 28: Quicksort and Mergesort
- Lecture 29: Priority Queues and Heapsort
- Lecture 30: Breadth-first search and Depth-first search on graphs
- Lecture 31: Dijkstra’s Algorithm for single-source shortest paths
- Lecture 34: Implementing Objects

- Introductions & motivation,
- Syllabus, class webpage, programming review,
- Designing data-driven programs, the ACL2s development environment,
- Basic data types, expressions, syntax & semantics of atomic data and associated primitive functions,
- Syntax & semantics of lists, design considerations of the ACL2s core language, contracts, termination
- helpful function, quote, let, Datatypes: enumerated, range, product, record, union, list, (mutually) recursive
- Property-based testing, test?, thm, design recipe, program mode and defunc settings
- Property-based testing in industry, Fuzzing, security applications
- Boolean logic, characterization of formulas, introduction to P=NP, Security: one-time pads,
- Properties of Boolean operators, Proof methods: instantiation, case analysis, equational proofs, truth tables, decision procedures,
- Normal forms, Boolean logic in ACL2s, applications,
- Limitations of Boolean logic, intro to equational reasoning for programs,
- Axioms for equality, cons-first-rest axioms, definitional axioms, instantiation, contract checking and completion,
- Equational reasoning in the presences of implications, context vs. theorems, undecidability results,
- Reasoning about arithmetic, program equivalence: proving correctness of an exponential-time improvement, numeric reasoning in C & other languages
- Equational reasoning with nested Boolean operators, derived context, how to prove theorems
- The equational reasoning recipe and examples,
- Definitions: soundness, termination, contracts, the ACL2s Definitional Principle
- Termination, measure functions, Review
- Using termination to show soundness of common recursions schemes and the design recipe, big-Oh analysis as a refinement of termination
- Undecidability of halting problem
- Proof by contradiction, mathematical induction, well-foundnesses, a proof that mathematical induction works, how to extract induction schemes - from admissible recursive functions
- Using induction to prove program correctness
- Data-function-induction trinity, Importance of termination
- Induction like a professional, reasoning about algorithms: sorting, correctness
- Generalization, lemma generation, dealing with induction failure
- Intro to reasoning about accumulators
- Tail recursion: efficiency considerations, how to prove correctness
- Accumulator reasoning examples
- Abstract and algebraic data types
- Observational equivalence
- Reasoning about imperative programs: defining the semantics of a simple while language in ACL2s
- Reasoning about imperative programs using loop invariants; checking such proofs in ACL2s
- Reasoning about imperative programs and security
- Compiler correctness, exam2 review
- Compiler correctness
- Mathematical logic: syntax, semantics, proof theory, undecidability, incompleteness
- A look back: Logic and the birth of computer science; A look forward: what’s next

- Introduction to C++
- Control flow
- I/O and streams
- Data types
- Functions
- Debugging Tools
- Analysis Tools
- Structs and Enums
- Data structures
- STL containers and iterators
- STL algorithms
- Exceptions
- Classes
- Inheritance and Polymorphism
- Operator Overloading
- Memory and pointers
- Smart pointers
- Templates
- Unit Testing
- Processes and threads

- Thu Intro
- Lexers
- Parsing LL
- Parsing LL
- Parsing LR
- Parsing LR
- Parsing ML-Yacc
- Symbol tables
- Semantic analysis
- Semantic analysis
- Stack layout & procedure linkage 1
- Stack layout & procedure linkage 2
- Translating to an IR 1: expressions, booleans for val & control
- Translating to an IR 2: control structures, functions
- Translating to an IR 3: compound data (records & arrays)
- Generating basic blocks
- Instruction selection: maximal munch, BURG, insn grammars
- Data-flow analysis 1, Liveness
- Register allocation 1
- Register allocation 2
- Data-flow analysis 2
- TBD (GC, etc.)
- TBD (GC, etc.)
- TBD (GC, etc.)

- Introduction to PL and to Racket
- Grammars, BNF, Typed Racket, Simple Parsing, The AE Language
- Semantics: Implementing an Evaluator for AE, Intro to Typed Racket
- The need For Bindings, Bindings & Substitution, The WAE Language, Formal Specs
- Lazy vs Eager, de Bruijn Indexes, First Class Functions, Implementing FLANG
- More on Implementing First-Class Functions, Racket Functions: lambda
- “Point-Free” Programming, Substitution Caches, Dynamic vs Lexical Scope
- Implementing Lexical Scope: Closures and Environments, More Closures
- Types of Evaluators, Feature Embedding, Recursion without the Magic, the Y Combinator
- The Property of Y, Typing Y, Minimal Language: Lambda Calculus
- Lambda Calculus cont., Alternative Encoding
- Recursive Binder: letrec, Implementing Recursion using letrec, Boxes and Mutation
- rec Using a Cyclic Structure, Variable Mutation, State and Environments, Implementing Objects
- Toy, “Compilation” and Partial Evaluation
- Compilation contd, Lazy evaluation in Racket
- Lazy Programming, Call by Need vs by Name
- Implementing Laziness, Sloth, Implementing Call by Need, Side Effects in a Lazy Language
- Designing DSLs
- Syntax Transformations: Macros, Macro Problems, Racket Macros, Implementing Laziness in Racket
- Recursive Macros, Low Level Macros
- Types, What are Types?, The Picky Language, Typing Control
- Implementing Picky, Recursion, Data
- Type Soundness, Polymorphism
- Web Programming, Introduction to Continuations, Transforming Code
- Automatic Continuation Converter, Continuations as a Language Feature
- Continuation in Racket, Implementing New Features with Continuations

- Intro: Systems; C and ASM
- AMD64 Assembly; ASM: “Design Recipe” - HW01: Linux Setup & Hello Worlds
- Large ASM Example; ASM: Syscalls, I/O, the heap - HW02: ASM, Pointers, Funs
- Processes & Memory; C: Arrays & Pointers - HW03: ASM Sort
- C: Complex Data Structures; A Simple Tokenizer - HW04: C Data Structures
- Syscalls: fork, exec, waitpid; Building a Shell & pipe - HW05: Shell Tokenizer
- read, write, proc table, vmem; shared mem & data races - CH1: Unix Shell
- semaphore locks & deadlock; threads and mutexes - HW06: Parallel Sort (Processes)
- cond vars and atomics; malloc: free lists - HW07: Parallel Sort (Threads)
- malloc: optimizations & threads; Concurrency solutions - HW08: Simple Memory Allocator
- OS Kernels; Looking at xv6 - CH2: Advanced Memory Allocator
- File Systems: FAT; File Systems: ext - HW09: Examining xv6
- The FUSE API - HW10: Simple FS
- Wrap Up - CH3: Advanced FS

- Why object-oriented design?
- The essence of objects
- Java review
- Java safari
- Java safari (part 2)
- Version control with Git
- Git explanation tutorial and Interactive tutorial
- Introducing the Model, and the Builder pattern
- Controllers and Mocks;
- Class Activity: abstracting I/O
- Design critique: testing, toString, Pile abstractions, I/O
- Encapsulation and Invariants
- Design exercise: Turtles
- Inheritance vs. composition
- Intro to Performance
- More performance
- Class activity: GUI basics
- MVC code, starter code and code
- GUI basics contd., Design critique: animation models
- MVC code, starter code and code
- The Adapter pattern
- The strategy and decorator patterns
- Class activity: Strategic Solitaire
- Case study: Interpreters
- Case study: Interpreters
- Exam review
- Introduction to JavaScript
- JavaScript
- Introduction to JavaScript

- Introduction
- BigO
- Design
- Java
- Graphs
- Greedy
- Greedy2
- Compression
- DandC1
- DandC2
- RDandC
- Randomized
- DynamicP
- DynamicP1_5
- DynamicP2
- NetworkFlow1
- NetworkFlow2
- Amortized
- Trees
- Heaps
- NPC
- Workarounds
- HarderStuff
- Final Review
- AI