The University of Western Ontario
Department of Computer Science

CS 849b --- Logical Foundations of Programming Languages

Course Outline -- Winter 2006

Course Description

For over 35 years, computer scientists have been slowly moving toward the goal of being able to mathematically prove properties of programs. For this, they have needed programming language semantics -- precise mathematical descriptions of what the syntactic constructs in a programming language are supposed to mean. Once we have such descriptions, we can associate each program with a mathematical structure such as an input/output relation, and then prove properties of those structures.

I believe that one of the things that has hindered progress towards proofs of properties of programs is that programming language semantics are traditionally based on lattice theory, not on logic. This has required us to define program-proving systems in separate logics and relate them to the semantics through complex theorems.

This course, based on a book that I am writing, gives a different view. Starting with symbolic logic and proof systems, it gives a logical foundation for logic, functional, imperative, and object-oriented programming languages, unifying and simplifying the semantics of all these forms of languages.

Students will gain an understanting of the mathematical structures used to characterize programming languages, such as symbolic logic, structured operational semantics, and the lambda-calculus. They will also gain an understanding of the relationships between the execution models of the various forms of programming languages.

Prerequisites

• Undergraduate (3rd-year) discrete structures and logic.

Instructor

• Prof. J. H. (Jamie) Andrews.
• Office: Middlesex College (MC) room 365.
• E-mail: andrews (at) csd [dot] uwo (dot) ca

Course Details

Textbook

Course Website

http://www.csd.uwo.ca/faculty/andrews/courses/849 (under construction)

Student Evaluation

• There will be four smaller written assignments, each worth 15% of the final grade.
• There will be one larger written assignment at the end, worth 40% of the final grade.
• If an assignment has to be cancelled for any reason, the remaining assignment marks will be prorated to add up to 100%.

Every effort will be made to have assignments marked and handed back within 2 weeks of the hand-in date.

Topics (with approximate dates)

• Week 1: Overview. First order logic. First order languages. Constants, constructors and lists. Proofs with =, &, or, \exists. Predicate definitions and programs.
• Week 2: Computing logical formulas. Computation results. Formulas with just =, \exists, constants and variables. Adding &. Closures.
• Week 3: Adding constructor symbols. Unification. Adding "or". Backtracking. Soundness of computation.
• Week 4: Positive and negative soundness. Completeness: definition. Incompleteness of computation in the presence of predicate definitions.
• Week 5: Groundedness of variables. Parameter modes. Well-modedness of predicate definitions and programs.
• Week 6: Simple function definitions. Predicate definition corresponding to a function definition. Transformation of function references.
• Week 7: Computation of functions. Soundness of computation. Lambda notation. The Y combinator. Objects and attributes. Equality over complex terms.
• Week 8: Procedure definitions. Predicate definition corresponding to a procedure definition. Transformation of imperative code.
• Week 9: Imperative computation. Soundness of computation. Parameter aliasing. Implementation issues.
• Week 10: Negation. Computation of negation. Well-modedness of programs in presence of negation. Soundness.
• Week 11: If-then-else in logic, functional and imperative languages. Recursive functional and imperative programs.
• Week 12: Types. Base types and arrow types. Subtype declarations. Universal and fixpoint types.
• Week 13: Object class definitions. Predicate and type definitions corresponding to object definitions. Transformation of object-oriented code.

Assignments

• Assignments are generally due Mondays by 5:00pm. Assignments should be submitted to me in class, put in my department mailbox, or slipped under my office door. Late assignments will have 10% subtracted from the grade off the top for each 24-hour period of lateness, to a maximum of 5 days of lateness. Assignments that are more than 120 hours late will not be accepted.

Ethical Conduct

All assignments are individual assignments. You may  discuss approaches to problems among yourselves; however, the actual details of the work (assignment coding, answers to concept questions, etc.) must be an individual effort. Assignments that are judged to be the result of academic dishonesty will, for the student's first offence, be given a mark of zero with an additional penalty equal to the weight of the assignment also being applied. You are responsible for reading and respecting the Computer Science Department's policy on  Scholastic Offences  and Rules of Ethical Conduct .

Please note that we have sophisticated software in place that will examine your code against everyone else in the class and report any incidents of copying.

Plagiarism: Students must write their essays and assignments in their own words. Whenever students take an idea, or a passage from another author, they must acknowledge their debt both by using quotation marks where appropriate and by proper referencing such as footnotes or citations. Plagiarism is a major academic offence (see Scholastic Offence Policy in the Western Academic Calendar).