$\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...
Сохранить в:
| Главные авторы: | , , , |
|---|---|
| Формат: | Artigo |
| Язык: | Inglês |
| Опубликовано: |
Logical Methods in Computer Science e.V.
2017-07-01
|
| Серии: | Logical Methods in Computer Science |
| Предметы: | |
| Online-ссылка: | https://lmcs.episciences.org/3771/pdf |
| Метки: |
Нет меток, Требуется 1-ая метка записи!
|