Full reduction in the face of absurdity

Abstract : Core calculi that model the essence of computations use full reduction semantics to be built on solid grounds. Expressive type systems for these calculi may use propositions to refine the notion of types, which allows abstraction over possibly inconsistent hypotheses. To preserve type soundness, reduction must then be delayed until logical hypotheses on which the computation depends have been proved consistent. When logical information is explicit inside terms, proposition variables delay the evaluation by construction. However, logical hypotheses may be left implicit, for the user's convenience in a surface language or because they have been erased prior to computation in an internal language. It then becomes difficult to track the dependencies of computations over possibly inconsistent hypotheses.We propose an expressive type system with implicit coercions, consistent and inconsistent abstraction over coercions, and assumption hiding, which provides a fine-grained control of dependencies between computations and the logical hypotheses they depend on. Assumption hiding opens a continuum between explicit and implicit use of hypotheses, and restores confluence when full and weak reductions are mixed.
Type de document :
Communication dans un congrès
ESOP'2015: European Conference on Programming Languages and Systems, Apr 2015, London, United Kingdom. Proceedings of the 24th European Conference on Programming Languages and Systems, 2015
Liste complète des métadonnées

https://hal.inria.fr/hal-01095390
Contributeur : Didier Rémy <>
Soumis le : lundi 15 décembre 2014 - 15:20:35
Dernière modification le : mardi 29 janvier 2019 - 11:58:59

Identifiants

  • HAL Id : hal-01095390, version 1

Collections

Citation

Gabriel Scherer, Didier Rémy. Full reduction in the face of absurdity. ESOP'2015: European Conference on Programming Languages and Systems, Apr 2015, London, United Kingdom. Proceedings of the 24th European Conference on Programming Languages and Systems, 2015. 〈hal-01095390〉

Partager

Métriques

Consultations de la notice

155