LaxLF: Side Conditions and External Evidence as Monads

Abstract : We extend the constructive dependent type theory of the Logical Framework LF with a family of monads indexed by predicates over typed terms. These monads express the effect of factoring-out, postponing , or delegating to an external oracle the verification of a constraint or a side-condition. This new framework, called Lax Logical Framework, LaxF, is a conservative extension of LF, and hence it is the appropriate metalanguage for dealing formally with side-conditions or external evidence in logical systems. LaxF is the natural strengthening of LFP (the extension of LF introduced by the authors together with Marina Lenisa and Petar Maksimovic), which arises once the monadic nature of the lock constructors of LFP is fully exploited. The nature of these monads allows to utilize the unlock destructor instead of Moggi's monadic let_T , thus simplifying the equational theory. The rules for the unlock allow us, furthermore, to remove the monadic constructor once the constraint is satisfied. By way of example we discuss the encodings in LaxF of call-by-value-calculus, Hoare's Logic, and Elementary Affine Logic.
Type de document :
Communication dans un congrès
Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I., Aug 2014, Budapest, Hungary. Springer Verlag, 8634, pp.327-339, Lecture Notes in Computer Science. 〈10.1007/978-3-662-44522-8_28〉
Liste complète des métadonnées

Littérature citée [25 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01146023
Contributeur : Luigi Liquori <>
Soumis le : lundi 27 avril 2015 - 14:53:50
Dernière modification le : jeudi 11 janvier 2018 - 16:25:40
Document(s) archivé(s) le : mercredi 19 avril 2017 - 07:35:00

Fichier

mfcs-14.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Furio Honsell, Luigi Liquori, Ivan Scagnetto. LaxLF: Side Conditions and External Evidence as Monads. Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part I., Aug 2014, Budapest, Hungary. Springer Verlag, 8634, pp.327-339, Lecture Notes in Computer Science. 〈10.1007/978-3-662-44522-8_28〉. 〈hal-01146023〉

Partager

Métriques

Consultations de la notice

134

Téléchargements de fichiers

49