Programming Language Foundation I is an introduction to the mechanized semantics of programming languages. The course will present modern techniques for defining static and dynamic semantics using Rocq for specification and verification. Topics include program equivalence, stateful systems, Hoare Logic, lambda calculus, evaluation relations, small-step operational semantics, typing relations, the simply typed lambda calculus, type safety, and subtyping. All with a heavy dose of Steely Dan and Buckaroo Banzai.
com IMP Subset, Total Maps2/24 No Class
Grades are assigned on a standard 10 point scale:
Classroom tasks are weighted using the following scale
Mini Projects will be due on approximately a bi-weekly basis and are the heart of the course. Modern semantics work is typically done using automated tools for specification and proving. Thus, we will work through a number of projects together in class and independently using Rocq to specify and verify programming language properties. Class participation is vital and will be considered when grading projects.
Most projects will require submission of documented Rocq source only. If you need to submit text, prepare your submissions using LaTeX with 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 solutions as Rocq and PDF files using the KU Canvas system unless otherwise specified. Assignments will be posted here:
All project and homework assignments, exams, solutions and handouts you receive in class are linked to the EECS 762 homepage.
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 unless we as a class decide otherwise. Topics will be posted here:
Pretty simple. Follow them and we’ll be great friends!
I do not take attendance in class, however participation in class is important to its success. I intend to work through projects together in class extensively. How much outside work is assigned and how rigorously it is graded will 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 make an error grading an exam or assignment, you have two weeks following the date the item is returned 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 semester 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 or exam.
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 frequently, particularly around project due dates and exams.
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 ask!
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!
Using AI for proofing and cleaning up solutions is appropriate without citation. Using generative AI to assist with proving or specification is also appropriate when it is properly acknowledged, and your prompts are included as a part of your solution. Using generative AI without proper attribution is claiming work you did not do and is considered academic misconduct. If you use AI tools the best thing is to document what you did.
Excusing a missed exam or assignment is left to my discretion. Illness, family emergencies, and religious observances are examples of acceptable excuses. Computer downtime, 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 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, but 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.
We will cover topics in roughly the same order as our texts. 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.