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.
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/