Adapting Proofs-as-Programs: The Curry--Howard Protocol

This monograph details several important advances in the area known as the proofs-as-programs paradigm, a set of approaches to developing programs from proofs in constructive logic. It serves the dual purpose of providing a state-of-the-art overview of the field and detailing tools and techniques to stimulate further research.

One of the book’s central themes is a general, abstract framework for developing new systems of program synthesis by adapting proofs-as-programs to new contexts,…