EECS 490 - Programming Languages

This class covered the fundamentals of programming language design, and provided an in-depth view of modern programming paradigms.

Language Design and Implementation

We began this class by implementing a language called AL, short for Arithmetic Language. This simple language, designed in the functional programming paradigm, was given more nuance as we progressed through the class, adding in functions, recursion, memory manipulation, self-referential and gradual typing, and various other functionalities that are indicative of modern programming languages. As we progressed through the course, AL became ALFA ML, a member of the ML family like Haskell, Elm, or OCaml. Throughout the process, we expressed the functionality of the language through Church's lambda calculus, enabling us to mathematically generate proofs of correctness for our programs.

Type Synthesis, Analysis, and Derivation

As we implemented AL, we began with static typing of numbers and booleans. As it progressed, however, we needed greater flexibility. We introduced arrow types to represent functions, universal types that allow for more abstraction, recursive types that can be used to define lists and trees, and more. Eventually, we also implemented a gradual typing design that matches the one found in most scripting languages, such that the program can be executed when some branches are not well typed.

We additionally implemented type checking systems, based on two paradigms: synthesis, which takes an expression and determines what type it has, and analysis, which takes an expression and a type and determines if the two are consistent. Both of these paradigms had their own rules and judgements, and they proved useful and necessary in checking whether a program was well-typed or not before execution could occur.

Lastly, we generated typing derivations by hand, in which we would take a complex expression and determine what its type was, then prove that our determination was correct through the judgements that defined our type system. This allowed us to prove through lambda calculus that our program behaved as expected for various complex types.

Functional Programming in OCaml

Our custom language, ALFA ML, was implemented using OCaml. This meant becoming broadly comfortable with OCaml as a language, and adopting a functional approach to programming more generally. Additionally, we were graded on efficiency and style in our OCaml code. As a result of this class, I consider myself a competent functional programmer, which combines nicely with my grasp on imperative programming to give me a wide breadth of skills in computer science.