Blog

Programming Language Foundation I is an introduction to the semantics of programming languages. The course will present modern techniques for defining operational semantics and type systems for programming languages. Topics include inductive definitions, the lambda calculus, defining evaluation relations, small-step operational semantics, the simply typed lambda calculus, defining type relations, progress and preservation, type reconstruction and subtyping.

- Room and Time
- 2112 Learned Hall
- 2:30-3:45 TR
- Prerequisites
- EECS 662 is recommended, but not required.
- Instructor Information
- Dr. Perry Alexander
- Office Hours: 1:30-2:30 TR in 3048 Eaton Hall, or by appointment
- Office: 3048 Eaton Hall / 208 Nichols Hall
- Phone: 4-7741
- Web: https://perry.alexander.name
- Email: palexand@ku.edu
- Textbooks
- Benjamin Pierce,
*Types and Programming Languages*, MIT Press, 2002. ISBN: 0-262-16209-1 (Required) - Benjamin Pierce, et. al.,
*Software Foundations*, published online. (Optional)

Grades are assigned on a standard 10 point scale:

- A = 90-100%
- B = 80-90%
- C = 70-80%
- F = 0-70%

Classroom tasks are weighted using the following scale

- Midterm Exam 40%
- Final Exam 40%
- Homework and Mini Projects 20%

You must pass both projects and homework, and exams separately to pass the class. Specifically, if you get less than 60% on your projects and homework or less than 60% on your exams, you will not pass the course.

I may curve final grades at the end of the semester. However, I will never curve individual assignments or exams. If I curve and how much I curve is at my discretion.

Projects and homework will be due on approximately a weekly basis. Unless otherwise noted, projects and homework are due at the beginning of the class period indicated on the web page. If the due date is a holiday and KU offices are closed, the due date becomes the next class period. Late homework assignments are not accepted. You must turn in 70% of your assignments on time to receive a passing grade in the course. If you have a valid excuse for being late, a new due date will be assigned.

Prepare your homework submissions using LaTeX using an equation formatting library such as the freely available semantic package. There are a number of ways to use LaTeX ranging from Emacs and AuCTeX to the online Overleaf system. If you are getting started with LaTeX, Overleaf is strongly suggested.

Submit your project and homework solutions as PDF files using the KU Blackboard system unless otherwise specified. This is the only thing we will use blackboard for.

All project and homework assignments, exams, solutions and handouts you receive in class are linked to the EECS 762 homepage. In general, I will not distribute hard copies of assignments in class. All documents will be published using the Adobe PDF standard.

This term we will be using Piazza for class discussion. The system is highly catered to getting you help fast and efficiently from classmates as well as me. I encourage you to post your questions on Piazza. Use the Piazza signup link to join. I will provide the permission code in class.

All exams are closed book, closed notes, in-class exams. The final exam will be held during the time assigned by the University in our regular classroom.

Pretty simple. Follow them and we’ll be great friends!

- Don’t whine
- Don’t cheat
- Don’t tell me what you don’t need to know

I do not take attendance in class; however participation in class is important to your success, however participation in class is important to its success. How much homework and how rigorously it is graded will definitely depend on class participation. Please ask questions and participate in class discussions. When assigning final grades, borderline cases will be decided based on class participation.

If I have made an error in grading an exam or assignment, you have two weeks following the date the item is available to see me about correcting the problem. Note that this includes the final! After that time, your grade is set and will not be changed. I also request that you wait 24 hours after an exam is returned before coming to me with questions.

I may decide to curve final scores when the quarter is over. Whether I curve and how much I curve is at my discretion. I will never curve up, but may curve down. Specifically, 90% and above will always be an “A”, but I may choose to lower the cutoff percentage. Whether I curve and how much I curve is at my discretion. I will never curve scores on an individual graded assignment, lab or exam.

I encourage you to use email to contact me. I am logged in whenever I am working and check my mail frequently. Email is my preferred means of communication.

The course blog is available on the website. I will post late-breaking news about projects, homework and class administration on the blog. Check the website and blog freqently, particularly around project due dates and exams.

Feel free to call me in any of my office at any time. I would prefer not to be called at home.

I will make every effort to be in my office during scheduled office hours. If there are exceptions, I will let you know as early as is possible. If you have a conflict with my office hours, please make an appointment. I have an open door policy, you are free to come by whenever you choose. If I am busy, I may ask that you come back later, but please don’t hesitate to knock!

Academic misconduct of any kind will automatically result in a 0 score on the homework, lab, project, or exam in question and your actions will be reported to the department chair. Your homework, exams and projects must be individually prepared unless otherwise noted. Posting your assignments to internet discussion lists is considered academic misconduct. Sharing your solutions with others is considered academic misconduct. Turning in solutions from previous semesters is considered academic misconduct. Paying people to prepare solutions is academic misconduct. Automated mechanisms are available for checking the originality of source code. Please spend your time trying to solve assigned problems rather than trying to get around the system. Don’t risk it!

Excusing a missed exam or assignment is left to the discretion of the instructor. Illness, family emergencies, and religious observances are examples of acceptable excuses. Computer down time, over sleeping, and social events are examples of unacceptable excuses. Please try to let me know of problems in advance when possible and be prepared to provide verification of your excuse.

As a policy, I do not extend due dates of homework and projects. If I choose to do so, I will only announce the extension in class, via email or on the blog. If you hear an extension has been granted and I have not announced it, your information is incorrect. Remember that if I grant extensions early in the semester, it will necessarily compress due dates the end of the semester.

Ties are expressly forbidden in my classroom. If you wear one you will be taunted mercilessly. Exceptions are made for bow ties which we all know are cool.

We will cover topics in roughly the same order as our text. I will also add miscellaneous topics throughout the semester. Specific topics are subject to change without notice and topics marked “(tentative)” will be covered as time permits.

- Preliminaries
- Formal Systems
- Sets, Relations and Functions
- Sequences
- Coq Basics

- Inductive Definitions
- Principles of Induction
- Rule Induction and Special Rule Induction
- Proof rules for operational semantics
- Least fixed points
- Coq Inductive Definitions and Proofs

- Untyped Systems
- Arithmetic expressions
- Untyped Lambda Calculus
- De Bruijn Numbering

- Simple Types
- Typed Arithmetic
- Simply Typed Lambda Calculus
- Simple Extensions to Typed Lambda Calculus
- Normalization

- Subtyping and Polymorphism
- Subtyping
- Type reconstruction
- Universal Types
- Existential Types