Master's thesis: Constructing Calculations from Consecutive Choices (C4P)
My thesis describes a computer program which helps learning and professional programmers as well as mathematicians to construct and review calculations and calculational proofs. For didactic and other purposes, the responsibility for the design of programs and proofs is on the human user. The computer, on the other hand, does all the substitution and formal pattern matching work, thereby freeing the human from petty work and guaranteeing correctness of proofs and calculations. It will also offer substantial guidance for the human intuition that's driving the proofs. The thesis specifies such a proof tool by describing the logical language, the rules of proof, and how the user can interact with proofs.