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.
Document type :
Conference papers
Complete list of metadatas

Contributor : Didier Rémy <>
Submitted on : Monday, December 15, 2014 - 3:20:35 PM
Last modification on : Tuesday, January 29, 2019 - 11:58:59 AM


  • HAL Id : hal-01095390, version 1



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⟩



Record views