The Curry–Howard correspondence for programmers

the logic of programming languages