Prior related joint work

• A Reasonably Gradual Type Theory

  
  Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau, Éric Tanter Proceedings of the ACM on Programming Languages, volume 6, number ICFP, pp.931-959, August 2022, ACM Press

• Gradualizing the Calculus of Inductive Constructions

  
  Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau, Éric Tanter ACM Transactions on Programming Languages and Systems, volume 44, number 2, June 2022 Presented at POPL 2022

• The Marriage of Univalence and Parametricity

  
  Nicolas Tabareau, Éric Tanter, Matthieu Sozeau Journal of the ACM, volume 68, number 1, pp.5:1-5:44, January 2021, ACM Press

• A Reasonably Exceptional Type Theory

  
  Pierre-Marie Pédrot, Nicolas Tabareau, Hans Fehrmann, Éric Tanter Proceedings of the ACM on Programming Languages, volume 3, number ICFP, pp.108:1-108:29, August 2019, ACM Press

• Equivalences for Free: Univalent Parametricity for Effective Transport

  
  Nicolas Tabareau, Éric Tanter, Matthieu Sozeau Proceedings of the ACM on Programming Languages, volume 2, number ICFP, pp.92:1-92:29, September 2018, ACM Press Distinguished Paper Award - superseded by JACM article "The Marriage of Univalence and Parametricity" (2021)

• Foundations of Dependent Interoperability

  
  Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter Journal of Functional Programming, volume 28, pp.9:1-9:44, 2018, Cambridge University Press

• Partial Type Equivalences for Verified Dependent Interoperability

  
  Pierre-Evariste Dagand, Nicolas Tabareau, Éric Tanter Proceedings of the 21st ACM SIGPLAN Conference on Functional Programming (ICFP 2016), pp.298-310, Nara, Japan, September 2016, ACM Press

• Gradual Certified Programming in Coq

  
  Éric Tanter, Nicolas Tabareau Proceedings of the 11th ACM Dynamic Languages Symposium (DLS 2015), pp.26-40, Pittsburgh, PA, USA, October 2015, ACM Press