The list of papers miss this one from 1970: https://personal.cis.strath.ac.uk/conor.mcbride/FVMcB-PhD.pdf https://personal.cis.strath.ac.uk/conor.mcbride/FVMcB-

The list of papers miss this one from 1970: https://personal.cis.strath.ac.uk/conor.mcbride/FVMcB-PhD.pdf https://personal.cis.strath.ac.uk/conor.mcbride/FVMcB-PhD.pd... This is thesis of Frederick McBride, father of Connor McBride, who does significant work in dependent types' circles [1]. The thesis describes symbolic computation algorithms, applies them to expression derivative calculation with simplification, and provides not only definition and construction of algebraic types, but also pattern matching over their values. [1] https://personal.cis.strath.ac.uk/conor.mcbride/ https://personal.cis.strath.ac.uk/conor.mcbride/