Calvin Loncaric

Hello! I am a PhD student in the programming languages and software engineering group at the University of Washington in Seattle. I am interested in a wide range of topics in this field, and my advisor is Michael Ernst.

I graduated from Harvey Mudd College in 2012 with a degree in computer science. Before joining UW I worked as a software engineer at a startup called Quixey. In 2015 I spent a summer working with Satish Chandra at Samsung Research America.


Data Structure Synthesis

High-performance data structures are at the heart of many applications. In our PLDI 2016 paper we describe how to generate complex data structure implementations from high-level specifications. Cozy (our implementation of these techniques) is available online.

I am currently working on extensions to Cozy so that it can handle a much wider class of data structures.

People: Michael Ernst, Emina Torlak, and Haoming Liu.

Formal Verification of a Neutron Therapy Machine

My group is working on formal verification techniques for a large real-world system: the Clinical Neutron Therapy System at the UW Medical Center. The CNTS is used for actual cancer treatments, so we want a high degree of confidence that all the code is correct!

Verifying all the CNTS code is challenging since it is built on many different technologies. Our SNAPL 2015 paper describes the need to combine many disparate verification strategies into a cohesive piece of evidence. In our CAV 2016 paper we describe how we actually achieved this for (parts of) CNTS.

People: Jon Jacky, Stuart Pernsteiner, Zach Tatlock, Emina Torlak, Michael Ernst, Dan Grossman, and Xi Wang.

Type Error Diagnosis

Many developers have horror stories of struggling to diagnose type errors in type-inferred languages like ML and Haskell. Recent research promises far more accurate error messages, but the techniques are difficult to implement and slow to run.

Our OOPSLA 2016 paper describes how to achieve comparable quality at substantially lower run-time cost. Even better, our technique can be implemented with only small modifications to a compiler's existing type inference algorithm!

There is also a tech report on this research that expands some details in the OOPSLA paper. In particular, Appendix C gives advice for compiler writers and future researchers. Note that this is my own version of the paper and has not been peer-reviewed. (Last updated 10 October, 2016.)

Our code and evaluation materials are available on request.

People: Satish Chandra, Cole Schlesinger, and Manu Sridharan.

Other Projects

Generator to Iterator Converter
February 2017
Compiles Python-style generator functions to Java-style iterators.
Sketch to UI converter
June 2015
Computer vision class project to convert hand-drawn sketches into user interface code (e.g. HTML).
Coq Plugin for Sublime Text 3
May 2014
A plugin for interacting with the proof assistant Coq in the Sublime text editor.
Marching Tetrahedrons
April 2012
A clean implementation of the marching tetrahedrons algorithm for rendering implicit surfaces.


Calvin Loncaric
CSE Department at the University of Washington
Office: CSE 430
Online: GitHub, LinkedIn