[Alta-Logic] Peripatetic talk: Wed., November 26 th

[Robin Cockett]

Time: 10:00am - 11:00am

Place: ICT 616

Date: Wednesday, 26th November

Title: Curry Howard Isomorphism

Speaker: Prashant Kumar, University of Calgary

Abstract:

In this talk , we will explore an interesting connection between logic and
programming
languages. In brief, logical proofs embody certain constructions which may
be interpreted as
programs. Under this interpretation,propositions become types. It was first
observed by the
logicians Haskell Curry[1960] and William Howard [1969] in different
contexts that this is in
fact an isomorphism: in a certain fragment of logic, every proof describes
a program and every
program describes a proof.

Although Curry Howard can be interpreted at various levels , we will look
into the relationship
using Simply Typed Lambda calculus from the programming side and
Intuitionistic Natural
Deduction from the logic side.

A natural question to ask here is what is such a relationship good for.
Like any isomorphism,
it allows us to switch back and forth and think in whichever system suits
our intuition
in a given situation. Moreover, we can save a lot of work by transferring
theorems that were
proved about the lambda calculus to logic, and vice versa.Proof assistants
like Coq , Agda etc
make use of Curry Howard Isomorphism to extract programs from proofs and
vice versa.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.ucalgary.ca/pipermail/alta-logic-l/attachments/20141125/6e808b5a/attachment.html