The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 19–21, 2011 in Tokyo, Japan. After the conference, the programme committee, chaired by Olivier Danvy, selected several outstanding papers and invited their authors to submit to this special issue of the Journal of Functional Programming. Kenichi Asai and Benjamin C. Pierce acted as editors for these submissions. This issue includes the three accepted articles, each of which provides substantial new material beyond the original conference version. The selected papers represent the importance of various aspects of proof techniques, from theory to practice, all of which aim at verifying realistic programs.