NP
Очень тупой вопрос: компилятор/интерпретатор cubicaltt'a существует в природе?
Size: a a a
2017 November 03
2017 November 06
TN
Пацаны, бухаем, официально мы комитеры в самый крутой прувер на планете Земля: https://github.com/mortberg/cubicaltt/pull/86 🖖🎉
2017 November 07
TN
#kievfprog Fall 2017 is finally here!
The event will be headlined by Vitaly Bragilevsky with a 2-hour lecture on Idris and Dependent Types, picked up by Maxim Sokhatsky who will feature his recent Groupoid Infinity project work on cubicaltt and carried on by Sergey Vinokurov and Andrew Lelechenko with Recursion Schemes and Number Theory in Haskell!
See you next week Institute of Mathematics of the National Academy of Sciences of Ukraine at 11 am on Saturday, November 18 and do not forget to register!
https://www.eventbrite.com/e/kievfprog-fall-2017-tickets-39509911208
The event will be headlined by Vitaly Bragilevsky with a 2-hour lecture on Idris and Dependent Types, picked up by Maxim Sokhatsky who will feature his recent Groupoid Infinity project work on cubicaltt and carried on by Sergey Vinokurov and Andrew Lelechenko with Recursion Schemes and Number Theory in Haskell!
See you next week Institute of Mathematics of the National Academy of Sciences of Ukraine at 11 am on Saturday, November 18 and do not forget to register!
https://www.eventbrite.com/e/kievfprog-fall-2017-tickets-39509911208
VS
#kievfprog Fall 2017 is finally here!
The event will be headlined by Vitaly Bragilevsky with a 2-hour lecture on Idris and Dependent Types, picked up by Maxim Sokhatsky who will feature his recent Groupoid Infinity project work on cubicaltt and carried on by Sergey Vinokurov and Andrew Lelechenko with Recursion Schemes and Number Theory in Haskell!
See you next week Institute of Mathematics of the National Academy of Sciences of Ukraine at 11 am on Saturday, November 18 and do not forget to register!
https://www.eventbrite.com/e/kievfprog-fall-2017-tickets-39509911208
The event will be headlined by Vitaly Bragilevsky with a 2-hour lecture on Idris and Dependent Types, picked up by Maxim Sokhatsky who will feature his recent Groupoid Infinity project work on cubicaltt and carried on by Sergey Vinokurov and Andrew Lelechenko with Recursion Schemes and Number Theory in Haskell!
See you next week Institute of Mathematics of the National Academy of Sciences of Ukraine at 11 am on Saturday, November 18 and do not forget to register!
https://www.eventbrite.com/e/kievfprog-fall-2017-tickets-39509911208
А будет стрим?
TN
Стрима не будет, будет запись.
VS
Здорово
NK
Написал заметку-отчет по своим разбирательствам с cubicaltt: https://nponeccop.livejournal.com/581276.html
2017 November 08
TN
Андрей и я хотим для разминки закодировать этот пейпер в кубикале
NK
в процессе работы модуляризируем стдлибу cubicaltt, которая писалась учоными и достаточно безобразна с точки зрения программиста
2017 November 09
NK
NK
случайно нашел но должно быть полезно
2017 November 10
TN
В копилочку литературы по индуктивным типам
TN
1. A.Berarducci. Automatic Synthesis of Typed Lambda-Programs. 1985
2. F.Pfenning. Inductively defined types in the CoC. 1989
3. P.Wadler. Recursive types for free. 1990
4. N.Gambino. Wellfounded Trees and Dependent Polynomial Functors. 1995
5. P.Dybjer. Inductive Famalies. 1997
6. B.Jacobs. (Co)Algebras and (Co)Induction. 1997
7. V.Vene. Categorical programming with (co)inductive types
8. H.Geuvers. Dependent (Co)Inductive Types are Fibrational Dialgebras. 2015
2. F.Pfenning. Inductively defined types in the CoC. 1989
3. P.Wadler. Recursive types for free. 1990
4. N.Gambino. Wellfounded Trees and Dependent Polynomial Functors. 1995
5. P.Dybjer. Inductive Famalies. 1997
6. B.Jacobs. (Co)Algebras and (Co)Induction. 1997
7. V.Vene. Categorical programming with (co)inductive types
8. H.Geuvers. Dependent (Co)Inductive Types are Fibrational Dialgebras. 2015
2017 November 12
TN
Кюрен (автор КАМ), Категорная Семантика зависимых типов в струнных диаграмах, классика. 1993
https://www.irif.fr/~curien/substitution.pdf
https://www.irif.fr/~curien/substitution.pdf
2017 November 15
TN
T. Coquand. Equality and dependent type theory
http://www.cse.chalmers.se/~coquand/equality.pdf
http://www.cse.chalmers.se/~coquand/equality.pdf
TN
Хороший PhD тезис как введение в завтипы
https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/thesis-2011-phd/thesis.pdf
https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/thesis-2011-phd/thesis.pdf
TN
Вторая глава David Aspinall and Martin Hofmann из книги
Advanced Topics in Types and Programming Languages
http://cs.swan.ac.uk/~cspt/DependentTypes.pdf
Advanced Topics in Types and Programming Languages
http://cs.swan.ac.uk/~cspt/DependentTypes.pdf
TN
Известная статья МакБрайда Datatypes of Datatypes, 2015
https://www.cs.ox.ac.uk/projects/utgp/school/conor.pdf
https://www.cs.ox.ac.uk/projects/utgp/school/conor.pdf