Blog

Adding a new theory to cvc5

Extending an SMT solver

Student Opinions on Intro CS Topics

Data and reflection after teaching introductory computer science at Loomis Chaffee

Revisiting the Mohr-Mascheroni Theorem

A compass is not necessarily as powerful as a compass & straightedge

Construct & The Mohr-Mascheroni Theorem

Exploring Construct: a domain-specific-language for classical geometry

General Top-Down Splay Trees

Exploring generalizations of splay trees.

Generating Personal Statements

Generating natural language using a syntax-aware model.

Unsafe in Rust: The Abstraction Safety Contract and Public Escape

Defining and detecting some ways `unsafe` is misused

Unsafe in Rust: Syntactic Patterns

Finding common syntactic patterns in the use of `unsafe`.