Pavel Panchekha’s Blog
We'd be Better Off with 9-bit Bytes
Distinguished (for me) Papers of PLDI'25
Testing My M1 Simulator
Simulating Double-Double Addition Algorithms
Some Surprising Quantifier Elimination Operators
LIN-graphs, an Egraph modulo T
Deciding Equality for Trigonometric Expressions
Egraphs Modulo T (Attempt 1)
How Operator Fusion Affects Error
The Promise of P-Graphs
Absorption in Double-Double Arithmetic
The Fastest TwoSum on an Apple M1
FastTwoSum is Faster Than TwoSum
ChatGPT o3 is the Real Deal
Binary Search is Very Fast
How Stylo Matches CSS Selectors
Does O3 beat a specalized numeric compiler?
Herbie Without Iterations
A Plan for Herbie Plaforms
Not all Arithmetic Operations are Created Equal
Batches as Virtual Mu Types
OpenAI o1 vs. Herbie
Batches for Recursive Data Structures
Selector Matching is Quadratic
Optimal Heap Limits for Generational GCs
Rounding Bits over Rounding Modes
ChatGPT vs Herbie
How I Think About Research Projects
Top-down LR parsing
MegaLibm: a Math Library Workbench
Improving Rust with Herbie
Affine Arithmetic and Error Taylor Series
A new era for Herbie
Optimizing Pruning in Herbie
Speeding up Skia using E-graphs
What is the Complexity of Selector Matching?
Epsilon and Delta in Error Models
Binding in E-graphs
Synthesizing Range Reductions
An Accurate Quadratic Formula
User Trust in Herbie
Fuzzing for Layout Invalidation Bugs
Understanding Error Taylor Series
A DSL for Math Library Implementation
Detecting Symmetric Expressions
Balancing Multiple Garbage Collectors
A Software Verification Project
Using Egg in Herbie
A Feb 2020 look at Herbie
Verification Beyond Functions
Why are Shell Scripts Bad?
Parallel Line Breaking
Proof Systems are Operating Systems
A Survey of PL Blogging (Part 2)
Intrinsic and Extrinsic Data
Architecture Patterns
Long-term Goals for Herbie
Sub-specifications
Was Lower Case Designed for Reading Speed
Designing Libraries Like Languages
Learning Shame
What's Wrong with CSS?
Dedicated Crossword Practice
Categories for Reactive Programming
Selective Crossword Submissions
You Start Off Bad at Crosswords
Crossword Science with Stan
How I Track TODOs
Remembering the Herbie Visualizer
Social Processes in Package Managers
First Impressions with Typed Racket
Programs as Patchwork
Solving Resistance
Programming with Pushouts
Not Quite Pushouts
Cryptic Mastermind with Z3
A Survey of PL Blogging (Part 1)
A Game Theory of Primaries
WIP: Programming by Voice
Assigning Meaning to open terms
Floating Point Error in Polynomials
Floating Point Error in the Small
Functions and Relations in First Order Logic
How Cassius Works
Variary Functions in Coq
Local Error and Blame Analysis
A Fine Language
Unpublished blog posts in Magit
Exact Geometric Operations
Why Equality?
Paper Statistics with TimeTracker
Shadow Icons with CSS
First-order Logic is a Modal Logic
How CSS Floats Work
Multi-command-line in Racket
Grammars in Racket
How Herbie Happened
Bimodal logic
Rational Rationality
Models for Modal Logic
What is Modal Logic?
Solving the Prisoners’ Dilemma
Designing the PLSE logo
Modularity for Verdi
Quadrature in Bash
Equal functions in ITT
Well-Suited
WIP: Refinement in Mathematics
Zippers, Part 4: Multi-Zippers
Models from Models
Game-theoretic Protesters
Pedestrian Statistics
Logarithms of Taylor Expansions
Hyperbolic sines in math.js
Taylor Expansions of Taylor Expansions
Arbitrary Precision, not Arbitrary Accuracy
Complex Square Roots in math.js
The Eigenvalue Game
Paper Statistics with Git
Defining our Logic
What is a Model?
Floating Point Guarantees
Tree Lookups
Major Key
Age-aware Array Search
Fixed Points, Part 4: Stability
Stream Fuse Carefully
Plotting Functions in D3
Pairs in Hindley-Milner Languages
Fixed Points, Part 3: Attraction and Orders
Fixed Points, Part 2: Fixed Behaviors
Fixed Points, Part 1: What is a Fixed Point?
The Gaussian and the Sine
Tea Physics
Xifed points
(call/cc call/cc) and friends
Engineering Taste
Organizing Objects
Algebraic Data Types in Scheme
Uniqode
Typing Analytics in Emacs
Forward with Federated
Package Management for the 21.1st Century
The Law of Demeter, and a question of design
The Levels of Concurrency
Time, Clocks, and an Implementation in Erlang
Zippers, Part 3: Kiselyov Zippers
Zippers, Part 2: Zippers as Derivatives
Zippers, Part 1: Huet Zippers
Injection is a Display-level Problem
Programming with Types
MIT Zephyr from Arch Linux
Using Org-mode to Publish a Web Site
Treaps: The Magical Awesome BBT
Installing Ubuntu on LVM
Sequences, Series, and Recursion
How to Draw a Heart in Polar Coordinates
7919, 7853, and Li(x)