All posts by Ian Stark

Lecture 6: Dependent Types

Title SlideThis 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 4: Higher Polymorphism

Title slideBeyond 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, F2, Fω, existential types, and more…
Continue reading Lecture 4: Higher Polymorphism

Programming Languages Interest Group

When 1pm Thursday 29 September
Where IF 2.33, Informatics Forum

PLInG is an informal meeting series for Informatics students and staff interested in programming languages. It’s organized by James Cheney and Michel Steuwer with meetings every fortnight or so.

All are welcome to attend, and the format is flexible: with presentations of work in progress, interesting recent papers, reports from conferences, or discussion with visitors. This first meeting is to make plans for the semester and hear trip reports from those just back from last week’s International Conference on Functional Programming (ICFP) in Japan.

Links: Meeting schedule; Mailing list

Lecture 3: Parameterized Types and Polymorphism

Title slideToday’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


Welcome to Advances in Progamming Languages, September–December 2016. If you are interested in the course then come along to the first lecture at 1510 on Tuesday 20 September, in the George Square Lecture Theatre. There’s no need to enroll beforehand, but please do prepare by following these instructions.

1. Watch this
MIT Technology Review: 35 Innovators under 35

Jean Yang
Assistant Professor of Computer Science, Carnegie Mellon University

Link: Prof. Yang at CMU

Jean Yang
2. Do this
  • Find out about the Blub Paradox.
  • Read the article which named it.