United Monoids: Finding Simplicial Sets and Labelled Algebraic Graphs in Trees, 2022
A. Mokhov

https://arxiv.org/abs/2202.09230

HasChor: Functional Choreographic Programming for All (Functional Pearl), 2023

G. Shen, S. Kashiwa, L. Kuper
https://arxiv.org/abs/2303.00924

[PADL'23] Modern Macros
Robert Findler

https://www.youtube.com/watch?v=YMUCpx6vhZM

Mechanised Metamathematics
An Investigation of First-Order Logic and Set Theory in Constructive Type Theory, 2022
D. Kirst

https://www.ps.uni-saarland.de/~kirst/thesis/

Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
N. Zilberstein, D. Dreyer, A. Silva

https://arxiv.org/abs/2303.03111

Verus: Verifying Rust Programs using Linear Ghost Types
A. Lattuada et al

https://arxiv.org/abs/2303.05491

A Half Century of Formal Methods
D. Bjørner, K. Havelund

https://www.havelund.com/Publications/fm-50-2022.pdf

Updated: The Verse Calculus: a Core Calculus for Functional Logic Programming

36 pages of changed/new stuff.

Authors: The same guys plus a new guy, Guy Steele.

https://simon.peytonjones.org/assets/pdfs/verse-March23.pdf

Dana Scott: Seventy years using fixed points

https://youtu.be/jHJE9GoFZCY

CALL FOR PREPODS

В начале июля под Тбилиси пройдёт школа сложного программирования lalambda.school. Приходите рассказывать про ФП, верификацию, железо, купаться и жечь петухов.

Школа идёт семь дней: в дне семь пар, четыре из которых идут на гомотопическую теорию типов, синтез звука, движки регулярных выражений, теорию оптимизации, введение в FPGA, и ray tracing на SQL; а оставшиеся три на григорианскую акапеллу, театральную импровизацию, хайкинг по деревьям, тиктоки короткого метра, столярное мастерство и груминг лошадей. Ещё будут рейв и хакатон.

Площадка — пятизвёздочная конструкция у Тбилисского Моря: на природе и в 20 минутах от аэропорта.

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

Аудитория школы — студенты, которые ищут темы за страницами учебника с сочными и неожиданными применениями; профессиональные программисты, которые хотят выглянуть из тасков джиры в полёт академической и арт-фантазии; и бывшие программисты, которые стали менеджерами или учёными, и хотят по хардкору тряхнуть стариной. И все отлично умеют программировать, поэтому можно рассказывать сразу про свой предмет.

Чтобы податься, напишите пару слов про курс — краткое описание, требования к участникам — в форму. @AntonTrunov вам перезвонит.

Если хотите быть students, а не prepods, мы скоро окончательно подтвердим даты и откроем регистрацию. Апдейт будет в канале школы.

Teaching Category Theory to Computer Scientists

https://blog.sigplan.org/2023/04/04/teaching-category-theory-to-computer-scientists/

Друзья! Мы рады анонсировать новую школу

\ | | | /
— Лялямбда —
/ | | | \

15-23 июля в получасе от Тбилиси пройдёт летняя школа сложного программирования и современного искусства «Лялямбда».

День на школе — это семь пар: четыре пары курса и три арт-попурри.

В этом году на школе будут курсы не только про формальные методы, странные логики спецификации и ФП, но и про стэйт оф зэ арт теории музыки и проектирование микропроцессоров.

В арте будут перформансы и джемы, утренняя йога, лежать на пуфике и слушать музыку, стоять на руках, плавать под водой, танцевать хип-хоп или танго, гулять по берегу озера — можно выбирать.

В этот раз мы в модном отеле на озере. До среды открыта ранняя регистрация: здесь можно зарегистрироваться, здесь запросить грант, если он вам нужен, а здесь подать курс, мы помогаем их готовить. Вопросики можно писать @lalambda_bot.

Yaay, tail calls

https://v8.dev/blog/wasm-tail-call

Foundational distributed systems papers (2021) (Score: 152+ in 1 day)

Link: https://readhacker.news/s/5Ch5c
Comments: https://readhacker.news/c/5Ch5c

Patterns of data flow in words: Learning APL ideas without APL syntax

https://okmij.org/ftp/Computation/ARPL.html

Better Together: Unifying Datalog and Equality Saturation

Yihong Zhang, Yisu Remy Wang, Oliver Flatt, David Cao, Philip Zucker, Eli Rosenthal, Zachary Tatlock, Max Willsey

egglog unifies both Datalog and EqSat style fixpoint reasoning. From the perspective of a Datalog programmer, egglog adds fast and extensible equivalence relations that still support key database optimizations like query planning and semi-naive evaluation.

egglog is implemented in approximately 4,200 lines of Rust https://github.com/mwillsey/egg-smol

https://arxiv.org/abs/2304.04332