Proof Nets And Explicit Substitutions. - Roberto Di Cosmo; Delia Kesner; Emmanuel Polonowski (Math. Struct. Comput. Sci., 2003)

Strong Normalization of lambda-mu-mu/tilde-Calculus with Explicit Substitutions. - Emmanuel Polonowski (FoSSaCS, 2004)

Deriving SN from PSN: a general proof technique - Emmanuel Polonowski (CoRR, 2009)

A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables - Tristan Crolard; Emmanuel Polonowski (CoRR, 2009)

LoopW Technical Reference v0.3 - Emmanuel Polonowski (CoRR, 2009)

Extending the loop language with higher-order procedural variables. - Tristan Crolard; Emmanuel Polonowski; Pierre Valarcher (ACM Trans. Comput. Log., 2009)

Generic Environments in Coq - Emmanuel Polonowski (CoRR, 2011)

A program logic for higher-order procedural variables and non-local jumps - Tristan Crolard; Emmanuel Polonowski (CoRR, 2011)

Deriving a Hoare-Floyd logic for non-local jumps from a formulae-as-types notion of control - Tristan Crolard; Emmanuel Polonowski (CoRR, 2011)

DBGen User Manual - Emmanuel Polonowski (CoRR, 2012)

Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control. - Tristan Crolard; Emmanuel Polonowski (J. Log. Algebraic Methods Program., 2012)

Automatically Generated Infrastructure for De Bruijn Syntaxes. - Emmanuel Polonowski (ITP, 2013)