Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » Education » math-teach

Topic: Structured Programming
Replies: 103   Last Post: Mar 25, 2014 12:33 AM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
GS Chandy

Posts: 7,761
From: Hyderabad, Mumbai/Bangalore, India
Registered: 9/29/05
Re: Structured Programming
Posted: Mar 11, 2014 4:42 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

Many thanks, Joe Niederberger, for drawing our attention to 'Homotopy Type Theory' (HOTT; in your post dt. Mar 4, 2014 1:36 AM [http://mathforum.org/kb/message.jspa?messageID=9400390]) and to the BIG book on it: "Homotopy Type Theory: Univalent Foundations of Mathematics".

I have since re-read, quite carefully, the Introduction to the book - No, I've not yet done any modeling there, because I believe this will be possible only when I've at least started studying 'Foundations'. I HAVE made a fair start on 'reading through' "Foundations" - Type Theory; Type Theory Vs. Set Theory; Function Types; Category Theory; etc, etc. (I recall, from my grad school days, that Category Theory used those days to be considered to be a most abstract and perhaps a most advanced topic!!)

I've also read (and listened to) the talk on "Univalent Foundations" by Vladimir Voevodsky.

As noted in an earlier post, some of it is pretty hairy stuff (in particular when I look at some of the 'exercises' in the book). I'm also sure I'll not succeed in 'studying HOTT as a discipline' (with modeling) UNLESS I am guided by someone who's reasonably expert with HOTT. Let's see how it goes.

I believe that the real impact of HOTT will not be just to enable "all mathematicians routinely do all their work in machine readable form and work collaboratively off github. Russel' dream realizedm etc, etc"... I believe HOTT's real impact will be to enhance the 'development of the foundations of math' (much more than is possible by earlier approaches), AND also to help enable people at large (Mr John Doe and Ms Mary Doe) to appreciate and understand AND use math much more effectively than they have been able to do in the past. As I've earlier tried to make clear, this is precisely what OPMS tries to do - perhaps I may be able to interest some HOTT person in this kind of thing as a worthwhile thing to do? Let's see.

However, I DO believe that the 'structures' (the 'higher-level models') within OPMS would help clarify several of the issues in HOTT. Hopefully, I shall be able to convince someone accordingly at 'The Univalent Foundations Program'. As noted, let's see how it goes.

GSC


Message was edited by: GS Chandy


Date Subject Author
3/6/14
Read Re: Structured Programming
kirby urner
3/6/14
Read Re: Structured Programming
Robert Hansen
3/7/14
Read Re: Structured Programming
Louis Talman
3/7/14
Read Re: Structured Programming
kirby urner
3/7/14
Read Re: Structured Programming
Robert Hansen
3/7/14
Read Re: Structured Programming
Joe Niederberger
3/8/14
Read Re: Structured Programming
Joe Niederberger
3/9/14
Read Re: Structured Programming
Robert Hansen
3/9/14
Read Re: Structured Programming
GS Chandy
3/9/14
Read Re: Structured Programming
GS Chandy
3/9/14
Read Re: Structured Programming
GS Chandy
3/10/14
Read Re: Structured Programming
kirby urner
3/9/14
Read Re: Structured Programming
GS Chandy
3/10/14
Read Re: Structured Programming
kirby urner
3/11/14
Read Re: Structured Programming
Louis Talman
3/11/14
Read Re: Structured Programming
Robert Hansen
3/11/14
Read Re: Structured Programming
kirby urner
3/12/14
Read Re: Structured Programming
Robert Hansen
3/12/14
Read Re: Structured Programming
kirby urner
3/9/14
Read Re: Structured Programming
GS Chandy
3/10/14
Read Re: Structured Programming
GS Chandy
3/9/14
Read Re: Structured Programming
GS Chandy
3/9/14
Read Re: Structured Programming
GS Chandy
3/9/14
Read Re: Structured Programming
GS Chandy
3/10/14
Read Re: Structured Programming
Joe Niederberger
3/10/14
Read Re: Structured Programming
Robert Hansen
3/11/14
Read Re: Structured Programming
Robert Hansen
3/10/14
Read Re: Structured Programming
GS Chandy
3/12/14
Read Re: Structured Programming
kirby urner
3/11/14
Read Re: Structured Programming
GS Chandy
3/12/14
Read Re: Structured Programming
GS Chandy
3/12/14
Read Re: Structured Programming
GS Chandy
3/11/14
Read Re: Structured Programming
Joe Niederberger
3/11/14
Read Re: Structured Programming
Robert Hansen
3/11/14
Read Re: Structured Programming
Joe Niederberger
3/11/14
Read Re: Structured Programming
GS Chandy
3/12/14
Read Re: Structured Programming
Joe Niederberger
3/12/14
Read Re: Structured Programming
Robert Hansen
3/12/14
Read Re: Structured Programming
GS Chandy
3/12/14
Read Re: Structured Programming
Robert Hansen
3/12/14
Read Re: Structured Programming
GS Chandy
3/12/14
Read Re: Structured Programming
GS Chandy
3/12/14
Read Re: Structured Programming
GS Chandy
3/12/14
Read Re: Structured Programming
GS Chandy
3/12/14
Read Re: Structured Programming
Robert Hansen
3/12/14
Read Re: Structured Programming
Robert Hansen
3/13/14
Read Re: Structured Programming
GS Chandy
3/13/14
Read Re: Structured Programming
GS Chandy
3/13/14
Read Re: Structured Programming
Robert Hansen
3/13/14
Read Re: Structured Programming
Joe Niederberger
3/13/14
Read Re: Structured Programming
Joe Niederberger
3/13/14
Read Re: Structured Programming
Robert Hansen
3/13/14
Read Re: Structured Programming
GS Chandy
3/13/14
Read Re: Structured Programming
Robert Hansen
3/13/14
Read Re: Structured Programming
Joe Niederberger
3/16/14
Read Re: Structured Programming
Robert Hansen
3/15/14
Read Re: Structured Programming
GS Chandy
3/13/14
Read Re: Structured Programming
GS Chandy
3/14/14
Read Re: Structured Programming
kirby urner
3/14/14
Read Re: Structured Programming
GS Chandy
3/15/14
Read Re: Structured Programming
kirby urner
3/16/14
Read Re: Structured Programming
Robert Hansen
3/16/14
Read Re: Structured Programming
kirby urner
3/16/14
Read Re: Structured Programming
Robert Hansen
3/16/14
Read Re: Structured Programming
kirby urner
3/16/14
Read Re: Structured Programming
Robert Hansen
3/17/14
Read Re: Structured Programming
Joe Niederberger
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
Joe Niederberger
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
Joe Niederberger
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
kirby urner
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
Joe Niederberger
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
kirby urner
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
kirby urner
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
kirby urner
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
kirby urner
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
kirby urner
3/18/14
Read Re: Structured Programming
Robert Hansen
3/19/14
Read Re: Structured Programming
kirby urner
3/18/14
Read Re: Structured Programming
Joe Niederberger
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
Robert Hansen
3/18/14
Read Re: Structured Programming
Joe Niederberger
3/19/14
Read Re: Structured Programming
Robert Hansen
3/20/14
Read Re: Structured Programming
Louis Talman
3/20/14
Read Re: Structured Programming
Robert Hansen
3/20/14
Read Re: Structured Programming
Louis Talman
3/18/14
Read Re: Structured Programming
Joe Niederberger
3/19/14
Read Re: Structured Programming
Joe Niederberger
3/19/14
Read Re: Structured Programming
Robert Hansen
3/20/14
Read Re: Structured Programming
Louis Talman
3/19/14
Read Re: Structured Programming
Joe Niederberger
3/25/14
Read Re: Structured Programming
GS Chandy

Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.