15-317 Constructive Logic

Fall 2013
Penny Anderson
TuTh 12:00-1:20
NSH 3002
Recitation Sec A, Wed 12:30-1:20, WeH 6423
9 units

This multidisciplinary junior/senior-level course is designed to provide a thorough introduction to modern constructive logic, its roots in philosophy, its numerous applications in computer science, and its mathematical properties. Some of the topics to be covered are intuitionistic logic, inductive definitions, functional programming, type theory, connections between classical and constructive logic, logic programming, linear logic.


Class Material

Schedule Lecture schedule, readings, and code
Assignments Assignments, due dates, and policies
Handouts Course handouts
Software Proof checkers, language implementations, model-checkers

Course Information

Textbook There is no textbook.
Notes will be handed out throughout the class.
Grading 40% Homework, 15% Midterm I, 15% Midterm II, 30% Final
Homework Most weeks homework is assigned each Thursday and due the following Thursday.
3 late days can be used throughout the semester.
(Each late day beyond the 3 free ones will deduct 20% from an assignment's total possible score.)
Homework assignments are worth a total of 400 points.
Midterm I Thu Oct 3, in class, 150 points.
Closed book, one two-sided sheet of notes permitted.
Midterm II Thu Nov 7, in class, 150 points.
Closed book, one two-sided sheet of notes permitted.
Final Time and place TBD, 300 points
Topics Intuitionistic Logic, Natural Deduction, Sequent Calculus, Inductive Definitions,
Functional Programming, Type Theory, Logic Programming, Classical Logic, Linear Logic
Piazza discussion group

Teaching Staff

    Office Office Hours Phone Email
Lecturer Penny Anderson GHC 6025 Tue, Thu 2:00 - 3:00 and by appointment x8-3413 annpenny at Andrew
Teaching Assistant Michael Sullivan GHC 9005 Wed, Fri 3:00 - 4:00 x8-5940 mjsulliv at Andrew

[ Home | Schedule | Assignments | Handouts | Software ]

annpenny at Andrew