xefのブックマーク - はてなブックマーク

Justified SMT 1: The Minikanren inside Z3

xef 2024/06/14

リンク

There are lots of interesting little subprobl ems in compilation like instruction selection, register allocation and instruction scheduling. These can be expressed in declarative interlinked way to constraint solvers. I’ve been fiddling with probably 6 iterations of using constraint solvers for compiler backends over the last 3 years and never written a blog post on it. This is long over due, and s

xef 2024/03/20

Z3

リンク

Egglog 2: Automatically Proving the Pullback of a Monic is Monic

xef 2021/08/06

TheoremProving

リンク

Translating My Z3 Tutorial to Coq

I had a fun time giving a Z3 tutorial at Formal Methods for the Informal Engineer (FMIE) https://fmie2021.github.io/ (videos coming soon hopefully!). I got to be kind of the "fun dad" with the Z3 tutorial https://github.com/philzook58/z3_tutorial , while at times it felt a bit like Cody's Coq tutorial https://github.com/codyroux/broad-coq-tutorial was trying to feed the kids their vegetables. It w

xef 2021/03/01

Coq

リンク

Linear Relation Algebra of Circuits with HMatrix

xef 2019/11/11

Haskell

リンク

Linear Algebra of Types

It gives my brain a pleasant thrum to learn new mathematics which mimics the algebra I learned in middle school. Basically this means that the new system has operations with properties that match those of regular numbers as much as possible. Two pretty important operations are addition and multiplication with the properties of distributivity and associativity. Roughly this corresponds to the mathe