/programming-languages-2019

Primary LanguageHaskell

programming-languages-2019

Notes for the Programming Languages course at Chapman University 2019 by Alexander Kurz and Samuel Balco.

For any questions, comments, etc raise an issue.

Office Hours Tue and Thu 2pm to 3.30pm in Hashinger 208 or by appointment.

The aim of the course is to have a look under the hood of programming languages. How do programming languages work? Could you design your own programming language? Instead of looking at particular examples of programming languages, we will build our own. It will be small and not efficient, but we will be able to understand in all detail how it works. The principles we learn apply to industrial scale programming languages such as C++ as we will see in more detail in the sequel course of Compiler Construction next semester.

Prerequisites: I assume that you know at least one, ideally a few more, programming languages. It would also be good to have learned something about computer architecture. One theme of the course is how to bridge the gap between a programming language and the actual machine, so some awareness of how actual machines work is needed to fully appreciate the material. Finally, while I will introduce the mathematics that we need to engineer our programming languages, some ability in manipulating formal mathematical models as typically aquired in a discrete mathematics or introductory logic course will be needed.

It is possible to read the following notes without doing the labs and the programming assignments, but it will make it more difficult to appreciate that the methods and tools presented in this course solve real, every day practical software engineering problems that are impossible to solve without beautiful and powerful mathematics.

Lecture 1.1: Overview and Organisation.
Lecture 1.2: Short Introduction to Parsing.

Part I: Lambda Calculus and Functional Programming

Lecture 2.1: Syntax of Lambda Calculus.
Lecture 2.2: Semantics of Lambda Calculus.
Lab 3.1 - 4.2: Programming the Lambda Calculus. See also the Lab1-solutions
Lecture 5.1: Introduction to Term Rewriting.
Lecture 5.2: Syntax and Semantics and Equivalence Relations. Meaning in Syntax

Assignment 1: Deadline Thursday Oct 3

Part II: Term Rewriting

Lecture 6.1: Abstract Reduction Systems Examples
Lecture 6.2: ARS2: Confluence and Normal Forms
Lecture 7.1: ARS3: Termination. ARS4: Finitely Branching ARSs
Lecture 7.2: Rules of logic. ARS5: Invariants
Lecture 8.1: Normalisation by Evaluation

Exercises on ARSs. Midterm: Thu, Oct 17. Feedback on Midterm

Part III: Logic and Program Verification

Lecture 9.1: Induction and Equational Reasoning
Lecture 9.2: Theorem Proving
Lecture 10.1 and 10.2: Hoare Logic

Exercises on Program Verification. Test on Hoare Logic Tue, Nov 12. Feedback.

Part IV: Universal Algebra and Category Theory

Lecture 11.1: Abstract Data Types, Structure Preserving Maps,
Lecture 11.2: Universal Properties, Variables and Free Algebras

Part V: Memory and References

Lab 12.1, 12.2: The Programming Language LambdaFun

Lab 13.1, 13.2: Assignment 2
Lecture 13.2: Correctness of Computer Arithmetic

Part VI: Type Theory

deferred to the course on Compiler Construction in Semester 2

Part VII: Essay and Presentation, Instructions
Presentations 14.1: Schedule tba
Presentations 14.2: Schedule tba