Today’s lecture set out some alternative approaches for managing concurrency in programming languages: asynchronous message-passing *Actors* and the always-upbeat optimistic concurrency of *Software Transactional Memory*. These are two examples from a wide range of mechanisms in use across many programming languages and applications domains, all of which seek to balance the key concurrency requirements of *separation* to prevent inconsistency and *co-operation* to allow interaction.

Continue reading Lecture 10: Some Other Approaches to Concurrency

# Category Archives: Lecture Log

# Lecture 9: Concurrency Abstractions

In this lecture I reviewed the built-in Java concurrency primitives, the challenges of writing thread-safe code, and introduced some patterns that can help: immutability, synchronization wrappers, and control abstractions like producer/consumer. More high-level currency abstractions, such as those in the `java.util.concurrent`

package, support programming that is not only thread-safe but takes explicit advantage of concurrency to increase performance and responsiveness. Finally, I walked through some intentionally racy code in the Java `String`

library.

Continue reading Lecture 9: Concurrency Abstractions

# Lecture 8: Peer Review and Feedback

Today’s session was to review and give feedback in small groups on the preliminary reports submitted as the first stage of the APL assignment. Thanks to everyone who came along to today’s session and contributed their comments. This was the first time I’ve done this in the course, and I’m grateful to those who commented on the arrangements.

Continue reading Lecture 8: Peer Review and Feedback

# Lecture 7: Concurrency

Moving on from type systems, today’s lecture started a look at programming for concurrency: why you might want — or need — to write concurrent code and some of the challenges in doing so. I also introduced some of the concurrency primitives in Java and how they are used, as well as telling a story about the Apollo Guidance Computer and the robustness of its concurrent event handling under input overload.

Continue reading Lecture 7: Concurrency

# Lecture 6: Dependent Types

This lecture completes the quartet of type/term interactions: after first-class functions, parameterized types, and polymorphic terms, we have types that depend on the value of terms. Numerical examples include types to capture vector lengths and matrix dimensions. Dependent types can also be used to strengthen the *deep embedding* of domain-specific languages into a host *meta-language*. Examples given included typed lambda-terms and logical formulas. The lecture also touched on the *Curry-Howard correspondence* of *propositions-as-types* seen earlier in Wadler’s talk, and the use of dependently-typed programming in the machine-assisted proof of mathematical theorems. Finally, there were some references to dependently-typed languages for writing and verifying programs that are correct by construction.

Continue reading Lecture 6: Dependent Types

# Lecture 5: Coursework Assignment Topics

The coursework assignment for APL is to select a programming language feature from a short list, research what it does, try it out, and write a 10-page report about this. In today’s lecture I presented each of the five possible topics and outlined the assignment structure.

Continue reading Lecture 5: Coursework Assignment Topics

# Lecture 4: Higher Polymorphism

Beyond the simply-typed lambda-calculus, and even Hindley-Milner polymorphism, there’s a world of type systems for more expressivity, more precision, and more polymorphism. Today’s lecture looked at some of this: issues around subtype polymorphism in object-oriented code, motivations for higher-rank polymorphism, and beyond that to *System F*. For System F in particular there’s a range of further possibilities: this lecture covered encoding datatypes, but there are also subtyping, bounded and F-bounded quantification, F_{2}, F_{ω}, existential types, and more…

Continue reading Lecture 4: Higher Polymorphism

# Lecture 3: Parameterized Types and Polymorphism

Today’s lecture gave examples of *parameterized types* in different programming languages: families of data types with a common structure, built by applying *type constructors* to one or more *type parameters*; as in Java or C# *generics*, or the algebraic datatypes of Haskell and OCaml. To work with parameterized types we use *polymorphic functions* — code that can work with more than one type, either in a uniform way (*parametric* polymorphism) or with type-specific variations (*ad-hoc* polymorphim).

Continue reading Lecture 3: Parameterized Types and Polymorphism

# Lecture 2: Terms and Types

Friday’s lecture introduced the first topic for the course, on *types* in programming languages: some of the ways they are used, and their relation to the mathematical models of *lambda-calculus* and *type theory*. This lecture presented the simply-typed lambda-calculus and some examples of programming language support for *first-class* functions.

Continue reading Lecture 2: Terms and Types

# Lecture 1: What’s So Important About Language?

This opening lecture presented some context for studying programming languages, and what might inspire research into new ones. You can read some of this in the slides which are also available by clicking on the title slide image to the right.

Continue reading Lecture 1: What’s So Important About Language?