logic foundations Basic ideas of functional programming, constructive logic, and the Coq proof assistant.