Full reduction in the face of absurdity

Abstract : Core calculi that model the essence of computations use full reductionsemantics to be built on solid grounds. Expressive type systems forthese calculi may use propositions to refine the notion of types, whichallows abstraction over possibly inconsistent hypotheses. To preservetype soundness, reduction must then be delayed until logical hypotheseson which the computation depends have been proved consistent. Whenlogical information is explicit inside terms, proposition variablesdelay the evaluation by construction. However, logical hypotheses may beleft implicit, for the user's convenience in a surface language orbecause they have been erased prior to computation in an internallanguage. It then becomes difficult to track the dependencies ofcomputations over possibly inconsistent hypotheses.We propose anexpressive type system with implicit coercions, consistent andinconsistent abstraction over coercions, and assumption hiding, whichprovides a fine-grained control of dependencies between computations andthe logical hypotheses they depend on. Assumption hiding opens acontinuum between explicit and implicit use of hypotheses, and restoresconfluence when full and weak reductions are mixed.
Type de document :
Rapport
[Research Report] INRIA. 2014
Liste complète des métadonnées


https://hal.inria.fr/hal-01093910
Contributeur : Didier Rémy <>
Soumis le : jeudi 11 décembre 2014 - 12:24:18
Dernière modification le : mardi 13 décembre 2016 - 15:43:24
Document(s) archivé(s) le : samedi 15 avril 2017 - 08:12:27

Fichier

Scherer-Remy!fich@rr2014.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01093910, version 1

Collections

Citation

Gabriel Scherer, Didier Rémy. Full reduction in the face of absurdity. [Research Report] INRIA. 2014. <hal-01093910>

Partager

Métriques

Consultations de
la notice

100

Téléchargements du document

139