Plugging-in Proof Development Environments using Locks in LF

Abstract : We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for plugging-in, i.e. gluing together, different Type Theories and proof development environments. The oracle can be invoked either to check that a constraint holds or to provide a suitable witness. The systems are presented in the canonical style developed by the "CMU School". The first system, CLLFP , is the canonical version of the system LLFP, presented earlier by the authors. The second system, CLLF P? , features the possibility of invoking the oracle to obtain also a witness satisfying a given constraint. We discuss encodings of Fitch-Prawitz Set theory, call-by-value λ-calculi, systems of Light Linear Logic, and partial functions.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), A Paraître
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01272647
Contributeur : Luigi Liquori <>
Soumis le : jeudi 11 février 2016 - 11:07:02
Dernière modification le : vendredi 12 janvier 2018 - 11:03:45
Document(s) archivé(s) le : jeudi 12 mai 2016 - 17:31:41

Fichier

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

Identifiants

  • HAL Id : hal-01272647, version 1

Collections

Citation

Furio Honsell, Luigi Liquori, Petar Maksimoviç, Ivan Scagnetto. Plugging-in Proof Development Environments using Locks in LF. Mathematical Structures in Computer Science, Cambridge University Press (CUP), A Paraître. 〈hal-01272647〉

Partager

Métriques

Consultations de la notice

117

Téléchargements de fichiers

51