The Next 700 Syntactical Models of Type Theory, CPP, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01445835
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
A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, Proceedings of POPL '16, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01256092
The duality of computation, ACM SIGPLAN Notices, vol.35, pp.233-243, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00156377
A new deconstructive logic: linear logic, Journal of Symbolic Logic, 1997. ,
A new constructive logic: classic logic, Mathematical Structures in Computer Science, 1991. ,
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. ,
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
Étude de la polarisation en logique, 2002. ,
Call-By-Push-Value: A Functional/Imperative Synthesis (Semantics Structures in Computation, 2004. ,
An Extended Calculus of Constructions, 1990. ,
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
Syntax and Models of a non-Associative Composition of Programs and Proofs, 2013. ,
URL : https://hal.archives-ouvertes.fr/tel-00918642