For many users of theorem provers, tactics are merely an inelegant solution to a difficult problem. However, we believe that tactics deserve more attention and appraisal, and well-designed tactics are actually a well-structured way to construct programs. In this work, we will explore the connection between tactics and structure editors, as well as emphasize the importance of designing tactics with well-defined semantics with respect to proof terms and proof states.

I am a master’s student in computer science at Tufts University, where I am advised by Sam Guyer. Previously, I was a research visitor at Nagoya University, Japan, working with Jacques Garrigue, and before that an undergraduate student at Tufts University, from where I graduated with a B.S. in 2018.