to post messages and comments.

может быть ван Рой и неглупый чувак, но этот его моцарт какое-то мудацкое говно, которое хрен скомпиляешь, не говоря уже о юзабилити (плюнул и скачал бинарник в итоге)

Роберт Харпер в CMU проводит семинар по Homotopy Type Theory (HoTT, homotopytypetheory.org ) — cs.cmu.edu [15-819 Advanced Topics in Programming Languages, Fall 2013]

Утверждается, что курс self-contained, в доп.литературу вынесено только "Programming in Martin-Löf's Type Theory" [ cse.chalmers.se ]

Имеются также и видеозаписи с Харпером у доски, но там "Silverlight is required to use the Panopto viewer". Худо-бедно показывает, mp4 ничего не мешает выдернуть со страницы.

да... чот с калтеком лажевато выходит — поток ustream периодически затыкается, слайдов не видать, об ускоренной перемотке даже не стоит упоминать, видимо... МИТ рулит по сравнению с ними (хотя ютюб тоже иногда выдумывает потупить, но для оффлайна это похрен)

чтот как-то Caltech несколько стремает — в форме регистрации нажал кнопку отправки формы — отобразило сообщение от ошибке на странице ("registration failed" вроде), но сабмит прошёл и показало "success". Интересно насколько курс будет лажать.

Последние пару месяцев, я начал слушать/смотреть лекции на iTunesU. Делюсь ссылками, на лекции с видео записями:
Oxford: Quantum Physics – deimos3.apple.com
MIT: Classical Physics – deimos3.apple.com
MIT: Electricity and Magnetism – deimos3.apple.com
MIT: Blach Holes and General Relativity – deimos3.apple.com
MIT: Multicore Programming – deimos3.apple.com
MIT: Intoduction to Algorithms (ОЧЕНЬ РЕКОМЕНДУЮ!) – deimos3.apple.com