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

Для Scala.js разработали новый плагин для hot reload: https://www.scala-lang.org/blog/2023/04/18/faster-scalajs-development-with-frontend-tooling.html
В отличии от старого scalajs-bundler, который работал с webpack, новая разработка нацелена на Vite.
А вы пробовали этот бандлер?

Logic, Optimization, and Constraint Programming: A Fruitful Collaboration

There are deep connections between logic, optimization, and constraint programming (CP) that underlie some of the most effective solution methods. Conflict clause generation in SAT algorithms, as well as SAT modulo theories, are forms of Benders decomposition, a classical optimization method that can itself be generalized by viewing it as based on logical inference. The resolution method for logical inference is intimately related to the core concept of cutting planes in integer programming (IP), as well as to Fourier-Motzkin elimination, which lies at the root of linear programming (LP) and ultimately network flow models that play an essential role in CP’s filtering techniques. In first order logic, Herbrand’s theorem is based on a compactness property that is perfectly mirrored in IP, while CP is based on a generalization of unification. Boole’s probability logic poses an LP problem that can be solved by column generation, while default and nonmonotonic logics have natural IP models. Binary decision diagrams, used for logic circuit design, provide the basis for recent developments in both CP and combinatorial optimization. The concept of consistency in CP inspires a reinterpretation of cutting planes in IP.

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