Harmonic Type Theory
Charles Alexander Stewart

C. A. Stewart: Dresden, Germany, June 2002. Harmonic Type Theory. Lecture course delivered to the Workshop on Proof Theory and Computation, held at Dresden University of Technology.


Despite all the progress made in semantics of programming languages, it is still a scary place for the beginner. By applying insights from proof theory and the philosophy of language, the theory of harmony in logic and type theory hopes to provide a more natural approach than either denotational or operational approaches.

This course consisted of five tutorial lectures. The slides used for the talks are available (PDF, 34 pages, 2002).