
15317 Constructive Logic
Fall 2014 
Karl Crary 
TR 12:001:20 
HH B131 
Recitation Sec A, Wed 12:301:20, SH 222 & GHC 5222 
9 units 
This multidisciplinary junior/seniorlevel 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,
proof search, logical frameworks.
See Constructive
Logic, Fall 2012 for information on a prior version of this course.
What's New?
 (12/10) Solutions for Homework 10 are now available.
 (12/9) Solutions for Midterm II are now available.
 (12/9) Practice final now available. Note that this is from an earlier version of the course in which the material covered was slightly different.
 (12/3) List of natural deduction rules for linear logic now available. Note that this does not include persistent assumptions or the ! connective.
 (12/3) Solutions for Homework 9 are now available.
 (12/2) List of rules for focused linear logic now available.
 (11/26) Homework 10 now available.
 (11/16) After the previous correction, the PDF temporarily said that the assignment was due on the 20th. It is actually due on Nov. 27th, before noon, as it said on the website and original PDF.
 (11/15) There was an error in the first two parts of Task 1 on Homework 9. Please download the corrected assignment. Sorry for any inconvenience.
 (11/14) Solutions for Homework 8 are now available.
 (11/13) Homework 9 now available. NOTE: This assignment is due in 2 weeks, on Nov. 27th. However, it does not require any additional material beyond what we've already covered, so please feel free to get started.
 (11/5) Solutions for Homework 7 are now available.
 (11/1) The second part of task 4 in homework 8 was not written correctly. It has been removed. Please download the fixed PDF.
 (10/30) Homework 8, with starter code, now available.
 (10/30) Solutions for Homework 6 are now available
(SML, Written).
 (10/28) Prolog (1,
2,
3)
and Elf (1,
2,
3,
4,
5)
files from lecture have been posted.
 (10/23) Homework 7 now available.
 (10/22) Solutions for Homework 5 and Midterm I are now available.
 (10/20) There was a typo in the heading for section 2 of homework 6. The section is worth 25 points total, not 35, since task 2 is worth 25 points.
 (10/16) Homework 6 now available,
with SML starter code.
 (10/9) Homework 5 now available.
 (10/8) Solutions for Homework 4 are now available
(Tutch, Written).
 (10/1) Solutions for Homework 3 are now available
(Tutch, Written).
 (9/25) Homework 4 now available.
 (9/24) Solutions for Homework 2 are now available
(Tutch, Written).
 (9/23) Reminder: as indicated on the schedule, the first midterm is Thu. October 2.
 (9/22) There was a typo in homework 3 for tasks 4 and 5. It has now been fixed.
 (9/18) Homework 3 now available.
 (9/17) Solutions for Homework 1 are now available
(Tutch, Written).
 (9/11) Homework 2 now available. NOTE: submission instructions have changed starting with this assignment.
 (9/10) The course Piazza has been created. Please enroll.
 (9/4) Homework 1 now available.
 (9/3) Starting on Wed. 9/10, recitation B will be held in GHC 5222 instead of GHC 4215.
 (8/31) Website created.
Class Material
Schedule 
Lecture schedule, readings, and code 
Assignments 
Assignments, due dates, and policies 
Software 
Proof checkers, language implementations 
Course Information
Lectures 
TR 12:001:20, HH B131, Karl Crary 
Recitations 
Section A, Wed 12:301:20, SH 222, TBA
Section B, Wed 12:301:20, GHC 5222, TBA

Textbook 
There is no textbook.

Credit 
9 units 
Grading 
40% Homework, 15% Midterm I, 15% Midterm II, 30% Final 
Homework 
Weekly 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 25% from an
assignment's total possible score.
NOTE: Each late day extends the deadline by 24 hours.

Midterm I 
Thu Oct 2, in class.
One twosided sheet of notes permitted.
Solutions

Midterm II 
Thu Nov 6, in class.
One twosided sheet of notes permitted.
Solutions

Final 
TBA.
Open notes.

Home 
http://www.andrew.cmu.edu/course/15317/ 
Newsgroup 
academic.cs.15317 
Directory 
/afs/andrew.cmu.edu/scs/cs/15317/ 
Teaching Staff


Office 
Office Hours 
Phone 
Email 
Lecturer 
Karl Crary 
GHC 9217 
Tuesdays 4:00pm  5:00pm 
x87687 
crary@cs 
Teaching Assistant 
Joe Tassarotti 
GHC 7713 
Wednesdays 1:30pm  2:30pm in GHC 7713 

jtassaro@andrew 
Teaching Assistant 
Evan Cavallo 

Mondays 3:00pm  4:30pm in GHC Fifthfloor TA Space 

ecavallo@andrew 
[ Home
 Schedule
 Assignments
 Software
]
