Fall 93 Lecture Notes

• Does this course appropriate for you? ( by V. Divakar )
  Is CS611 the Right Course for You? - Outline - Motivation
• Lecture 1 ( by David Karr )
  Organization and Administration - Course Sections - Motivation & Goals
• Lecture 2 ( by Mike Smyth )
  Programming Languages in the Context of CS - Experimental Science - Case Study of an Experiment - Math Preliminaries
• Lecture 3 ( by Jason Hickey )
  Review of Definitions of Natural Numbers - Primitive Recursion on N - Algebraic Account of the Integers - Summary and Relation to Programming Paradigms - Set vs Types - Coming Attractions
• Lectures 4, 5, and 6 ( by Professor Constable )
  An Introduction to Naive Type Theory
• Lecture 7 ( by Takako M. Hickey )
  More on Set Theory - lambda-calculus
• Lecture 8 ( by Sophia Georgiakaki )
  Background Remarks - Notation for lambda-terms - Inductive definition of the lambda terms - Lambda term primitive recursion - Equality - Subterms - Inductive reasoning - Intuitive meaning of lambda-calculus - Coming Attractions
• Lecture 9 ( by Stef Lucas )
  Lambda-Calculus as Rules for Functions - The lambda-calculus Notation - Alternative Definition of lambda Terms - Scribe's Notes
• Lecture 10 ( by Edward Wang and Kodukula Induprakas )
  Binding - Free variables - Substitution - Binding Structure and Substitution Continued (Discussion) - Binding Structure
  • Supplement ( by Paola Nieddu )
    Alternative definition of alpha-equality - Relating substitution to alpha-equality
• Lecture 11 ( by Craig Lewis )
  Operational Semantics - Eager Evaluation
• Lecture 12( by Vladimir Kotlyar )
  Plan - Combinators as values - Example - Semantic Theorem 1
  • Supplement ( by Marcel Rose )
• Lecture 13( by Divakar Viswanath )
  Review - The Reduction Method
• Lecture 14( by Peter Kopke )
  Definition - Theorem
• Lecture 15( by Kenji Saito )
  Heart of Pure Lisp - Syntax - Semantics
• Lecture 16( by Professor Constable )
  Semantic Equivalence
• Lecture 17( by Max Forester )
  Typed Lambda Calculus
  • Supplement ( by Alan Wenban )
    Typing Derivations - Examples
• Lecture 18( by James Durkin )
  More on Typing Derivations - Connections to the Computation System
• Lecture 19( by Katherine Guo and Donald Wihardja )
  Adding Cartesian Product - Disjoint Union
• Lecture 20 ( by Takako M. Hickey )
  Recursive Types - Definition of ind using rec_ind - Dependent Types and the lambda calculus
• Lecture 21( by David Bau and Rick Aaron )
  Logic and Reasoning About Programs
• Lecture 22( by Christother Suley, Donald Wihardjha, and Jason Hickey)
  Carry-Howard Isomorphism - Semantics - Further Extensions - Conjunction and Cartesian Products - Constructive "or" and Disjoint Union - Semantics - Quantifiers - Notation Summary
• Lecture 23 ( by David Sturgill, Roderick Moten, and John O'Leary)
  Arithmetic in Types Theory - I Type as Atomic Propositions - Logic and Type Theory - Induction (a review) - Type reduction rule - Semantics - Proof of Program Correctness Over N - Discussion of Example - Conclusion
• Lecture 24( by Stuart Allen)
  Semantics of Imperative Sequential Lanquages
• Lecture 25( by Stef Lucas and Vladimir Kotlyar)
  Partial Computable Functions
• Lecture 26( by Divakar Viswanath and Funda Ergun )
  Domain Theory - CPO Semantics for PCF - Appendix