On: Definite clause grammars and symbolic differentiation

[ted_dunning]

This book does it well. It can be a heavy slog:

https://mitpress.mit.edu/9780262536431/the-little-typer/

Here is a free book on how type checking can be used to do mathematical proofs:

https://lean-lang.org/functional_programming_in_lean/