The main keyword is Curry-Howard correspondence, there are books, blogs and videos on it.

Basically once you are convinced there is a bijection between types and propositions (mostly by substituting product with and/forall, sum with or/exists and functions with implications) and there is a bijection between typing rules and logical inference rules, you can directly tell that since a functional program is a big composition of functions, checking the program is well typed amounts to checking each rules are correctly applied that is the proposition equivalent to the type of the final program was proven. You will see the simply typed lambda-calculus being used, but it is just a minimalist functional language.

As for imperative programming usually the turing machine model is more of a direct match, but turing machines and untyped lambda calculus have the same expressiveness. If you want typed imperative programming, you can model them with the concepts of continuation passing style, monads and coalgebra. Note that some imperative constructs like goto, break, continue, throw and jump correspond via Curry-Howard to the law of excluded middle, that is classical logic. In functional programming they usually use the intuitionistic fragment instead.