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.

https://journals.plos.org/plosone/article?id=10.1371/journal.pone.0115069

The choice of an efficient document preparation system is an important decision for any academic researcher. To assist the research community, we report a software usability study in which 40 researchers across different disciplines prepared scholarly texts with either Microsoft Word or LaTeX. The probe texts included simple continuous text, text with tables and subheadings, and complex text with several mathematical equations. We show that LaTeX users were slower than Word users, wrote less text in the same amount of time, and produced more typesetting, orthographical, grammatical, and formatting errors. On most measures, expert LaTeX users performed even worse than novice Word users. LaTeX users, however, more often report enjoying using their respective software. We conclude that even experienced LaTeX users may suffer a loss in productivity when LaTeX is used, relative to other document preparation systems.

O-oh, it's so disheartening! 😢
#latex #msword #study #paper

Выложили записи всех трёх частей "Towards third generation HOTT":

* Part 1: Basic syntax (slides)
* Part 2: Symmetries and semicartesian cubes (slides)
* Part 3: Univalent universes (slides)

Андрей Бауэр выложил черновик лекций по реализуемости:

http://www.andrej.com/zapiski/MGS-2022/notes-on-realizability.pdf Bauer, [2022] "Notes on realizability"

Реализуемость можно понимать как более слабую/обобщенную версию соответствия Карри-Говарда, т.е. идеи о том что логические доказательства можно интерпретировать как программы - в случае реализуемости не обязательно тотальные или даже типизированные.

hexdump4s: building a simple command line application using scodec and scala-cli https://github.com/scodec/hexdump4s/blob/main/README.md

Tree Automata Techniques and Applications

https://hal.inria.fr/hal-03367725

http://philsci-archive.pitt.edu/19634/ Papayannopoulos, [2020] "Unrealistic Models for Realistic Computations: How Idealisations Help Represent Mathematical Structures and Found Scientific Computing"