A theory of reflexive computation based on soft intuitionistic logic

Hubert Godfroy 1 Jean-Yves Marion 1
1 CARTE - Theoretical adverse computations, and safety
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Computational Reflection is a paradigm in which the computational mechanisms controls the different levels of data interpretation. It can be decomposed into two processes: (i) reification, which turns a program into a data and (ii) reflection, which, inversely, installs a data as a program or a context in order to be run. We present a logical account of reflection based on a confluent lambda-calculus. We define two type assignment systems called Soft Intuitionistic Logic (SIL) and Intuition-istic Logic with Promotion (PIL) in which we introduce the exponential modality ! of linear logic. The duality between reification and reflection is to be found in the soft-promotion rule in SIL (resp. in the promotion rule in PIL) and in the dereliction rule. We also show that SIL (or PIL) is a framework in which partial evaluation can be efficiently performed. Finally, we add a control operator, which reifies its evaluation context. Thus a program may have full control of its computational state. We extend the type system with classical logic and semantics is provided by Krivine abstract machine. We establish the soundness of our type system.
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01394263
Contributeur : Hubert Godfroy <>
Soumis le : mercredi 9 novembre 2016 - 09:41:58
Dernière modification le : mardi 17 avril 2018 - 09:08:36
Document(s) archivé(s) le : mardi 14 mars 2017 - 22:23:24

Fichiers

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

Licence


Distributed under a Creative Commons Paternité - Partage selon les Conditions Initiales 4.0 International License

Identifiants

  • HAL Id : hal-01394263, version 1

Collections

Citation

Hubert Godfroy, Jean-Yves Marion. A theory of reflexive computation based on soft intuitionistic logic. 2016. 〈hal-01394263〉

Partager

Métriques

Consultations de la notice

323

Téléchargements de fichiers

104