S. Boulier, P. Pédrot, and N. Tabareau, The Next 700 Syntactical Models of Type Theory, CPP, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01445835

W. J. Bowman, Y. Cong, N. Rioux, and A. Ahmed, Type-Preserving CPS Translation of ? and ? Types is Not Not Possible, Proc. ACM Program. Lang. 2, POPL, Article Article 22, vol.33, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01672735

P. Curien, M. Fiore, and G. Munch-maccagnoni, A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, Proceedings of POPL '16, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01256092

P. Curien and H. Herbelin, The duality of computation, ACM SIGPLAN Notices, vol.35, pp.233-243, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00156377

V. Danos, J. Joinet, and H. Schellinx, A new deconstructive logic: linear logic, Journal of Symbolic Logic, 1997.

J. Girard, A new constructive logic: classic logic, Mathematical Structures in Computer Science, 1991.

H. Herbelin, On the Degeneracy of Sigma-Types in Presence of Computational Classical Logic, Proceedings of TLCA 2005 (LNCS), Pawel Urzyczyn, vol.3461, pp.209-220, 2005.

H. Herbelin, A Constructive Proof of Dependent Choice, Compatible with Classical Logic, Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pp.365-374, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00697240

O. Laurent, Étude de la polarisation en logique, 2002.

L. Paul-blain, Call-By-Push-Value: A Functional/Imperative Synthesis (Semantics Structures in Computation, 2004.

Z. Luo, An Extended Calculus of Constructions, 1990.

É. Miquey, A Classical Sequent Calculus with Dependent Types, ACM Transactions on Programming Languages and Systems, vol.41, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01519929

G. Munch-maccagnoni, Syntax and Models of a non-Associative Composition of Programs and Proofs, 2013.
URL : https://hal.archives-ouvertes.fr/tel-00918642