Jeremy Siek

Take-aways from using Deduce in the classroom

Binary Search Trees, Correctly!

Binary Trees with In-order Iterators (Part 2)

Binary Trees with In-order Iterators (Part 1)

Merge Sort with Leftovers, Correctly

Insertion Sort, Correctly

Sequential Search, Correctly

Data Structures and Algorithms, Correctly

Help! We're Failing to Prove Correctness of Closure Conversion using Denotational Semantics (Graph Models)

Gradual Guarantee via Step-indexed Logical Relations

Type Safety in 10 Easy, 4 Medium, and 1 Hard Lemma using Step-indexed Logical Relations

Using Agda's Induction/Recursion Library

Strongly Connected Components and Kosaraju's Algorithm

Type Safety in Two Easy Lemmas

Reading list for getting started on Gradual Typing

Intersection Types, Sub-formula Property, and the Functional Character of the Lambda Calculus

What do real numbers have in common with lambdas? and what does continuity have to do with it?

Putting the Function back in Lambda

New revision of the semantics paper (POPL rejection, ESOP submission)

Comparing to Plotkin and Engeler's Set-theoretic Models of the Lambda Calculus

POPL submission, pulling together these blog posts on semantics!

Revisiting "well-typed programs cannot go wrong"

Consolidation of the Denotational Semantics and an Application to Compiler Correctness

The Take 3 Semantics, Revisited

Sound wrt. Contextual Equivalence