We formalize a higher-order logic with Church style typing. We also formalize an M-set model where the monoid M is a type of substitutions and a base type is interpreted as untyped lambda terms. This M-set model justifies representing untyped lambda terms using higher-order abstract syntax in the higher-order logic. The Autosubst package is used to support reasoning about substitutions and terms.
Formalization: html version; Coq code
Report: pdf