About My Research
I work in the area of programming languages where I apply mathematical techniques, in particular mathematical logic, towards the problems of understanding programs, verifying software, and designing better programming languages. My current research agenda has two prongs, both of which I am looking for undergraduates to assist me with!
Program Synthesis and Semi-automated Programming
Program synthesis is the automatic generation of programs from specification. By using synthesis technology, we can help developers create difficult-to-write programs automatically with strong guarantees about its correctness as well as assist non-programmers in writing programs.
As a simple example, suppose that we are writing a function to calculate the length of a list. Rather than writing down this function directly, we can specify this function another way—with input/output examples:
 => 0 (* Given an empty list, the function produces 0 *)  => 1 (* Given the list , the function produces 1 *) [0;2] => 2 (* Given the list [0; 2], the function produces 2 *)
With a program synthesis tool such as our current prototype, Myth, we can take these examples and produce a working program:
let rec length (l:list) : int = match l with |  -> 0 | x::l' -> 1 + length l'
Unsurprisingly, it turns out that program synthesis is a very difficult problem and we are only able to automatically generate relatively simple programs. However, what if we involved the programmer directly in the synthesis process, directing the synthesis tool where it should search and helping it prune down the space of possible programs? Such a tool I call a semi-automated programming assistant; think auto-complete like you have seen in Eclipse, but on large chunks of a program rather than just method calls.
Students on this project will help scope, develop, and evaluate our initial efforts into building such a semi-automated programming assistant. They will learn about the theory and technology that powers our type-directed program synthesis systems and put that into practice to help build these tools.
Program Reasoning and Pedagogy
Mathematics sits at the foundation of computer science, providing practitioners with techniques to model and reason about programs. In particular, the study of mathematical proof is essential to algorithmic design and reasoning about program correctness, in both formal and informal settings. However, computer science undergraduates often fail to appreciate the value of mathematical proof in their studies. They never truly understand the mechanics of proof and its similarities to the mechanics of programming. And they are also unaware of how formal proof informs the informal day-to-day reason they perform over their computer programs.
With this project, we would like to develop pedagogy and tools using to help students understand how to reason about their programs. A proof assistant is a software package that helps a user develop and verify a formal mathematical proof, typically related to the properties of a computer program. Ideally, students could use proof assistants to help author proofs, particular about computer programs, receiving immediate feedback and validation on the proof. However, proof assistants are heavyweight programs designed for experts, and are not directly accessible by undergraduate computer scientists without significant additional training.
In this project, students will help develop proof assistant technology to support the integration of formal reasoning about programs into the undergraduate curriculum. They will learn about modern-day proof assistants such as Coq and put that knowledge into practice to build an automated tutor to support this pedagogy.
In an ideal world, you should have finished the computer science introductory series (through CSC 207) and taken discrete mathematics (CSC 207) or the computer science-approved mathematics bridge course (MAT 218)—or have equivalent experience. Comfort with functional programming (e.g., Racket) and mathematical maturity (i.e., background in additional math courses) is a plus! But ultimately, if you’re simply curious about programming language theory and want to try it out, let’s chat!
Schedule and Expectations
I think the MAP program is a great opportunity for undergraduates to learn what research is like as well as learn about the cutting-edge in computer science. However, it is very much an experience that pays off in proportion to how much you put into it. As a result, I place high expectations on my undergraduate research students and their work during their tenure as a MAP student. These expectations hold not just during the summer—I expect students to put in work in the spring to prepare and in the fall to disseminate and share their work through poster sessions, student research competitions, and/or talks, at regional and national conferences.
In the spring semester, I usually provide one or more opportunities for students interested in doing a MAP with me as well as people generally interested in programming language theory. These include:
- An informal reading group in current trends in programming languages and systems. The reading group builds up foundational knowledge in programming language theory, e.g., by working through chapters of Types and Programming Languages or Software Foundations as well as reading current papers in the field.
- Advanced courses in the areas of programming languages and systems, e.g., programming languages seminars (CSC 395) and compilers (CSC 312).
MAPs run for ten weeks in summer starting close to or immediately after finals week and ending approximately in the first week of August. I will typically be away for a week or two for conferences or family vacation. Depending on the timing, these weeks will either be conducted remotely or be consider vacation weeks for the entire group. Exact official times for the MAP are negotiable on an individual basis.
Fall and Spring MAPs
Due to the high workload for both students and faculty during the regular school year, I typically do not offer MAP opportunities during the fall and spring semesters. However, I am open up to working with highly-motivated students that have a demonstrated ability to complete independent work and have a strong interest in programming languages. If you believe you fit this description and are interested in such an opportunity, please let me know.
Additional Questions and Applying
If you have any questions or would like more information about pursuing a MAP with me, please don’t hesitate to email me or drop by my office. To apply:
- Please fill out the standard Grinnell MAP application form.
- Schedule a 30 minute block to meet with me (via my Scheduling page) for an informal interview. You don’t need to do anything to prepare for this interview. It is an opportunity for us to discuss your research interests and the potential projects in more detail.
- Read the first two chapters (through the induction chapter) of Software Foundations and complete the exercises within. Please send your completed Coq files (
Induction.vfrom the book) to me and send them to me by February 28th.
At a bare minimum, you should complete the following exercises from these two chapters:
Basics.v: Exercise: 2 stars (boolean_functions)
Induction.v: Exercise: 2 stars, recommended (basic_induction)
Induction.v: Exercise: 2 stars (double_plus)
Although I encourage you to complete as many of the exercises as you deem necessary to learn the concepts found in the chapters as well as those that capture your interests. On top of this, if you have the time, capacity, and/or interest, feel free to move forward in the book and send me any additional work that you produce.