Home » forums » LtU Forum

Teaching challenge: culturally enriching formulae-as-types

In a G+ request, Norman Ramsey says he wants spice up his PL survey course with a little bit of "cultural enrichment" to show my students the "propositions as types" approach to proof. He's looking for source materials, and, I take it, experiences from people who have tried to teach similar things.

By Charles Stewart at 2012-02-09 10:56 | LtU Forum | previous forum topic | next forum topic | other blogs | 5340 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Adam Chlipala

Adam Chlipala is teaching courses and writing a textbook in this vein. Follow the links, maybe approach the man for advice.

By dmbarbour at Thu, 2012-02-09 19:53 | login or register to post comments

FWIW

Adam was hugely patient with me when I sat next to him at the POPL '08 Coq tutorial. I'm currently working through his CPDT, and am enjoying it tremendously.

By Paul Snively at Thu, 2012-02-09 22:50 | login or register to post comments

Too heavyweight

This is meant to be an intro lecture in a course to students who have met the simply-typed and polymorphic lambda calculus, but not yet dependent types.

As a general point, this is the right way around. Dependent type theory features complex inference rules that are much easier to grasp if you understand the formulae-as-types correspondence.

Adam Chlipala's book was mentioned in the answers to a relevant cstheory.sx question, What is the most intuitive dependent type theory I could learn?

By Charles Stewart at Fri, 2012-02-10 10:00 | login or register to post comments

Software Foundations

I quite liked Benjamin Pierce et al.'s Software Foundations. It starts off at a slower pace than CPDT.

By Ruud Koot at Sat, 2012-02-18 22:10 | login or register to post comments

The last lecture to my first

The last lecture to my first year students (Informatics 1 Functional Programming---taught in Haskell) covers Boole, Frege, Church, Gentzen, and Curry-Howard. Slides are here.

By Philip Wadler at Fri, 2012-02-10 22:36 | login or register to post comments

Wow, you actually lecture in Haskell too?

Seriously, that seems like a short amount of time to give to those five worthies.

By johnwcowan at Wed, 2012-02-15 14:46 | login or register to post comments

Simply Typed Lambda Calculus?

The 'propositions as types' derives from the fact that for a lot of lambda calculi types can be seen to encode logical propositions, and a lambda term can only be constructed in case the proposition is true. The terms are often called 'witnesses' or 'proof objects' because of that quality. Apart from that, very intricate types can specify very specific programs, and conversely the 'witnesses' of that type are programs which will calculate values according to the specification as provided by the intricate type.

Most of this is not that hard to explain when starting from simply typed lambda calculus, and there should be enough text books explaining this. Barendregt should be a good place to start.

I am a natural sceptic and often doubt the validity of claims made by fundamental CS or 'obvious' correspondences. One way to look at the 'types as propositions' correspondence is to view it as a necessary, but also 'coincidental,' correspondence with a limited application domain. Very sceptically, the correspondence just shows that you need proving power to prove any, or some (type), property over a program. (The correspondence is deeper than that, though.)

For programming languages, where I doubt types actually often form a consistent logic, the 'types as propositions' might therefor not be a very interesting quality to have, or to strive for. But I would need to show that, and I didn't do that as of yet.

By marco at Mon, 2012-02-13 18:36 | login or register to post comments