# Types Are Theorems; Programs Are Proofs

• Jul 14, 2014 · 6:30 PM

Join Philly Lambda and speaker Mark Jason Dominus for another talk diving into the deep waters of type theory and the Curry-Howard correspondence.  Mark writes:

One of the most famous features of functional languages such as Haskell and Scala is their complex, fine-grained type systems. In Haskell, we find that it's easy to construct functions with types

a -> (b -> b)
a -> (b -> a)
a -> (a -> b) -> b

but it is impossible to construct functions with types

a -> (a -> b)
(a -> b) -> a
(a -> b) -> b

What is the distinction here? The answer is astounding:

There is a function of type T if and only if T, reinterpreted as a statement of logic, is a *true* statement.

The correspondence goes futher: if you have a program P with type T, then not only can you understand T as a theorem of logic, but you can understand P as a proof of the theorem. Or working the other way, if you have a proof P of some logical theorem T, you can convert P into a program whose type is T.

This is the foundation for more complex, dependently-typed languages such as Agda where the type of a program P are understood explicitly as assertions about the behavior of P.

• ##### Tim V.

Monday's are out for me. Really wish I could make it. :( Any chance of a recording?

July 2, 2014

• ##### Joshua K.

The slides are up on Mark's website: http://perl.plover.co...­

1 · July 15, 2014

• ##### Tim V.

Thanks! :)

July 15, 2014

• ##### Mark D.

Thanks for coming to my talk yesterday! I hope everyone had a good time. The complete slides (including the ones I didn't get to about logical-or and negation( are at http://perl.plover.com/yak/CHI/ . Please feel free to email me with questions at [masked].

2 · July 15, 2014

• ##### Jim

Mark, thanks for the great talk! Got me excited about learning some agda!

2 · July 15, 2014

• ##### A former member

What floor is SevOne at? I do not see it on the board...

July 14, 2014

• ##### A former member

Never mind... it is the 11th floor

July 14, 2014

• ##### Michael R.

Is the presentation starting at 6:30, or is that just the arrival time?

July 14, 2014

• ##### Dan M.

good question. i guess it depends when mark and or the pizza get here.

July 14, 2014

• ##### Daniel M.

Sorry, something has come up, I can't make it out tonight.

July 14, 2014

• ##### Paul S.

We've had to move the date of this talk from Wednesday, July 9 to Monday, July 14. Apologies for the inconvenience.

July 1, 2014

### 20 went

• ##### Ben A.
• A former member
• A former member
• A former member
• A former member

Founded Sep 26, 2013

#### People in this Meetup are also in:

• ##### Philly DevOps

1,367 Members

• ##### GeoPhilly

1,257 Mappers

• ##### Philly.rb

1,039 Rubyists

• ##### Software as Craft Philadelphia

1,487 Crafters

• ##### PhillyJS

1,147 Members

• ##### The Philadelphia Python Users Group (PhillyPUG)

2,230 Pythonistas