Fregel: a functional domain-specific language for vertex-centric large-scale graph processing

https://www.cambridge.org/core/journals/journal-of-functional-programming/article/fregel-a-functional-domainspecific-language-for-vertexcentric-largescale-graph-processing/A6D4FC0B42C87B752E9AF88F681C5F13

Обзор работ и достижений по языку MPL (Parallel ML on top of MLton) для неявного параллелизма в функциональном языке использующем fork-join framework. Главная идея — привязка (куска) кучи к выполняемой (параллельной) задаче, что делает данные в этих кучах независимыми и обрабатываемыми полностью параллельно. Для эффективного выполнения на железе эти подкучи объединяются в более крупные независимые блоки через посредство heap scheduler, работающего в связке с (work-stealing) task scheduler. Приведены ссылки на статьи, замеры и исходники реализации.

Learning Computer Science With Categories

The first book in Bob Coecke’s series on applied category theory is out, and the pdf is free — legally, even! — until 8 February 2022.

https://golem.ph.utexas.edu/category/2022/01/learning_computer_science_with.html

https://github.com/Kindelia/HVM и еще один параллельный рантайм на сетях взаимодействия от виктора майя

DeepMind выпустил AlphaCode, который прогает лучше половины твоих знакомых.

Во многом похож на Codex, но есть отличия.

Основной подход:
1. Encoder-decoder, 41B параметров
1. Декодер обучается предсказывать следующее слово, а энкодер делает MLM. Всё end2end.
1. Заскрапили датасет задачек с Codeforces и зафайнтюнили на нём модель
1. Во время тестирования семплили очень большое количество решения (до миллиона) и потом выбирали из них с помощью кластеризации, эвристик и, самое главное, проходят ли они открытые тесты которые приложены к задачке. Сабмитили на финальную проверку только топ-10.

По результатам: AlphaCode решает задачки лучше, чем 54% пользовалетей Codeforces (не очень альфа пока что, но стремится туда).

Небольшие технические отличия от Codex:
1. Максимальная длина для энкодера 1536, для декодера 768
1. Использовали Multi-query attention, модификацию attention, которая использует одни и те же K и V для разныех голов – позволило улучшить потребление памяти и скорость декодирования
1. Очень маленький словарь токенизатора, 8К.
1. Во время файтнюнинга использовали температуру 0.2, которая делает распределение более острым. При тесте температура не использовалась, назвали это tempering.
1. Файнтюнились и на правильных и на неправильных решениях, при этом моделе заранее сообщается сигнал корректное ли это решения.
1. Для файнтюнинга использовали лосс, который называется GOLD. По сути это взвешенная кросс-энтропия, несмотря на то, что выглядит как RL.

Вот тут можно посмотреть на визуализацию attention, а ещё есть популярно написанный блогпост

Олега ответ https://medium.com/@odomontois/several-days-ago-we-saw-the-new-experimental-feature-called-capture-checking-was-announced-in-e4aa9bc4b3d1

https://dlnext.acm.org/doi/abs/10.1145/3498886.3502201 Biri, [2022] "Dependent tagless final"

https://github.com/idris-lang/Idris2/blob/main/libs/papers/Language/Tagless.idr

# Лялямбда 22 — Call for Prepods

Летом пройдёт школа по формальной верификации и функциональному программированию. Приходите преподавать и жечь петухов.

Школа будет идти две недели: это два недельных интенсива друг за другом, ориентировочно в июле. Даты и место сейчас выбираем.

Интенсивы будут в несколько потоков: можно предложить что-то как для матёрых верификаторов, так и для начинающих хаскеллят. Хорошо идут минипроекты.

Податься просто, как 1-2-3:

1. Заполните [анкету курса](https://docs.google.com/forms/d/e/1FAIpQLSdjVSLijWI4H7iN5HJ2jz1ukZve_YYhKo9KqrNRNcJ3cxM2xw/viewform) (с кратким описанием, требованиям к участникам, т.п.) и посмотрите на анкеты курсов коллег.
2. Выберите время для звонка с нами. Будем встраивать курс в общую программу.
3. Приезжайте на офлайн-педсовет. Задача педсовета — познакомиться, синхронизироваться по тому, что хотим донести, культурным взглядам, художественным вкусам, собраться в стройную боевую единицу и зарядиться силой весны.

Сориентироваться, как было в прошлый раз, можно [тут](https://lalambda.school); задавать вопросы можно @AntonTrunov; приезжайте, будем рады.

Если хотите быть students, а не prepods, мы скоро откроем регистрацию и напишем в [канале школы](https://www.tg-me.com/lalambdaschool).

В Inria порываются создать пиринговую сеть сертифицированных машинных доказательств: https://www.inria.fr/en/towards-internet-proof
Звучит, конечно, классно, но что-то мне сомнительно, что это будет пользоваться популярностью в обозримом будущем...

Janet is a functional and imperative programming language and bytecode interpreter. It is a lisp-like language, but lists are replaced by other data structures (arrays, tables (hash table), struct (immutable hash table), tuples). The language also supports bridging to native code written in C, meta-programming with macros, and bytecode assembly.

https://github.com/janet-lang/janet

https://www.hytradboi.com/
Super cool online one-day conference around Databases topics organized by pretty well-known Jamie Brandon. Look at the speakers, there are familiar names too.

Вдруг кто-то мечтал освоить биоинформатику за 21 день 3 дня.

https://rsmu.ru/structure/edu-dept/mbf/bioinf-school/

А вы знали про https://learn-idris.net/play ? Там даже можно переключаться между первым и вторым! 😃

Доклады Scala Love 2022 https://youtube.com/playlist?list=PLBqWQH1MiwBTMk9HV-RNN7sQpB9ZPi_Az

https://proofassistants.stackexchange.com/a/940/333

This answer is golden, it links to all of the best materials on Type Theory and related subjects.

https://press.princeton.edu/books/paperback/9780691145990/how-mathematicians-think

"How Mathematicians Think: Using Ambiguity, Contradiction, and Paradox to Create Mathematics"

Sounds like serious fun! 😁