An Applicative Module Calculus. - Judicaël Courant (TAPSOFT, 1997)

A Module Calculus for Pure Type Systems. - Judicaël Courant (TLCA, 1997)

Explicit Universes for the Calculus of Constructions. - Judicaël Courant (TPHOLs, 2002)

Strong Normalization with Singleton Types. - Judicaël Courant (ITRS, 2002)

Proving termination using dependent types: the case of XOR-terms. - Jean-François Monin; Judicaël Courant (Trends in Functional Programming, 2006)

Computationally Sound Typing for Non-interference: The Case of Deterministic Encryption. - Judicaël Courant; Cristian Ene; Yassine Lakhnech (FSTTCS, 2007)

MC2 A module calculus for Pure Type Systems. - Judicaël Courant (J. Funct. Program., 2007)

Towards automated proofs for asymmetric encryption schemes in the random oracle model. - Judicaël Courant; Marion Daubignard; Cristian Ene; Pascal Lafourcade 001; Yassine Lakhnech (CCS, 2008)

Automated Proofs for Asymmetric Encryption. - Judicaël Courant; Marion Daubignard; Cristian Ene; Pascal Lafourcade 001; Yassine Lakhnech (J. Autom. Reason., 2011)

Developer-Proof Prevention of SQL Injections. - Judicaël Courant (FPS, 2020)