CPSC 629: Deductive Systems

 

Instructor: Carsten Schürmann
Department of Computer Science
Yale University
Time: TTh 4:00-5:15
Room: AKW 500

  Home
  Schedule
  Handouts
  Assignments
  Projects
  Links
 
  

Projects

The project should consist of a term paper and an implementation in Elf. The term paper should summarize and explain a piece of research in the theory of programming languages or logics. Typically, the informal development follows a given research paper or report. The Twelf implementation should formalize the language, judgments, algorithms, and metatheory to the extent that this is feasible for a term project. Each student should propose his or her own term project. Some topics are suggested below, but they should not be considered as canonical or exhaustive.
  1. A calculus of explicit substitutions [Abadi, Cardelli, Curien, & Levy 91]
  2. A calculus of objects [Abadi & Cardelli 94]
  3. Coherence of a language with subtyping and implicit coercions [Breazu-Tannen, Coquand, Gunter, & Scedrov 91]
  4. A lambda-calculus with intersection types [Coppo, Dezani-Ciancaglini, & Venneri 81] [Reynolds 91]
  5. A logic for parametricity [Plotkin & Abadi 93]
  6. A lambda-calculus with names [Odersky 94]
  7. First-order unification [Snyder & Gallier 88]
  8. Higher-order logic programming [Miller, Nadathur, Pfenning, & Scedrov 91]
  9. Program analysis and optimization
    1. Binding-time analysis [Nielson & Nielson 92] [Davies & Pfenning 96] [Davies 96] [Hatcliff 96]
    2. Abstract interpretation [Cousot & Cousot 77]
    3. Strictness analysis [Hankin & Metayer 94]
  10. The Categorical Abstract Machine [Cousineau, Curien, & Mauny 87]
  11. Closure conversion and lambda-lifting [Reynolds 72]
  12. Extending Mini-ML (each topic below is a possible separate project)
    1. with exceptions
    2. with references
    3. with general datatype definitions
    4. overloading and typecase
  13. Mini-Forsythe [Reynolds 88]
  14. Elementary notions of rewrite systems [Bachmair 91]
  15. Modal logic and Kripke semantics [Basin, Matthews, Vigano 96]
  16. Polymorphic recursion and semi-unification [Henglein 93, TOPLAS]
  17. Lazy evaluation [Launchbury 93]
  18. Pure functional programming and monads [Filinski 94]
  19. Evaluation based on evaluation contexts [Felleisen]
  20. Logical interpretations [Goedel, Friedman]
  21. Linear logic [Girard 87, Pfenning 96]
  22. Computational interpretations of classical logic [Ong 96, Ong & Stewart 97]
  23. Pi-calculus [Milner]
  24. Theorem proving
    1. via tactics
    2. via iterative deepening
    3. other methods
    4. induction
    5. Presburger arithmetic
    6. decision procedures for fragments
  25. Elementary category theory [Rydeheard & Burstall, Gehrke]
  26. Type-directed compilation [Morrisett 95]
  27. Shape types [Fradet & Metayer 97]
  28. Relational parametricity and units of measure [Kennedy 97]
  29. Type directed partial evaluation [Danvy 96]
  30. Typed closure conversion [Minamide, Morrisett, Harper 96]
  31. Call-by-value lambda-calculus [Plotkin 75, Sabry & Wadler 96]
  32. Call-by-need lambda-calculus [Ariola et al 95]
  33. Recursive types [Abadi & Fiore 96]
  34. ``Logical'' logic program compilation [Pfenning 97]
  35. LF in Twelf
  36. Twelf in Twelf
  37. Intensional type analysis [Harper, Morrisett 95]