LLFp

LLFp: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. We extend the constructive dependent type theory of the Logical Framework 𝖫𝖥 with monadic, dependent type constructors indexed with predicates over judgements, called Locks. ...