Pavel Panchekha

About:

Pavel Panchekha is an Assistant Professor at the University of Utah, focusing on mechanical reasoning and domain-specific languages.

Website:

pavpanchekha.com

Specializations:

Researcher Assistant Professor

Interests:

Mechanical reasoning Synthesis for domain-specific languages Floating-point numerical programs Web page layout code

Incoming Links:

Nathan Knowler

Outgoing Links:

Evan Miller

Subscribe to RSS:

Link

2025-08-06 • computing technology history byte ipv6

The post explores the hypothetical implications of using 9-bit bytes instead of the standard 8-bit bytes in computing systems. It discusses how this change could have affected various aspects of technology, including IPv4 address ...

2025-12-03 • web development design css layout conditions and constraints

The blog post discusses the complexities and challenges of CSS layout rules, particularly the difficulties in centering elements and achieving consistent layouts. The author, who has expertise in CSS specifications, explores the i...

2025-12-04 • chatgpt software development code github copilot ai

The post discusses three methods for AI coding: using auto-complete features in text editors, leveraging chat interfaces like ChatGPT for code generation, and employing AI agents that utilize a loop structure to generate and execu...

2025-12-05 • shells collaboration ai agent harness

The text discusses the concept of 'agent harnesses' as collaborative shells that allow both users and AI models to execute commands and control processes symmetrically. It highlights the potential for these harnesses to improve us...

2025-06-23 • conference research computer science programming languages pldi 2024

The text is a summary of the author's experience at PLDI'25, highlighting the talks and papers that stood out to them. They discuss various presentations, including EGRAPHS'25, Automated High-Level Synthesis Design, Oatlog, Partia...

2025-05-31 • cpu simulation microarchitecture assembly apple m-series

The author describes the process of testing a simulator for the Apple M1 chip, which involved writing assembly code, handling flags registers, doing register allocation, and timing the simulator to validate its results.

2025-05-30 • simulation assembly language apple m-series algorithms double addition

The text describes a cycle-accurate simulator for the Apple M1 P- and E-cores, and provides details on the definition of the cores, assembly code, and algorithms for double-double addition.

2025-05-26 • syntax move operation order modular arithmetic quantifier elimination

The text discusses quantifier elimination and how it leads to ordinary mathematical syntax such as modular arithmetic, set operations, and order. It provides examples of how quantifier elimination results in these mathematical con...

2025-05-23 • pattern matching quantifier elimination line graphs e-graphs modulo t cell decomposition

The text discusses LIN-graphs and Egraphs modulo T, focusing on pattern-matching, relational e-matching, quantifier elimination, and cell decomposition. It explains the concept of LIN-graphs, linear combinations, linear equations,...

2025-05-21 • trigonometry expressions variables rational functions

The text discusses the process of deciding equality for trigonometric expressions with multiple variables by using common denominators, expanding trig functions, and applying the Weirstrass substitution.

2025-05-21 • reasoning e-graphs matching equality e-graphs modulo t term bank canonicalization process

The text is an attempt to summarize the concept of Egraphs modulo T, which is a method for conjunctive reasoning with equality. The author discusses the structure of an E-graph, the term bank, and the canonicalization procedure. T...

2025-05-20 • error fusion amplification factors

The text discusses the impact of operator fusion on error in mathematical operations. It explains how fused operations can be more accurate than unfused operations, and how the choice of implementation can affect error. It also hi...

2025-05-19 • computer science mathematics resources algebra

The text discusses the use of P-graphs as an extension of E-graphs for algebraic rewriting of mathematical expressions. It explains the limitations of E-graphs and the potential of P-graphs in handling basic sums and products. The...

2025-05-14 • debugging arithmetic computation theory numerical optimization

The text discusses the concept of 'safe' numerical programming and the challenges of existing debuggers. It focuses on the use of double-double arithmetic as an oracle to address false negatives in floating-point computations.

2025-05-12 • optimization latency apple m-series throughput fast two-sum

The post discusses the FastTwoSum algorithm and its optimization on the Apple M1 chip. It analyzes the latencies and throughputs of different versions of the algorithm and concludes that the '@2' version is the best for the Apple ...

2025-05-05 • gcc simd compiler intrinsics clang branch prediction

The author compares the performance of TwoSum, FastTwoSum, basic sort, SIMD sort, and integer sort algorithms using GCC and Clang. The author analyzes the assembly code and explains the differences in performance.

2025-04-24 • chatgpt web development teaching software engineering ai

The author discusses their experience with ChatGPT o3, the full version, and how it has impressed them with its capabilities in software engineering projects, web browser engineering exercises, and software verification. They also...

2025-03-13 • search algorithms assembly hybrid search apple m-series chips quaternary search octal search intel 8th gen chip memory and compute dependencies

The author tested various search algorithms and found that binary search is the fastest, with a basic implementation taking 54 cycles. They also tested hybrid, quaternary, octal, and shar search algorithms, and found that the shar...

2025-03-07 • web development bloom filter personal style

The text explains how Stylo matches CSS selectors using a bloom filter per thread, which is pretty big and counted. Each rule has up to four hashes, and the limit is critical for fast-reject to be fast. Counted bloom filters can b...

2025-01-31 • herbie o1 o3 mini

The text discusses the performance of O3 and O3-mini-high in comparison to Herbie, highlighting that O3-mini-high is close to being competitive with Herbie, especially on easier textbook examples. It also mentions that O3-mini-hig...

2025-01-14 • herbie accuracy and validity e-graphs oracle solaris condition numbers

The proposal suggests a new method for Herbie to work, using oracle-free methods of evaluating error to make it simpler, faster, and possibly better. It discusses the current method of Herbie, preliminary work, the proposal, poten...

2024-12-28 • api herbie build tools and infrastructure platform creation auto-tuning

The text discusses the idea of making it easy for users to create platforms of their own for Herbie. It proposes the use of command-line tools and APIs to achieve this, as well as the ability to modify existing platforms and autot...

2024-10-08 • hardware floating point numerical kernels

The text discusses different levels of floating-point operations, including bitwise operations, polynomial operations, algebraic operations, simple elementary functions, hard elementary functions, and weird functions. It also expl...

2024-09-15 •

The post discusses the concept of batches as virtual mu types, aiming to make programming with batches 'normal'. It explores the relationship between recursive and batch code, the use of mu types as data representations, and the p...