proof engineer / prog lang dev
Community of Madrid, Spain
Joined November 2007
- Tweets463
- Following193
- Followers210
- Likes1.1K
Alex G retweeted
Applying Functional Programming to make AI more reliable? HELL YEAH!
AI isn’t only about big data and neural networks there’s also a world where logic leads the way... That’s where Alexander Gryzlov, proof engineer, steps in.
In his talk, he’ll show how classic techniques get a fresh twist, with clever combinators doing the heavy lifting so you can focus on the ideas.
From his early days as an industry developer, Alexander blends practice and theory to show how “old-school” AI and modern techniques can work together to create software that’s both reliable and a little bit magical
Get to know him and his talk in depth here: lambda.world/speakers/?speak…
#SymbolicAI #Agda #DependentTypes #FormalVerification
ALT Alexander Gryzlov's talk: "Total Functions for Automated Reasoning: Building Terminating Theorem Provers"
Alex G retweeted
Live coding Haskell and specifications! @nikivazou introduces LiquidHaskell and refinement types in this afternoon session
Alex G retweeted
Join us for an engaging talk by @clayrat from @IMDEA_Software as we delve into the intriguing realm of formalizing infinite programs and codata, using #Agda as our vehicle👨💻. Don’t miss out on this enlightening event! 📆 /cc @iLABMadrid meetup.com/fp-madrid/events/…
Показал одновременную завершимость и корректность для RLE, wordsBy, квиксорта и мержсорта, добавил guarded Rose trees, расширил инфраструктуру для кванторов над стримами с часами. Почти доделал порт на гварды Abel'17 (автоматы для произведения и звезды Клини).
Основное время занимался доказательствами завершимости: GCD, wordsBy, RLE, мержсорт, вложенная рекурсия (zeroOut, функции Маккарти & Аккермана), рекурсия высшего порядка (зеркалирование дерева со списком ветвей), рекурсия внутри продолжений (алгоритм Харпера для регэкспов).
Начал пилить порт Абеля'17 на гварды (про автоматы и производные для регулярок), построил коиндуктивные префиксные деревья, доказал для них законы алгебры Клини и лемму Ардена, начал сами автоматы. Порефакторил кодировки нестрогопозитивных типов на стиль рекурсивных схем.
Сделал частичный порядок и предикат сходимости на паршиалити монаде, доказал законы монады на ней, сделал обобщенный оператор гвардед аппликатива (давно пора), поправил кванторы на стримах. Набросал автоматы Мили & Мура на гвардах. Начал NbE на паршиалити монаде по Абелю-Чапману.
Копался с конечным вариантом монады частичности, в конечном счёте понял, что нужно сделать невыразимой ▹-алгебру. Запилил на гвардах кванторы для стримов, WLPO, начал расширять инфраструктуру для часов, спортировал на них первую половину статьи Амбриджа про теорему Тихонова.
Начал синтетический порт варианта денотационки Харта, дошел до здравости включительно; показал, что гварды коммутируют с гетеропутями и характеризацией уровня; сегодня наконец доказал, что монада частичности сохраняет гомотопический уровень содержимого начиная с сетов!