RN
у кого назрело?
Size: a a a
2021 February 02
RN
у меня есть один докладик
RN
если немного - можно у нас
RN
Главное запишите для тех у кого нет антител)
ок
2021 February 03
IT
В целом, я, конечно, соскучился по движухе (наконец-то, а то я загасился конкретно в последние годы). Но мне поделиться нечем, кроме как немного пожаловаться.
RN
тоже опыт
DG
Не так давно в канале можно было делать ссылку на чатик для обсуждения
Кажется, что это не так — меня там нет)
По крайней мере я не знаю, что я там есть)
По крайней мере я не знаю, что я там есть)
AV
Ну это про все каналы, а канал где есть те кому не пофиг на мое нытьё гипотетический, все равно 0 человек будет
DG
В среду, 3 февраля, в Спейсе (Воронцово поле, 5/7с8, Москва) в 20:00 Денис Буздало́в (ИСП РАН) сделает доклад о Quantitative Type Theory и о ее применении.
Также будет трансляция, ссылка на которую появится в канале за 10мин до начала.
QTT — это расширение системы типов для языков программирования со строгой типизацией, которая позволяет в сигнатурах функций уточнять когда может использоваться тот или иной параметр, тем самым давая более точные обещания пользователю функции или сужая возможные реализации для того, кто эту функцию пишет. В частности, таким образом можно избегать определённого рода ошибок в программах.
Для людей, знакомых с линейными типами (например, знакомых с Rust), можно сказать, что QTT — это обобщение линейных типов, которое, правда, в отличие от Rust, в докладе будет рассматриваться на примере функциональных языков.
Изложение будет лежать в практической плоскости: будет рассказано не о самой теории типов QTT как таковой, а о применении этой теории типов — о том, что можно специфицировать в языках, в основе которых лежит QTT
QTT лежит в основе системы типов Idris 2, примеры в докладе будут использовать синтаксис Idris.
Основная статья по QTT:
Robert Atkey. The Syntax and Semantics of Quantitative Type Theory. 2018.
https://bentnib.org/quantitative-type-theory.pdf
Также будет трансляция, ссылка на которую появится в канале за 10мин до начала.
QTT — это расширение системы типов для языков программирования со строгой типизацией, которая позволяет в сигнатурах функций уточнять когда может использоваться тот или иной параметр, тем самым давая более точные обещания пользователю функции или сужая возможные реализации для того, кто эту функцию пишет. В частности, таким образом можно избегать определённого рода ошибок в программах.
Для людей, знакомых с линейными типами (например, знакомых с Rust), можно сказать, что QTT — это обобщение линейных типов, которое, правда, в отличие от Rust, в докладе будет рассматриваться на примере функциональных языков.
Изложение будет лежать в практической плоскости: будет рассказано не о самой теории типов QTT как таковой, а о применении этой теории типов — о том, что можно специфицировать в языках, в основе которых лежит QTT
QTT лежит в основе системы типов Idris 2, примеры в докладе будут использовать синтаксис Idris.
Основная статья по QTT:
Robert Atkey. The Syntax and Semantics of Quantitative Type Theory. 2018.
https://bentnib.org/quantitative-type-theory.pdf
Где же ссылка?)
DG
Ещё не начали(
Не начали сам доклад или трансляцию?
Если доклад, то и ладно — я бы пока всем интересующимся знакомым отправил ссылку.
Если трансляцию — тогда ждём)
Если доклад, то и ладно — я бы пока всем интересующимся знакомым отправил ссылку.
Если трансляцию — тогда ждём)
DG
Будет ближе к 20:15
Понял, спасибо!
p
А запись будет?