Lectures and coursework for APL are now complete. The exam will be held in the April/May diet; exact dates will be announced by the Student Administration Service on Monday 2 March 2015.
If you have any questions about the course, or would like to discuss preparation for the exam, then please send me email or drop in during my office hours, 1030–1130 every Wednesday during semester.
Thank you for your participation and contributions to this course.
Links: Lecture slides; Exam arrangements
I have just sent out by email the grades and detailed feedback sheets for all students’ coursework submissions. My apologies for the extended delay in marking and returning this.
If you would like a short one-to-one meeting for individual feedback then please send me an email to arrange a time at the start of Semester 2.
Thank you for your participation in the course, and I wish you all well for the remainder of your studies in Edinburgh.
This final lecture for the course included advice on the exam structure and content, some general information about different kinds of assessment, and discussion of specific questions from previous papers.
Today’s lecture presented the final component in the quartet of type/term interaction: after first-class functions, parameterized types, and polymorphic terms, we have types that depend on the value of terms. Numerical examples include type-safe vectors and matrices; but 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 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.
Beyond the simply-typed lambda-calculus, and even Hindley-Milner polymorphism, there’s a whole world of type systems for more expressivity, more precision, and more polymorphism. Tuesday’s lecture looked at some of this: issues around subtype polymorphism in object-oriented code, motivations for higher-rank polymorphism, and the wonders of 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…
This lecture presented examples of parameterized types in different programming languages: families of data types with a common structure, built by applying type constructors to on or more type parameters; as in Java or C# generics, or the algebraic datatypes of Haskell or 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). The Hindley-Milner type system, illustrated in this lecture as applied to the simply-typed lambda-calculus, expands types into type schemes that summarize multiple possible types of a polymorphic function. Hindley-Milner is distinctive in guaranteeing that any code has a principal type scheme that captures every possible type, and the efficient Algorithm W for type inference which can find (“infer”) that most general type scheme.
Static Analysis for Java Concurrency with ThreadSafe
I’m very pleased to have Bob Atkey present a guest lecture in APL.
Bob is a researcher and developer: his extensive original research on programming languages, types, and effects stands alongside practical work such as that with Edinburgh spin-out Contemplate on their flagship ThreadSafe product for early detection of concurrency bugs in Java.
||ThreadSafe: Static Analysis for Java Concurrency
ThreadSafe is the leading static analysis tool for finding and diagnosing dangerous concurrency bugs in Java code.
Why wait for customers to find what ThreadSafe can help prevent? Take your free trial today.
He is also an engaging and approachable speaker, and I strongly recommend coming along to hear him this afternoon.
Links: Slides; Bob Atkey; Contemplate
Friday’s lecture began a final block of material 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
This lecture presented ways to take proofs of code properties beyond correctness or safety of individual programs into the domain of mobile code, trustworthiness, and complete systems. Continue reading
Friday’s lecture presented two different methods for Java programs that are intended to help with writing correct code: the standard Java
assert statement; and JML, the Java Modeling Language. Continue reading