What type of theory?

When I studied mathematics in college, I really loved algebraic topology, set theory and (first-order) logic. After a graduate course in computer science, I was fascinated by automated theorem proving, constructive proof and type theory. The foundations of mathematics has also been a subject that has interested me.

I came across the Homotopy Type Theory site a few weeks ago while following a link from this blog post where the author discusses the meaning of proof in mathematics. HTT is an attempt to re-launch the foundations of mathematics on a more constructive computational footing. A book written as part of a year long special program at the IAS is available here with an introductory chapter that gives a very good overview of Type Theory.

There are introductory slides here, a blog here and a discussion of the meaning of equality in this setting here.

One of the interesting parts of Type Theory, that can be instantly related to computer science applications is the notion of dependent types. This paper shows some of the uses of this concept.

There team are working hard to get many of their proofs verified by proof assistants such as COQ, so perhaps we really entering a new age of mathematics.

This entry was posted in Computers and Internet. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s