Structural Refactorings for Exploring Dependently Typed Programming

Dependent types provide users with the tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language develops such programs by enriching simply typed programs through a process of refactoring.