Course Outline

1. Background from general computability theory.
   
   
   1. A review of basic recursion theory.
      Sources: Class notes, part 1; Odifreddi, Chapter I; and Rogers, Chapter 1.
      
      
   2. Basic properties of r.e. sets, m-reductions and T-reductions.
      Class notes, part 2; Odifreddi, Sections II.1, II.2, and III.3; and Rogers, Chapters 2, 5, 6, 7, and 9.
      
      
   3. Standard sorts of functionals and operators from classical recursion theory and their basic properties.
      Sources: Odifreddi, Section II.3; Rogers, Chapter 9 and Sections 11.5 and 15.3.
      
      
   4. The Rice-Shapiro, Myhill-Shepherdson, and Kreisel-Lacombe-Shoenfield Theorems. Friedberg's counter-example.
      Sources: Class notes, part 3; Odifreddi, Section II.4; Rogers Sections 11.5 and 15.3. Also see my note on obtaining the MS and KLS theorems by almost the same proof.
      
      
   5. A very quick survey of extentions of computability theory beyond type-2 and what might possess someone to do do such a thing.
      Sources: Sections of Cook, Gandy & Hyland, and Odifreddi.
      
      
2. The simple types and the simply typed lambda calculus.
   
   
   1. Basics of the simply typed lambda calculus.
      Sources: Gunter Chapter 2.
      
      
   2. Computational aspects of the simply typed lambda calculus.
      Sources: Mairson and Schwichtenberg.
      
      
   3. The partial and total continuous functionals of simple type and their effective versions.
      Sources: Hyland, Schwichtenberg, and Scott. Also see Schwichtenberg's type theory notes.
      
      
   4. A very quick look at some other type systems.
      Sources: Gunter's survey (perhaps).
      
      
3. Background from complexity theory
   
   
   1. A quick review of bread and butter complexity theory.
      Sources: Papadimtriou (perhaps).
      
      
   2. Common sorts of functionals and operators used in complexity theory.
      Sources: Papadimtriou (perhaps).
      
      
   3. Characterizations of polynomial time.
      Sources Bellantoni & Cook, Cobham, and Leivant.
      
      
4. Analogs of polynomial time at type-2 and the simple types
   
   
   1. The type-2 Basic Feasible Functionals and their various characterizations.
      Sources: Cook, Cook & Kapron, Kapron & Cook, Royer, and Seth.
      
      
   2. Requirements for type-2 ``feasibility.''
      Sources: Cook, Cook & Kapron, Kapron & Cook, and Seth.
      
      
   3. Feasibility at type-3 and beyond.
      Sources: Cook, Cook & Kapron, Kapron & Cook, Royer, and Seth.
      
      
5. Other topics.
   These will be as interest, time, and energy allow.
   Possibilities include:
   
   
   1. Higher-types via associates.
   2. General type-2 complexity.
   3. Computability and complexity in non-simple types.
   4. Applications to proof theory.

Back to the course homepage