Observational Equivalence and Program Extraction in the Coq Proof Assistant. - Nicolas Oury (TLCA, 2003)

Extensionality in the Calculus of Constructions. - Nicolas Oury (TPHOLs, 2005)

Pattern matching coverage checking with dependent types using set approximations. - Nicolas Oury (PLPV, 2007)

The power of Pi. - Nicolas Oury; Wouter Swierstra (ICFP, 2008)

First-Class Type Classes. - Matthieu Sozeau; Nicolas Oury (TPHOLs, 2008)

PiSigma: Dependent Types without the Sugar. - Thorsten Altenkirch; Nils Anders Danielsson; Andres Löh; Nicolas Oury (FLOPS, 2010)

Equilibrium and Termination - Vincent Danos; Nicolas Oury (DCM, 2010)

Coloured stochastic multilevel multiset rewriting. - Nicolas Oury; Gordon D. Plotkin (CMSB, 2011)

Handlers in action. - Ohad Kammar; Sam Lindley; Nicolas Oury (ICFP, 2013)

Canonical Labelling of Site Graphs. - Nicolas Oury; Michael Pedersen; Rasmus L. Petersen (CompMod, 2013)

Equilibrium and termination II: the case of Petri nets. - Vincent Danos; Nicolas Oury (Math. Struct. Comput. Sci., 2013)

Multi-level modelling via stochastic multi-level multiset rewriting. - Nicolas Oury; Gordon D. Plotkin (Math. Struct. Comput. Sci., 2013)

Bio Simulators: a web UI for biological simulation. - Michael Pedersen; Nicolas Oury; Colin Gravill; Andrew Phillips (Bioinform., 2014)