About Me

I'm a 4th year PhD student at Indiana University working with Sam Tobin-Hochstadt.

I am interested in programming language research, particularly in leveraging type theory and formal verification techniques to build more robust systems. My recent work has involved an extension to Typed Racket which adds support for basic dependent types. You can try it out by downloading Racket here (version >= 6.11).

Email | CV | Github | Twitter

Project Involvement

Racket

Typed Racket


Publications

Migratory Typing: Ten Years Later, with Sam Tobin-Hochstadt, Matthias Felleisen, Robert Findler, Matthew Flatt, Ben Greenman, Vincent St-Amour, T. Stephen Strickland, and Asumu Takikawa, at SNAPL 2017. [pdf]

Occurrence Typing Modulo Theories, with David Kempe and Sam Tobin-Hochstadt, at PLDI 2016. [acm | arXiv]

Design and Evaluation of Gradual Typing in Python, with Michael M. Vitousek, Jeremy G. Siek, and Jim Baker, at DLS 2014. [acm]

Linking the Past: Discovering Historical Social Networks from Documents and Linking to a Geneological Database, with Douglas J. Kennard and William A. Barret, at HIP 2011. [acm]


Blog Posts

Some Changes in Typed Racket v6.8

:: Typed Racket, Performance

The more things change, the more they stay the same… at least for these updates! =)

TL;DR Typed Racket has a whole bunch of new parts under the hood for v6.8—hopefully as a user you can’t tell (unless of course it’s because your program type checks faster)!

If you’re a little curious about “how the sausage is made” (or what new ingredients they contain…?) read on!

Typesetting with PLT Redex

:: Racket

PLT Redex is a great tool for tinkering with and examining various aspects of programming languages. Although it can be used to programmatically generate mathematical figures for papers and the like (awesome!), the actual machinery for doing so is a little lower level than you want 99% of the time.

To alleviate this, I developed a package (typeset-rewriter) with a few simple tools that make it much easier to build the rewriters redex natively supports.

Let-aliasing in Typed Racket

:: Typed Racket

Although Typed Racket (TR) can currently typecheck a large number of common idioms found in Racket code, reasoning about direct and indirect usages of aliasing has escaped its grasp... until now!

Quicksort in Coq

:: Coq, Dependent Types

Coq’s support for dependent types mean that type checking not only catches trivial errors like passing an integer to a function expecting a string, but it can also check and verify types which represent properties regarding the functional behavior of the a program.

I thought it would be edifying to use this capability to write a verified version of quicksort (i.e. a quicksort with types that specify its behavior), and it was!

C to Racket Examples

:: Racket, C

This post is a collection of simple C code snippets and roughly equivalent Racket code.

Hopefully if you’re coming from a C background (or similar) and you’re struggling to make sense of Racket code, these examples will assist in clearing the fog.

Total List Functions

:: Coq, Dependent Types

What is the type of a function which returns the first element of a list? One possible (and likely common) answer would be:

1
(: first (All (X) ((Listof X) -> X)))

This (typed racket syntax) says first is a function from a list of X’s to an X (where X is any type). However, we really know that, although its type is ((Listof X) -> X), if we pass an empty list of X we will not get an X, but a runtime error of some sort (e.g. no values). The type then isn’t really giving us a guarantee of what it will do for us… it’s just telling us what it will try to do for us if it doesn’t fail.

“No. Try not. Do… or do not. There is no try.” - Master Yoda

There is a parallel in math: some functions are not defined for all possible input values (e.g. f(x)=1/x). These are called partial functions (as opposed to total functions). It is common practice to reserve the term “function” for total functions in math, while in programming partial functions are ubiquitous and there is little effort to distinguish between the two. If only there was some way that the types could reflect this possibility…