| 2024 | WoLLIC | Intersection Types via Finite-Set Declarations. | Fairouz Kamareddine, Joe B. Wells |
| 2023 | SYNASC | The paradoxes and the infinite dazzled ancient mathematics and continue to do so today. | Fairouz Kamareddine, Jonathan P. Seldin |
| 2015 | CSR | Automath Type Inclusion in Barendregt's Cube. | Fairouz Kamareddine, Joe B. Wells, Daniel Lima Ventura |
| 2010 | WoLLIC | Intersection Type Systems and Explicit Substitutions Calculi. | Daniel Lima Ventura, Mauricio Ayala-Rincn, Fairouz Kamareddine |
| 2008 | CiE | Principal Typings for Explicit Substitutions Calculi. | Daniel Lima Ventura, Mauricio Ayala-Rincn, Fairouz Kamareddine |
| 2008 | ICTAC | A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables. | Fairouz Kamareddine, Karim Nour, Vincent Rahli, J. B. Wells |
| 2007 | SYNASC | The Gradual Computerisation of Mathematics in MathLang. | Fairouz Kamareddine |
| 2004 | LPAR | Second-Order Matching via Explicit Substitutions. | Flvio L. C. de Moura, Fairouz Kamareddine, Mauricio Ayala-Rincn |
| 2002 | LATIN | Parameters in Pure Type Systems. | Roel Bloo, Fairouz Kamareddine, Twan Laan, Rob Nederpelt |
| 2002 | SOFSEM | On Functions and Types: A Tutorial. | Fairouz Kamareddine |
| 2001 | FLOPS | Refining the Barendregt Cube Using Parameters. | Fairouz Kamareddine, Twan Laan, Rob Nederpelt |
| 2001 | PPDP | De Bruijn's Syntax and Reductional Equivalence of Lambda-Terms. | Fairouz Kamareddine, Roel Bloo, Rob Nederpelt |
| 2000 | PPDP | Unification via | Mauricio Ayala-Rincn, Fairouz Kamareddine |
| 1999 | PPDP | On Formalised Proofs of Termination of Recursive Functions. | Fairouz Kamareddine, Franois Monin |