By
Pavel Panchekha
Blog
WBE
Herbie
Github
Papers/CV
Share under
CC-BY-SA
.
Pavel's Blog
Batches as Virtual Mu Types
pl
research
herbie
OpenAI o1 vs. Herbie
herbie
Batches for Recursive Data Structures
pl
research
herbie
Optimal Heap Limits for Generational GCs
research
Rounding Bits over Rounding Modes
pl
ChatGPT vs. Herbie
herbie
How I Think About Research Projects
research
Top-down LR parsing
prog
MegaLibm: a Math Library Workbench
research
Improving Rust with Herbie
herbie
Affine Arithmetic and Error Taylor Series
research
A new era for Herbie
herbie
Optimizing Pruning in Herbie
herbie
An update on Herbie, Summer 2022
herbie
Speeding up Skia using E-graphs
research
What is the Complexity of Selector Matching?
research
Epsilon and Delta in Error Models
research
Binding in E-graphs
research
Synthesizing Range Reductions
herbie
An Accurate Quadratic Formula
herbie
User Trust in Herbie
herbie
Fuzzing for Layout Invalidation Bugs
research
Understanding Error Taylor Series
herbie
A DSL for Math Library Implementation
herbie
Balancing Multiple Garbage Collectors
research
Detecting Symmetric Expressions
herbie
A Software Verification Project
prog
Using Egg in Herbie
herbie
A Feb 2020 look at Herbie
herbie
Verification Beyond Functions
pl
Herbie in 2019
herbie
Why are Shell Scripts Bad?
pl
Parallel Line Breaking
research
Proof Systems as Operating Systems
pl
A Survey of PL Blogging (Part 2)
pl
My job market materials
research
Intrinsic and Extrinsic Data
pl
Architecture Patterns
pl
Long-term Goals for Herbie
herbie
Sub-specifications
research
pl
Was Lower Case Designed for Reading Speed
misc
Learning Shame
math
Designing Libraries like Languages
pl
What's Wrong with CSS?
prog
Categories for Function Reactive Programming
pl
Crosswords:
Selective Crossword Submissions
misc
Crosswords:
Dedicated Crossword Practice
misc
Crosswords:
You Start Off Bad at Crosswords
misc
Crosswords:
Crossword Science with Stan
misc
How I Track Todos
misc
Remembering the Herbie Visualizer
pl
Social Processes in Package Managers
prog
Programs as Patchwork
pl
First Impressions with Typed Racket
herbie
Solving Resistance
prog
misc
Not Quite Pushouts
math
Programming with Pushouts
math
Cryptic Mastermind with Z3
prog
A Survey of PL Blogging (Part 1)
research
A Game Theory of Primaries
math
WIP:
Programming by Voice
prog
Assigning Meaning to Open Terms
pl
Floating Point Error in Polynomials
herbie
Floating Point Error in the Small
herbie
Functions and Relations in First-order Logic
pl
How Cassius Works
css
Variary Functions in Coq
pl
Blame Analysis and Local Error
fp
Modularity for Verdi
research
Exact Geometric Operations
herbie
Unpublished blog posts in Magit
misc
Why Equality?
pl
Paper Statistics with TimeTracker
research
Shadow Icons with CSS
css
How CSS Floats Work
css
Multi-command-line in Racket
herbie
A Fine Language
pl
Grammars in Racket
prog
How Herbie Happened
herbie
Bimodal Logic
math
misc
Rational Rationality
math
misc
Moral Prisoners
math
Models of Modal Logic
math
What is Modal Logic?
math
Solving the Prisoners’ Dilemma
math
First-order Logic is a Modal Logic
pl
Designing the PLSE Logo
prog
Quadrature in Bash
prog
Equal Functions in ITT
pl
Well-Suited
(a story)
misc
WIP:
Refinement in Mathematics
math
Zippers:
Multi-Zippers
(Part 4 of 4)
algs
Models from Models
math
Game-theoretic Protesters
math
Pedestrian Statistics
math
Logarithms of Taylor Expansions
math
prog
Hyperbolic sines in math.js
fp
Taylor Expansions of Taylor Expansions
math
Arbitrary Precision, not Arbitrary Accuracy
fp
Complex Square Roots in math.js
fp
The Eigenvalue Game
math
Paper Statistics with Git
research
Models:
Defining a Logic
(Part 2 of 6)
math
Models:
What is a model?
(Part 1 of 6)
math
Floating Point Guarantees
fp
Major Key
(a puzzle)
misc
Age-aware:
Tree Lookup
(Part 2 of 4)
algs
Age-aware:
Age-aware Array Search
(Part 1 of 4)
algs
Fixed points:
Stability
(Part 4 of 4)
pl
Stream Fuse Carefully
pl
Plotting Functions in D3
prog
Pairs in Hindley-Milner Languages
pl
Fixed points:
Attraction and Orders
(Part 3 of 4)
pl
Fixed points:
Fixed behaviors
(Part 2 of 4)
pl
Fixed points:
What is a fixed point?
(Part 1 of 4)
pl
The Gaussian and the Sine
math
Tea physics
misc
Xifed points
pl
(call/cc call/cc) and friends
pl
Engineering Taste
prog
Organizing Objects
misc
A Critique of ADT.scm
prog
Uniqode
(a puzzle)
misc
Typing Analytics in Emacs
misc
Forward with Federated
prog
Package Management for the 21.1st Century
misc
The Law of Demeter, and a question of design
pl
The Levels of Concurrency
pl
Time, Clocks, and an Implementation in Erlang
algs
Zippers:
Kiselyov Zippers
(Part 3 of 4)
algs
Zippers:
Zippers as Derivatives
(Part 2 of 4)
algs
Zippers:
Huet Zippers
(Part 1 of 4)
algs
Injection is a Display-level Problem
prog
Programming With Types
pl
MIT Zephyr from Arch Linux
misc
Using Org-mode to Publish a Website
misc
Treaps: The Magical Awesome BBT
algs
Installing Ubuntu on LVM
misc
Sequences, Series, and Recursion
math
How to Draw a Heart in Polar Coordinates
math
7919, 7853, and Li(x)
math