CPSC 415: Special Topics in Computer Science, Fall 1998: Logic and Computation

Class Time: Wed 6:45-9:15pm
Location: MCEC 220

Chuck C. Liang
Office: MCEC 343
Office Phone: (860 297) 5395
Designated Office Hours: Monday-Thursday 3-4pm, or by appointment
Email: chuck.liang@mail.trincoll.edu

Course Description:

This course is designed to introduce undergraduate students to some advanced topics in logic and computation that are typically studied at the graduate level. These topics include algebraic structures, term rewriting and unification, formal proof systems, higher order and intuitionistic logic, automated theorem proving, type theory and principles of declarative programming languages. Potential applications of these topics include formal specification of hardware and software, programming language design and implementation, deductive databases, and various subjects in artificial intelligence. It should be emphasized that the course will be taught at a very advanced and theoretical level. Students are expected to be self motivated. Course work may involve, in addition to assignments and quizes, writing of technical papers critically summarizing certain results, class presentations, and independent research. There may also be some short programming assignments.
Prerequisite: CPSC 203 or Math 205.

Reference Material: There is no official textbook. Reading will consist of various handouts.


Class Web Page: http://www2.trincoll.edu/~cliang/c415/


Tentative List of Topics:

  1. Overview and review of basic discrete math topics
  2. First Order Symbolic Systems:
    1. Abstract algebraic structures and properties
    2. Orderings and Latices
    3. Term Algebras, term trees
    4. Substitution and Unification
    5. Term Rewriting Systems
  3. Logic and Proof Theory
    1. The Sequent Calculus
    2. Classical v.s. Intuitionistic logic
    3. Cut Elminination and Proof Search
    4. An Abstract Logic Programming interpreter
  4. Higher Order Logic and Type Theory:
    1. The Lambda Calculus
    2. Termination and Confluence: The Church-Rosser Theorem
    3. Type systems
    4. Lambda Terms and Functional Programming
    5. Higher Order unification and rewriting
    6. Higher Order Abstract Syntax
  5. Additional Topics (if time allow:)
    1. The ML programming language
    2. Dependent Types
    3. The Lambda Prolog programming language

Exams, Assignments and Grading

There will be some written assignments and projects. There will be two 30-minute quizes and either a final exam or a final project. The final projects will likely involve writing a paper. The grade distribution will be roughly as follows: quizes and exams 40%, assignments and projects 60%.

All material handed in must be in hard copy, and be well organized and legible. Unreadable material will not be graded. Consultation of outside material for completion of assignments must be pre-approved. Late assignments will not be accepted.

Attendance

Regular attendence is expected. Students are responsible for all material, in all forms, presented during scheduled class times.

Final Note: The contents of the this syllabus may be modified according to the progress of the course