Lecture 7: Dependent Types

Title slide

Slides : Recording

Today’s lecture completes the quartet of type/term interactions: after first-class functions, parameterized types, and polymorphic terms, we have types that depend on terms themselves. Numerical examples include types to capture vector lengths and matrix dimensions, and thereby specify more precisely the domain and range of operations like matrix inversion or multiplication. Dependent types can also be used to strengthen the deep embedding of domain-specific languages into a host meta-language. Examples of this 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.

Links: Slides from Lecture 7; Recording of Lecture 7

Homework
1. Read This

Read through the instructions for the written coursework assignment. If you have questions then send me mail or ask on Piazza.

Link: Coursework instructions

2. Write This

The outline draft for your written coursework assignment, following in detail the instructions supplied.

Further Viewing

Dependent Types in Haskell
Strange Loop, September 2017

Stephanie Weirich
Professor of Computer and Information Science
University of Pennsylvania

Link: Video (38’41”)Prof. Weirich at Penn

Opening slide from talk

Gradual Typing
ICFP Keynote Talk, September 2018
(Audio poor at start, persist and it gets better)

Ronald Garcia
Associate Professor, Software Practices Laboratory
University of British Columbia

Link: Video (62’35”); Slides; Prof. Garcia at UBC

Photo of Prof. Garcia
References

The Coq Proof Assistant

Recipient in 2013 of both the ACM SIGPLAN Programming Languages Software Award and the ACM Software System Award

Links: Coq home page; Documentation and tutorials

Screenshot of web page

Idris

A general-purpose pure functional programming language with dependent types.

Link: Idris home page

Idris language logo

The F* Programming Language

Project demonstrating extensive application of dependently-typed programming for verification, distributed programming, cryptographic protocols, and more.

Links: The F* language; Interactive tutorial

F* language logo

ACM Notices — Special Issue on Formal Proof, November 2008

Includes Georges Gonthier explaining his Coq proof of the four-colour theorem.

Links: ACM Notices Special Issue; Four-colour theorem; Complete issue as PDF

Cover of ACM Notices

Leave a Reply

%d bloggers like this: