How Isabelle emerged from the trends of the 1980s
https://lawrencecpaulson.github.io/2022/07/13/Isabelle_influences.html

Hygienic Macro Technology (PDF, 2020), by William D Clinger and Mitchell Wand. “In this paper, we summarize that early history with greater focus on hygienic macros, and continue the story by describing the further development, adoption, and influence of hygienic and partially hygienic macro technology in Scheme.”

https://dl.acm.org/doi/pdf/10.1145/3386330

ML 2021: A metalanguage for multi-phase modularity, by Sterling and Harper (2021)
https://www.youtube.com/watch?v=5kWS-umBA7k

Programming Language Semantics: It’s Easy As 1, 2, 3
by Graham Hutton, 2021

comment: INTRODUCTORY ARTICLE

http://www.cs.nott.ac.uk/~pszgmh/123.pdf

‘do’ Unchained: Embracing Local Imperativity in a Purely Functional Language (Functional Pearl)
S. Ullrich, L. de Moura, 2022
https://leanprover.github.io/papers/do.pdf

Software eco-design: investigating and reducing the energy consumption of software
by Zakaria Ournani, 2022
https://tel.archives-ouvertes.fr/tel-03554712/document

We’ve just released a major milestone of Unison, version M4
Anyone can now self-publish code to http://share.unison-lang.org
<...>
We just launched our code-hosting platform!
It's like Github, but has hyperlinked syntax-highlighted code and docs from day one

https://twitter.com/unisonweb/status/1547953084394979329

ICYMI. Led by @clayrat https://www.tg-me.com/covalue/58

John Baez завел канал на ютубе, https://www.youtube.com/playlist?list=PLuAO-1XXEh0ZiJlRKz7EuODAdIOjC5-1l

Москвин, весна 2022
https://youtube.com/playlist?list=PLlb7e2G7aSpTDub2LFDVBvvjWj-53Gfuh

https://arxiv.org/abs/2203.15426 Dal Lago, Gavazzo, Ghyselen, [2022] "On Reinforcement Learning, Effect Handlers, and the State Monad"

We study the algebraic effects and handlers as a way to support decision-making abstractions in functional programs, whereas a user can ask a learning algorithm to resolve choices without implementing the underlying selection mechanism, and give a feedback by way of rewards. Differently from some recently proposed approach to the problem based on the selection monad [Abadi and Plotkin, LICS 2021], we express the underlying intelligence as a reinforcement learning algorithm implemented as a set of handlers for some of these algebraic operations, including those for choices and rewards. We show how we can in practice use algebraic operations and handlers -- as available in the programming language EFF -- to clearly separate the learning algorithm from its environment, thus allowing for a good level of modularity. We then show how the host language can be taken as a lambda-calculus with handlers, this way showing what the essential linguistic features are. We conclude by hinting at how type and effect systems could ensure safety properties, at the same time pointing at some directions for further work.

“CoqQ: Foundational Verification of Quantum Programs”

Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying (2022)

https://arxiv.org/abs/2207.11350

CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (mathcomp and mathcomp analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.

#coq #quantum_programming

Эта небольшая заметка посвящена нескольким новостям по нашей тематике.

Во-первых, хочу напомнить, что в июне прошла конференция PLDI 2022 и многие из представленных там работ имеют компиляторную тематику. Вот программа конференции: https://pldi22.sigplan.org/program/program-pldi-2022/

Во-вторых, давайте поговорим о весьма достойных книгах, которые официально только готовятся к печати и выйдут в 2022-2023 гг.

Нас ждет третье издание классики Engineering a Compiler. Второе издание вышло в 2012 году и мне, увы, пока не удалось установить, в чем же особенности нового издания. Судя по всему, новая версия знаменитого учебника выйдет в этом сентябре: https://www.amazon.com/Engineering-Compiler-Keith-D-Cooper/dp/0128154128

В феврале 2023 года выйдет Essentials of Compilation в издательстве MIT: https://mitpress.mit.edu/books/essentials-compilation Материал в разных редакциях давно уже публиковался на github: https://github.com/IUCompilerCourse/Essentials-of-Compilation

Еще одна довольно известная онлайн-книга скоро будет напечатана. Речь об SSA Book. Официально она теперь называется SSA-based Compiler Design: https://link.springer.com/book/9783030805142 Ждем ее ближе к февралю 2023 года.

Наконец, упомяну о настоящем "долгострое": новой версии классики Programming Languages: An Interpreter-Based Approach" от Samuel Kamin. Новый автор и известный компьютерный ученый, Norman Ramsey, работал над своей версией еще, кажется, с 2005 года. На протяжении многих лет черновые варианты учебника адресно рассылались отдельным профессорам в разных университетах. И, вот, наконец, в этом октябре книга под официальным названием Programming Languages Build, Prove, and Compare будет напечатана: https://www.cambridge.org/ru/academic/subjects/computer-science/programming-languages-and-applied-logic/programming-languages-build-prove-and-compare

Good overview of some entertaining stuff, by Xavier Leroy: https://xavierleroy.org/CdF/2018-2019/

Other courses are good as well (though the presentation is usually more deep/technical):
- https://xavierleroy.org/CdF/2020-2021/
- https://xavierleroy.org/CdF/2019-2020/
- https://xavierleroy.org/mpri/2-4/
- other materials at https://xavierleroy.org/teaching.html

Mathematical Proof Between Generations

https://arxiv.org/pdf/2207.04779.pdf

A Formalization of SQL with Nulls (Wilmer Ricciotti, James Cheney):

https://cs.paperswithcode.com/paper/a-formalization-of-sql-with-nulls

> SQL is the world's most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification. Commercial SQL implementations interpret the standard in different ways, so that, given the same input data, the same query can yield different results depending on the SQL system it is run on. Even for a particular system, mechanically checked formalization of all widely-used features of SQL remains an open problem. The lack of a well-understood formal semantics makes it very difficult to validate the soundness of database implementations. Although formal semantics for fragments of SQL were designed in the past, they usually did not support set and bag operations, lateral joins, nested subqueries, and, crucially, null values. Null values complicate SQL's semantics in profound ways analogous to null pointers or side-effects in other programming languages. Since certain SQL queries are equivalent in the absence of null values, but produce different results when applied to tables containing incomplete data, semantics which ignore null values are able to prove query equivalences that are unsound in realistic databases. A formal semantics of SQL supporting all the aforementioned features was only proposed recently. In this paper, we report about our mechanization of SQL semantics covering set/bag operations, lateral joins, nested subqueries, and nulls, written in the Coq proof assistant, and describe the validation of key metatheoretic properties. Additionally, we are able to use the same framework to formalize the semantics of a flat relational calculus (with null values), and show a certified translation of its normal forms into SQL.

An assortment of curious mathematical pieces.

A la POPLOG: https://kam.mff.cuni.cz/~matousek/stml-53-matousek-1.pdf

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

Demos of projectional editors for functional languages: Lamdu, Dark, Hazel, tylr and Lisperanto. Also a link to the whole meetup video is in the description.