Introduction to Higher Type Theory - Daniel Licata's PhD Thesis
67 views
Skip to first unread message
Mark Farrell
Dec 12, 2015, 3:41:18 PM12/12/15
to Type Theory Study Group
Hi all,
I've been taking a look at some of Daniel Licata's work with Robert Harper. Of the work that I've had a look at so, chapter's seven and eight of Licata's PhD seems like a good, digestible introduction to 'computational higher type theory', if/when we get there. From I've read so far, it seems good for 'bridging the gap' from the study of dependent type theory from a 'programming languages route', to the more recent work that has been in 'homotopy type theory' - involving people coming from both programming-languages-style-type-theory, category theory and algebraic topology backgrounds.
http://dlicata.web.wesleyan.edu/pubs/thesis/thesis.pdf
Have a look if interested!
(Not sure the extent that the member's of our study group are interested in 'homotopy type theory', etc., but I think it would be cool if that's eventually sort of where we go with all of this.)
-Mark
I've been taking a look at some of Daniel Licata's work with Robert Harper. Of the work that I've had a look at so, chapter's seven and eight of Licata's PhD seems like a good, digestible introduction to 'computational higher type theory', if/when we get there. From I've read so far, it seems good for 'bridging the gap' from the study of dependent type theory from a 'programming languages route', to the more recent work that has been in 'homotopy type theory' - involving people coming from both programming-languages-style-type-theory, category theory and algebraic topology backgrounds.
http://dlicata.web.wesleyan.edu/pubs/thesis/thesis.pdf
Have a look if interested!
(Not sure the extent that the member's of our study group are interested in 'homotopy type theory', etc., but I think it would be cool if that's eventually sort of where we go with all of this.)
-Mark
Mark Farrell
Dec 12, 2015, 4:21:51 PM12/12/15
to Type Theory Study Group
Sorry for the grammatical errors.
Alex Moore - Niemi
Jan 5, 2016, 9:02:33 PM1/5/16
to Type Theory Study Group
this is quite interesting to me so far -- thanks for the share
On Saturday, December 12, 2015 at 3:41:18 PM UTC-5, Mark Farrell wrote:
Reply all
Reply to author
Forward
0 new messages