Furio Honsell ; Luigi Liquori ; Petar Maksimovic ; Ivan Scagnetto - $\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

lmcs:3771 - Logical Methods in Computer Science, July 6, 2017, Volume 13, Issue 3 - https://doi.org/10.23638/LMCS-13(3:2)2017
$\mathsf{LLF}_{\cal P}$: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monadsArticle

Authors: Furio Honsell ; Luigi Liquori ; Petar Maksimovic ; Ivan Scagnetto

    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 an $\mathsf{LF}$ type. Standard examples are factoring-out the verification of a constraint or delegating it to an external oracle, or supplying some non-apodictic epistemic evidence, or simply discarding the proof witness of a precondition deeming it irrelevant. This new framework, called Lax Logical Framework, $\mathsf{LLF}_{\cal P}$, is a conservative extension of $\mathsf{LF}$, and hence it is the appropriate metalanguage for dealing formally with side-conditions in rules or external evidence in logical systems. $\mathsf{LLF}_{\cal P}$ arises once the monadic nature of the lock type-constructor, ${\cal L}^{\cal P}_{M,\sigma}[\cdot]$, introduced by the authors in a series of papers, together with Marina Lenisa, is fully exploited. The nature of the lock monads permits to utilize the very Lock destructor, ${\cal U}^{\cal P}_{M,\sigma}[\cdot]$, in place of Moggi's monadic $let_T$, thus simplifying the equational theory. The rules for ${\cal U}^{\cal P}_{M,\sigma}[\cdot]$ permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of $\mathsf{LLF}_{\cal P}$ by a novel indirect method based on the encoding of $\mathsf{LLF}_{\cal P}$ in $\mathsf{LF}$. We discuss encodings in $\mathsf{LLF}_{\cal P}$ of call-by-value $\lambda$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory.


    Volume: Volume 13, Issue 3
    Published on: July 6, 2017
    Accepted on: July 6, 2017
    Submitted on: July 6, 2017
    Keywords: Computer Science - Logic in Computer Science,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Deep Drug Discovery and Deployment; Code: PTDC/CCI-BIO/29266/2017

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1135 times.
    This article's PDF has been downloaded 266 times.