| 2020 | FOSSACS | Spinal Atomic Lambda-Calculus. | David Sherratt, Willem Heijltjes, Tom Gundersen, Michel Parigot |
| 2013 | LICS | Atomic Lambda Calculus: A Typed Lambda-Calculus with Explicit Sharing. | Tom Gundersen, Willem Heijltjes, Michel Parigot |
| 2013 | LPAR | A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus. | Tom Gundersen, Willem Heijltjes, Michel Parigot |
| 2011 | TABLEAUX | A Tentative Atomic Calculus for Natural Deduction. | Tom Gundersen, Michel Parigot |
| 2011 | TABLEAUX | A Symmetric Natural Deduction. | Michel Parigot |
| 2010 | LPAR | A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae. | Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, Michel Parigot |
| 2000 | CSL | On the Computational Interpretation of Negation. | Michel Parigot |
| 1993 | LICS | Strong Normalization for Second Order Classical Natural Deduction | Michel Parigot |
| 1993 | MFCS | Constant Time Reductions in Lambda-Caculus. | Michel Parigot, Paul Rozire |
| 1992 | LPAR | ProPre A Programming Language with Proofs. | Pascal Manoury, Michel Parigot, Marianne Simonot |
| 1992 | LPAR | Lambda-Mu-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. | Michel Parigot |
| 1991 | LPAR | Free Deduction: An Analysis of "Computations" in Classical Logic. | Michel Parigot |
| 1990 | MFCS | Internal Labellings in Lambda-Calculus. | Michel Parigot |
| 1989 | CSL | On the Representation of Data in Lambda-Calculus. | Michel Parigot |
| 1988 | ESOP | Programming with Proofs: A Second Order Type Theory. | Michel Parigot |