$\mathsf{LLF}_{\cal P}$: 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 $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by a...
| Príomhchruthaitheoirí: | , , , |
|---|---|
| Formáid: | Alt |
| Teanga: | English |
| Foilsithe / Cruthaithe: |
Logical Methods in Computer Science e.V.
2017-07-01
|
| Sraith: | Logical Methods in Computer Science |
| Ábhair: | |
| Rochtain ar líne: | https://lmcs.episciences.org/3771/pdf |