$\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 |
| الموضوعات: | |
| الوصول للمادة أونلاين: | https://lmcs.episciences.org/3771/pdf |
| الوسوم: |
لا توجد وسوم, كن أول من يضع وسما على هذه التسجيلة!
|