Breadth−First Traversal Via Staging
by Jeremy Gibbons‚ Oisin Kidney‚ Tom Schrijvers and Nicolas Wu
https://www.cs.ox.ac.uk/publications/publication14875-abstract.html

Aeneas: Rust Verification by Functional Translation
by Son Ho, Jonathan Protzenko
https://arxiv.org/abs/2206.07185

https://uwo.ca/math/faculty/kapulkin/seminars/hottest_summer_school_2022.html

The HoTTEST Summer School 2022 will take place online everywhere in the world during the months of July and August 2022. It will start with parallel introductions to homotopy type theory and formalization, and end with a series of colloquia introducing more advanced topics and exciting areas for further study.

This school is for everyone and anyone with some familiarity with abstract mathematics or theoretical computer science and an itching to learn about homotopy type theory.

Martín Escardó,
Dan Licata,
Egbert Rijke,
Anders Mörtberg;

And also your favorites,
Jon Sterling and Amélia Liao;

and other honest people

Scala 3 Compiler Academy
https://www.youtube.com/channel/UCIH0OgqE54-KEvYDg4LRhKQ

SHAP (SHapley Additive exPlanations) is a game theoretic approach to explain the output of any machine learning model. It connects optimal credit allocation with local explanations using the classic Shapley values from game theory and their related extensions:
https://github.com/slundberg/shap#citations

#machinelearning #explainableai

And now back to Scala 3:

https://hustmphrrr.github.io/blog/2019/compare-dots.html
"Comparison Between Different DOTs"

Apparently there's at least two DOT calculi and they are not equivalent. Actual connection of either one to Scala 3 is unclear.

https://www.hertzbleed.com/

Holw cow! They're now leaking secrets from constant-time cryptographic algorithms using CPUs' frequency scaling! 😱

https://www.unison-lang.org/unison-forall-2022/

June 24 2022, 9 AM - 5 PM EDT
(13:00 - 21:00 UTC)

https://handmade.network/jam

Another Handmade Network's Wheel Reinvention Jam. August 15 - 21.

Посмотрел лекцию — огонь! 😃

любопытный набор. Если кому-то, как и мне, стали интересны детали про синтетическую теорию веросятности, вот немножко:
- https://etda.libraries.psu.edu/files/final_submissions/20192
- http://tobiasfritz.science/2019/cps_workshop/slides/simpson.pdf
- https://www.youtube.com/watch?v=XtsBsLM9ofk

Pen and paper exercises in machine learning

https://arxiv.org/abs/2206.13446
https://github.com/michaelgutmann/ml-pen-and-paper-exercises

https://unsound-workshop.org/

A workshop at SPLASH 2022 about unsoundness in specifications, systems or expectations. CFP is open till 2022-09-01 (but no formal publication).

Expecting lots of Rust folks. 😁

Papayannopoulos, [2020] "Unrealistic Models for Realistic Computations: How Idealisations Help Represent Mathematical Structures and Found Scientific Computing"

Научные вычисления (scientific computing / computational science), т.е. общие техники для всех вычислительных ветвей эмпирических наук, можно разделить на символьные и численные методы, в статье идёт речь о последних. Т.к. численные методы работают с непрерывными значениями (действительными/комплексными числами и их обобщениями), появляются вопросы сходимости, устойчивости и вычислимости алгоритмов над плавающей арифметикой (в частности проблема накопления ошибок округления). Для изучения этих вопросов нужен математический фреймворк вычислений над несчетными множествами, из наиболее популярных это BSS model (aka Real-RAM) и computable analysis (aka Type Two Effectivity), причем друг с другом они несовместимы. Статья посвящена разбору этих двух подходов.

CA/TTE - более фундаментальная и "низкоуровневая" теория, это разновидность матанализа, где сохраняется классическая теория, но дополнительно учитываются вычислительные представления объектов через бесконечные аппроксимации. Как правило, это делается через работу с некоторыми разновидностями машин Тюринга (с оракулом или более сложной машинерией репрезентаций). Её появление можно отследить к трудам Бореля, Банаха и Тюринга 1910-30х годов, где рассматривались вычислимые подмножества R (эта идея получила развитие в Марковской школе конструктивизма/синтетической вычислимости). Более поздние подходы ("Хагенская школа") перешли к рассмотрению всего R (ключевая идея TTE). В этой модели вычислимые функции должны быть непрерывными - как следствие, мы теряем возможность полноценно использовать "точечные" функции сравнения и округления (ср. https://twitter.com/andrejbauer/status/1400172747930718209).

BSS - модель вычислений с идеализированной RAM-машиной, способной хранить в памяти произвольные числа (в т.ч. и точные значения действительных) и мгновенно производить арифметические операции над ними. Тут не возникает проблем с разрывными функциями, но усложняется работа с функциями алгебраическими и трансцендентными (с которыми нет проблемы у CA), начиная с банальных квадратных корней.

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

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

#realnumbers

Tomorrow July 8, on International Congress of Mathematicians (https://www.mathunion.org/icm/icm-2022/virtual-icm-2022-program-sections) will be a Computer Science session in room 1:
* The Mathematics of Hiding Secrets in Software
* Algorithmic aspects of discrepancy theory
* Beyond Linear Algebra
* A Mathematical Perspective on Machine Learning
Virtual attendance is possible (check the page).

http://aitp-conference.org/2022/

Apparently, there's an annual conference on all things AI and Mechanised Theorem Proving (automatic, interactive and their integration). Topics cover everything from mining archives of formal proofs to proving correctness of ML algorithms to AGI applications.

This year's speaker lineup is insane from Ben Goertzel and Stephen Wolfram to Kevin Buzzard and Talia Ringer.

https://www.amazon.com/gp/product/052103311X Appel, [1992] "Compiling with Continuations"

https://slang.soe.ucsc.edu/cormac/papers/pldi93.pdf Flanagan, Sabry, Duba, Felleisen, [1993] "The Essence of Compiling with Continuations"

https://www.microsoft.com/en-us/research/wp-content/uploads/2007/10/compilingwithcontinuationscontinued.pdf Kennedy, [2007] "Compiling with Continuations, Continued"

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/join-points-pldi17.pdf Maurer, Downen, Ariola, Jones, [2017] "Compiling without Continuations"

https://www.cs.purdue.edu/homes/rompf/papers/cong-icfp19.pdf Cong, Osvald, Essertel, Rompf, [2019] "Compiling with Continuations, or without? Whatever"

https://williamjbowman.com/downloads/wjb-paper-anf-sigma.pdf Bowman, Ahmed, [2019] "Compiling Dependent Types Without Continuations"

https://dl.acm.org/doi/pdf/10.1145/3485491 Paraskevopoulou, Grover, [2021] "Compiling with Continuations, Correctly"

Why Adjunctions Matter

• For the average programmer, adjunctions are (if known)
more respected than loved.
• However, they are key to explaining many things we do as
programmers.
• I will try to show how practical adjunctions are by revealing
their ”chemistry” in action.

https://www4.di.uminho.pt/~jno/ps/wadt22sl.pdf

A Note on the Under-Appreciated For-Loop
Jose N. Oliveira, 2020
https://www4.di.uminho.pt/~jno/ps/haslabtr202010.pdf

Excerpts:

> Just remove two letters from the word “foldr“‘ and you get “for”
<...>
> It is well known that, in the case of lists, foldr comes with its “left”-version foldl, which has the same functionality and implements foldr more efficiently under some mild conditions. What about for? Danvy [1] shows that a “left”-version of for exists