1) as formally rich and fascinating as reality admits, and
2) ultimately grounded in guiding human experience
So far these have included shape/alias/region-analysis types for usable ownership, learned bayesian models of total point-to-point information flow in programs (for better error location), and now hardware design to enable performant code in the transactional memory model.

📜🎉📜: flexible type system for fearless concurrency 🎉
 (PLDI '22), with Mae Milano and Andrew Myers

() -> Contact Info:

let t0 = 'turcotti.julia'
let t1 = '@gmail.com
while (true) skip //hot bots get stuck here
let myEmailAddr = t0 + t1

My site is pretty minimal so far - mostly a placeholder so the grand linking engines begin to acknowledge me. But here's recent work/research interests:

NilAway (blog announcement, github):

Null dereference freedom in languages can be phrased in terms of very simple constraints. NilAway is a compositional static analysis that incrementally computes and accumulates those constraints, reporting errors to the programmers when contradictions arise. I began work on its design and implementation in 2020 that has since been carried on by an amazing team at Uber. It seems to be very effective so far.

Swift (pitch on evolution forum):

Work on type systems for data race freedom that I undertook with Mae Milano and Andrew Myers has inspired collaboration with the Swift team at Apple. Namely, region-based linear ownership seems to fit naturally onto Swift's actor model, and I have worked to see if this graft can be adopted.

Wisening Assertions (popl src talk, short paper):

Languages can include assertions to give programmers a well-specified way to include correctness reasoning in their code. Unfortunately using these assertions to enforce correctness at runtime is prohibitively expensive because the cost of assertions is paid continuously for the lifetime of the software deployment. I think large code deployments should use their assertions to maintain a live and cheap model of where bugs could live in the running code, and then stop executing assertions that become redundant over time. Doing this in a way that still guarantees arbitrarily high assurance of bug freedom over time, I call "Wisening Assertions".

I've started building out systems for Wisening Assertions, and I like the underlying problem ("hard part") that's arisen as well:

Relate observable probabilistic events about code execution (branch frequency, other runtime monitors) to interesting probabilistic events about code execution (was there information flow? was an unoptimized path hit?)

This problem is in some ways a ripe candidate for ML - "train" a model to predict interesting code events given the observable facts about past executions - but I've been interested in a more basic approach inspired by probabilistic graphical models. It's been illuminating and I also have exciting ideas for applications to speculative compilation.

Current research direction

With boutique hardware becoming incresingly realistic there's a chance to reinvent hardware transactional memory and maybe finally realize HTM's original dream of embarassingly scalable, high throughput, contention-tolerant parallel processing.

Since coming to MIT I've been exploring this space, with the motivational example of Puppetmaster, a certified hardware accelerator for HTM scheduling. 

We finally believe that narrowing our task to the design of a chip for processing OLTP-like workloads might yield broad optimizations in the hardware design.

Greatest Mentors So Far:

Andrew Myers ????

Mae Milano 🫶🏻🦾

Priya Srikumar 💗💫