An Abstract Machine for Lambda-Terms Normalization. - Pierre Crégut (LISP and Functional Programming, 1990)

Interprétation abstraite pour améliorer la représentation des environnements dans les langages fonctionnels. - Pierre Crégut (JTASPEFT/WSA, 1991)

A Protocol for Supporting the ABT/DT Capability. - Pierre Crégut; Fabrice Guillemin; Barbara Heyd (ICNP, 1996)

A Modular Coding of UNITY in COQ. - Barbara Heyd; Pierre Crégut (TPHOLs, 1996)

Progress Properties for Empty UNITY Programs. - Pierre Crégut; Barbara Heyd (Inf. Process. Lett., 1999)

Improving the Security of Downloadable Java Applications With Static Analysis. - Pierre Crégut; Cuihtlauac Alvarado (Bytecode@ETAPS, 2005)

MOBIUS: Mobility, Ubiquity, Security. - Gilles Barthe; Lennart Beringer; Pierre Crégut; Benjamin Grégoire; Martin Hofmann 001; Peter Müller 001; Erik Poll; Germán Puebla; Ian Stark; Eric Vétillard (TGC, 2006)

The MOBIUS Proof Carrying Code Infrastructure. - Gilles Barthe; Pierre Crégut; Benjamin Grégoire; Thomas P. Jensen; David Pichardie (FMCO, 2007)

Extracting Control from Data: User Interfaces of MIDP Applications. - Pierre Crégut (TGC, 2007)

Strongly reducing variants of the Krivine abstract machine. - Pierre Crégut (High. Order Symb. Comput., 2007)

Developing and certifying Datalog optimizations in coq/mathcomp. - Pierre-Léo Bégay; Pierre Crégut; Jean-François Monin (CPP, 2021)