LLFP : A Logical Framework for modeling External Evidence, Side Conditions, and Proof Irrelevance using Monads

Abstract : We extend the constructive dependent type theory of the Logical Framework 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 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, LLFP, is a conservative extension of LF, and hence it is the appropriate metalanguage for dealing formally with side-conditions in rules or external evidence in logical systems. LLFP arises once the monadic nature of the lock type-constructor, L^P_{M,σ}[-], 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, U^P_{M,σ}[-], in place of Moggi’s monadic let_T, thus simplifying the equational theory. The rules for U^P_{M,σ}[-] permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of LLFP by a novel indirect method based on the encoding of LLFP in LF. We discuss encodings in LLFP of call-by-value λ-calculi, Hoare’s Logic, and Fitch-Prawitz Naive Set Theory.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, Special Issue in honor of Pierre Louis Curien, 〈http://www.lmcs-online.org/index.php〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01146059
Contributeur : Luigi Liquori <>
Soumis le : mercredi 15 mars 2017 - 15:20:39
Dernière modification le : mercredi 16 mai 2018 - 11:24:13
Document(s) archivé(s) le : vendredi 16 juin 2017 - 14:12:22

Fichier

LLFP_LMCS.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01146059, version 2
  • ARXIV : 1702.07214

Citation

Furio Honsell, Luigi Liquori, Petar Maksimovic, Ivan Scagnetto. LLFP : A Logical Framework for modeling External Evidence, Side Conditions, and Proof Irrelevance using Monads. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, Special Issue in honor of Pierre Louis Curien, 〈http://www.lmcs-online.org/index.php〉. 〈hal-01146059v2〉

Partager

Métriques

Consultations de la notice

458

Téléchargements de fichiers

51