Oℕ
Size: a a a
2020 February 27
Oℕ
Далеко шутка зашла
R
Лучше скажи что хорошо себя чувствуешь
ὦ
Спасибо
Ты молодой шутливый
ὦ
Не стоит лучше вскрывать эту тему
R
ὦan
Не стоит лучше вскрывать эту тему
ὦ
если бросишь писать монады по утрам
R
ὦan
если бросишь писать монады по утрам
Чистое велью пишу без монад, пью отвратительный флет уайт
w
Чистое велью пишу без монад, пью отвратительный флет уайт
В моменте.
SK
@skucherenko @clayrat скожите было ли что-то после этого http://www.cs.ox.ac.uk/jeremy.gibbons/publications/progorn.pf
Это стейт оф зе арт?
Это стейт оф зе арт?
Было вроде после 16-го, гляну
Oℕ
Было вроде после 16-го, гляну
спасибо
AT
@skucherenko @clayrat скожите было ли что-то после этого http://www.cs.ox.ac.uk/jeremy.gibbons/publications/progorn.pf
Это стейт оф зе арт?
Это стейт оф зе арт?
в 2019 на itp вот это было -- https://drops.dagstuhl.de/opus/volltexte/2019/11081/pdf/LIPIcs-ITP-2019-26.pdf
Ornaments for Proof Reuse in Coq
Ornaments for Proof Reuse in Coq
SK
от мужика, который с макбрайдом про категориальные основания писал, было https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/journal-2013-catorn-jfp/paper.pdf
SK
но уже без макбрайда
AT
вообще вроде много публикуют, судя по гугл школяру https://scholar.google.com/scholar?q=ornaments+dependent+types&hl=en&as_sdt=0%2C5&as_ylo=2017&as_yhi=
AT
много -- это штук 5-10 релевантных)
SK
да, самое оно - взять пару-тройку новых и отреверсить по референсам за промежуток 17-19