${\mathsf{LLF}}_{\mathcal{P}}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

Furio Honsell, Luigi Liquori, Petar Maksimovic +1

We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Lo…