From Untyped to Simply Typed Lambda Calculus

[supersven]

Proposal

type: long talk
audience: intermediate
category: pl theory

Summary

The Simply Typed Lambda Calculus adds function types (e.g. not:: Bool -> Bool) to the Untyped Lambda Calculus. It is the simplest example of a typed lambda calculus and can be used as a foundation for functional programming languages with simple type systems (i.e. without polymorphism, higher kinded types, dependent types...) You can also consider it as the next easy learning step into understanding more complex type systems.

Following the motto: "... there is nothing so practical as a good theory!" we'll combine theory and practice by writing an interpreter and a type checker, guided by their theoretical counterparts. These are Evaluation Rules for the interpreter and Typing Rules for the type checker.

To understand evaluation and typing rules we'll learn how to read Inference Rules in general. You can find this notation in many papers about type systems and operational semantics - so it's definitely worth learning.

Of course, we'll start with a quick recap / introduction to the Untyped Lambda Calculus.
Code examples will be in Haskell, but I promise to keep them as simple as possible - No fancy stuff... ;)

(Please note: I'm at the Haskell eXchange in London from 8th to 14th October, so I won't be able give this talk in that week...)

[pheymann]

Hi @supersven ,
thanks for your follow-up proposal for #5. It looks good to me. Regarding the next event, I will let you know in time when this will take place. But I think it will happen in October.

[supersven]

Hey @pheymann ,
Thanks a lot for checking that the proposal is "sound". 👍
I really appreciate that!

I would be glad to give this talk at the upcoming Meetup. So please consider this as a submission to the "November - Call for Papers".

Best regards,

Sven

[pheymann]

Hi @supersven ,
I will put you on the schedule. The meetup should be online today or tomorrow.

Cheers,
Paul

[pheymann]

@supersven I just realized that I booked the Meetup room for the 22.11, not the 20.11. Are you able to also give the talk on the Thursdays the 22.11?

[pheymann]

Doesn't matter. I found another room which should fit all people - I hope :) . So we keep the 20th.

[supersven]

Ok 👍