Full reduction in the face of absurdity - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2015

Full reduction in the face of absurdity

Résumé

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.
Fichier non déposé

Dates et versions

hal-01095390 , version 1 (15-12-2014)

Identifiants

  • HAL Id : hal-01095390 , version 1

Citer

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. ⟨hal-01095390⟩

Collections

INRIA INRIA2
119 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More