An Effectful Way to Eliminate Addiction to Dependence

• Published in: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Main Authors: Pédrot, Pierre-Marie, Tabareau, Nicolas
• Other Authors: University of Ljubljana, Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Institut Mines-Télécom Paris (IMT)-Institut Mines-Télécom Paris (IMT), Laboratoire des Sciences du Numérique de Nantes (LS2N), Département Automatique, Productique et Informatique (IMT Atlantique - DAPI), IMT Atlantique (IMT Atlantique), European Project: 637339,H2020 ERC,ERC-2014-STG,CoqHoTT(2015)
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2017
• Subjects: [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]; [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; Iceland
• Online Access: https://inria.hal.science/hal-01441829; https://inria.hal.science/hal-01441829/document; https://inria.hal.science/hal-01441829/file/main.pdf; https://doi.org/10.1109/LICS.2017.8005113

International audience We define a monadic translation of type theory, called weaning translation, that allows for a large range of effects in dependent type theory—such as exceptions, non-termination, non-determinism or writing operation. Through the light of a call-by-push-value decomposition, we explain why the traditional approach fails with type dependency and justify our approach. Crucially, the construction requires that the universe of algebras of the monad forms itself an algebra. The weaning translation applies to a version of the Calculus of Inductive Constructions (CIC) with a restricted version of dependent elimination. Finally, we show how to recover a translation of full CIC by mixing parametricity techniques with the weaning translation. This provides the first effectful version of CIC.