Big Picture
Basic Coordinates
Academic Integrity

CS93 - Programming Languages Directed Reading

CS93 Logo

Big Picture

Basic Coordinates

Instructor: Benjamin Ylvisaker

Textbook: We will be reading parts of three books:

Previously we considered using Coq instead of Isabelle. Some good starting points for Coq:

Piazza for most online class communications. If you email the instructor you will probably get a private response on Piazza.

Meetings: Friday 12:30-2; Wednesday 7pm-??? in the CS seminar room.

No scheduled office hours. Make an appointment or drop in.



Week Topic & Important Dates Misc
1 1/20 Intro Notes on the λ-calculus
Chapter 17 of PFPL
1/24 Lambda calculus
2 1/29 Ben traveling Logic notes 1
Logic notes 2
1/31 Ben traveling
3 2/5 Logic & proof techniques Isabelle/HOL tutorial chapters 1 & 2
2/7 Our first Isabelle programming!
4 2/12 Preservation & progress for untyped λ-calc
Maybe getting into typed languages a bit
Section II of PFPL (chapters 4-7)
Section III of PFPL (chapters 8-10)
5 2/19 [canceled]
6 2/26 Products
2/28 Unions
7 3/5 Pattern matching
3/7 Generics
8 Spring break (3/8-3/16) ❧
9 3/19 Inductive & coinductive
3/21 Recursive
10 3/26 Dynamic
11 4/2
12 4/9
13 4/16
14 4/23
15 4/30
16 5/? Finals week


Disability Accommodation

If you believe that you need accommodations for a disability, please contact Leslie Hempling in the Office of Student Disability Services (Parrish 113) or email to arrange an appointment to discuss your needs. As appropriate, she will issue students with documented disabilities a formal Accommodations Letter. Since accommodations require early planning and are not retroactive, please contact her as soon as possible. For details about the accommodations process, visit the Student Disability Service website at You are welcome to contact the instructor privately to discuss your academic needs. However, all disability-related accommodations must be arranged through Leslie Hempling in the Office of Student Disability Services.

Academic Integrity

This is the department policy on academic integrity. This is not really relevant to PL reading group, but it's reproduced here for your entertainment.

Academic honesty is required in all your work. Under no circumstances may you hand in work done with (or by) someone else under your own name. Your code should never be shared with anyone; you may not examine or use code belonging to someone else, nor may you let anyone else look at or make a copy of your code. This includes, but is not limited to, obtaining solutions from students who previously took the course or code that can be found online. You may not share solutions after the due date of the assignment.

Discussing ideas and approaches to problems with others on a general level is fine (in fact, we encourage you to discuss general strategies with each other), but you should never read anyone else's code or let anyone else read your code. All code you submit must be your own with the following permissible exceptions: code distributed in class, code found in the course text book, and code worked on with an assigned partner. In these cases, you should always include detailed comments that indicates on which parts of the assignment you received help, and what your sources were.

Failure to abide by these rules constitutes academic dishonesty and will lead to a hearing of the College Judiciary Committee. According to the Faculty Handbook: "Because plagiarism is considered to be so serious a transgression, it is the opinion of the faculty that for the first offense, failure in the course and, as appropriate, suspension for a semester or deprivation of the degree in that year is suitable; for a second offense, the penalty should normally be expulsion."

The spirit of this policy applies to all course work, including code, homework solutions (e.g., proofs, analysis, written reports), and exams. Please contact me if you have any questions about what is permissible in this course.

PL Courses from Around the Web ...

... in case you're curious.

... ... ...