Pavel Panchekha

I am Pavel Panchekha, a Ph.D. student at the University of Washington advised by Michael Ernst and Zachary Tatlock. I study new abstractions and tools for programming.

I like email (PGP key) and in-person meetings. I am “pavpanchekha” on Github and Hacker News.

Major Projects

Herbie

Automatically fix floating point accuracy problems. Github
Armstrong Algorithm

A better algorithm for bit-rate adaptation in Wi-Fi. Github
TimeTracker

Records how I spend my time and visualizes the results. Github
Complex Plotter

Plots functions of a complex variable in high resolution. Github

Papers

Automatically Improving Accuracy for Floating Point Expressions, PLDI 2015
P. Panchekha, A. Sanchez-Stern, J. Wilcox, Z. Tatlock
To appear; email for draft.
Verdi: A Framework for Formally Verifying Distributed System Implementations, PLDI 2015
J. Wilcox, D. Woos, P. Panchekha, Z. Tatlock, X. Wang, M. Ernst, T. Anderson
To appear; email for draft.
Expressing and Verifying Probabilistic Assertions, PLDI 2014
A. Sampson, P. Panchekha, T. Mytkowicz, K. S. McKinley, D. Grossman, L. Ceze
The paper, a video, and an introduction by a Adrian Sampson are available.
Blame Trees, WADS 2013
E. D. Demaine, P. Panchekha, D. A. Wilson, and E. Z. Yang
The paper, slides, a video, and introduction by Edward Yang are available.

Talks and Reports

Next-generation Eventual Consistency, Facebook (talk; 29 Jan 2015)
Distributed Shared State with History Maintenance, CSAIL TR 2013
P. Panchekha, M. Brodsky

Blog

Logarithms of Taylor Expansions math prog
Hyperbolic sines in math.js math prog
Taylor Expansions of Taylor Expansions math
Arbitrary Precision, not Arbitrary Accuracy math prog
Complex Square Roots in math.js math prog
The Eigenvalue Game math
Paper Statistics with Git tools
Non-standard models math
- What is a model? (Part 1 of 6)
- Defining a Logic (Part 2 of 6)
Floating Point Guarantees prog
Major Key (a puzzle) misc
Age-aware Data Structures algs
- Age-aware Array Search (Part 1 of 4)
- Tree Lookup (Part 2 of 4)
Stream Fuse Carefully plt
Plotting Functions in D3 prog
Pairs in Hindley-Milner Languages plt
Fixed Points (in abstract) plt
- What is a fixed point? (Part 1 of 4)
- Fixed behaviors (Part 2 of 4)
- Attraction and Orders (Part 3 of 4)
- Stability (Part 4 of 4)
The Gaussian and the Sine math
Tea physics misc
Xifed points plt
(call/cc call/cc) and friends plt
Engineering Taste prog
Organizing Objects tools
A Critique of ADT.scm prog
Uniqode (a puzzle) misc
Typing Analytics in Emacs tools
Forward with Federated prog
Package Management for the 21.1st Century tools
Defending the Web prog
The Law of Demeter, and a question of design plt
The Levels of Concurrency plt
Time, Clocks, and an Implementation in Erlang algs
Injection is a Display-level Problem prog
Zippers algs
- Huet Zippers (Part 1 of 4)
- Zippers as Derivatives (Part 2 of 4)
- Kiselyov Zippers (Part 3 of 4)
Programming With Types plt
MIT Zephyr from Arch Linux tools
Using Org-mode to Publish a Website tools
Treaps: The Magical Awesome BBT algs
Installing Ubuntu on LVM tools
Sequences, Series, and Recursion math
How to Draw a Heart in Polar Coordinates math
7919, 7853, and Li(x) math