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! 😁

Program Analysis of Probabilistic Programs
Maria I. Gorinova


https://arxiv.org/abs/2204.06868

Наверное все знают, но на Степике есть очень много бесплатных курсов по математике. Вот весть каталог https://stepik.org/catalog/6

Namespaced DeBruijn Indices By Gabriella Gonzalez https://watch.softinio.com/w/tgDXLAUEAhGooiJiskwCFy

Verified Textbook Algorithms
A Biased Survey
Tobias Nipkow and Manuel Eberl and Maximilian P. L. Haslbeck

https://www21.in.tum.de/~nipkow/pubs/atva20.pdf

Габриэла Гонзалез (широко известная в мире Хаскеля) написала хороший пост про то, как окунуться в теорию типов
https://www.haskellforall.com/2022/05/introductory-resources-to-type-theory.html

https://github.com/liquid-rust/liquid-rust

http://goto.ucsd.edu:8091/index.html

жидкие типы для раста

#prog #parsing #article

Faster general parsing through context-free memoization (pdf, thanks @zukaboo)

(thanks @grammarware, @GabrielFallen)

We present a novel parsing algorithm for all context-free languages. The algorithm features a clean mathematical formulation: parsing is expressed as a series of standard operations on regular languages and relations. Parsing complexity w.r.t. input length matches the state of the art: it is worst-case cubic, quadratic for unambiguous grammars, and linear for LR-regular grammars. What distinguishes our approach is that parsing can be implemented using only immutable, acyclic data structures. We also propose a parsing optimization technique called context-free memoization. It allows handling an overwhelming majority of input symbols using a simple stack and a lookup table, similarly to the operation of a deterministic LR(1) parser. This allows our proof-of-concept implementation to outperform the best current implementations of common generalized parsing algorithms (Earley, GLR, and GLL). Tested on a large Java source corpus, parsing is 3–5 times faster, while recognition—35 times faster.

Честно скажу, я прочитал по диагонали, но фактически алгоритм выглядит, как parsing with derivatives, но сделанный правильно.

Нашел два интересных обзорных эссе о теории доменов в прошлогоднем бюллетене от британской группы по формальным методам BCS-FACS:

* Monahan, [2021] "Domain Theory - Revisited"
* Winskel, [2021] "Domain theory and interaction"

Первое эссе за авторством Монахана даёт обзор мотивации, контекста появления и основных идей теории доменов. Рассказывается о преодолении недоверия к нетипизированному лямбда-исчислению, поиске способов масштабирования и подходов к спецификации программ, о необходимости работы с частичными (из-за общей рекурсии) функциями.

Ключевая идея теории доменов - функции ЛИ соответствуют математическим функциям над особыми множествами (собственно, доменами, которые моделируют типы), упорядоченными по количеству содержащейся в ней абстрактной информации, причем функции сохраняют этот порядок. Подобная структура функций позволяет конструировать неподвижные точки для них и таким образом моделировать рекурсию как предел нарабатывающего информацию процесса. Так впервые был выстроен топологический взгляд на вычисления, и информатика (точнее, теория языков программировании) оказалась полноценной математической теорией, а не просто "двиганием битов", что в свою очередь дало толчок развитию теорий типов и формальных семантик.

Эссе Винскеля более техническое и фокусируется на теме конкурентных и взаимодействующих вычислений. Начинается оно с введения в историю ТД с точки зрения её создателей, упоминает о создании LCF/PCF и ML, затем переходит к классическим проблемам ТД - работа с нондетерминизмом, проблема полной абстракции (конструкции в модели, для которых не существует синтаксиса). Пытаясь решить эти проблемы, теория доменов (и денотационная семантика в целом) перешла к созданию интерактивных моделей, в дальнейшем оформившихся в виде игровой семантики. С другой стороны, из-за проблем при работе с конкурентными программами, часть исследователей переключилась на алгебры процессов CCS/CSP с синхронизацией. Тем временем продолжение работ в рамках теории порядков привело к созданию понятия структуры событий (формализацию которых на Coq, кстати, можно найти тут).

Дальше эссе подчеркивает связи с теорией категорией - предпучки, моноидальные категории, затрагивает связи с работами Жирара, описывает появление игровой семантики и её конкурентной разновидности - где одновременно и игры (модели типов), и стратегии (модели программ) описываются структурами событий (в отличие от классических игр на деревьях), показывает как свести конкурентные игры к доменным моделям, геометрии взаимодействия и линзам.

Writing portable code is hard: https://www.chemistryworld.com/news/structures-in-more-than-150-papers-may-be-wrong-thanks-to-nmr-coding-glitch/4010413.article

The error is the result of a simple file sorting problem. On operating systems without default file name sorting, the script fails to match the files containing a conformer’s free energy with its chemical shift – leading to an overall wrong value.

Which meant the script worked fine on Windows while producing incorrect results on GNU/Linux. This jeopardizes some 150 chemistry papers.