Fairouz Dib Kamareddine
Fairouz Dib Kamareddine
Professor
  • : +44 131 451 3868
    • : +44 131 451 8179

School of Mathematical and Computer Sciences,
Heriot-Watt University,Edinburgh
UK

Education

  • PhD (Semantics in a Frege structure) University of Edinburgh, 1989
  • MSc with distinction (Computer Science) University of Essex, 1983
  • Diploma with distinction (Programming & Microprocessing) University of Essex, 1982
  • Ma^trise (BSc) with distinction (Pure Mathematics) Lebanese University, Beirut 1980

 

Biography

Fairouz Kamareddine earned a Maîtrise (French B.Sc.) in Pure Mathematics, from the Lebanese University, Beirut in 1980. Since she obtained her Maîtrise with the highest distinction (she was the top (number 1) in Pure Mathematics in all the branches of the university), she was awarded a scholarship to study for a PhD in her choice of 3 countries: France, the UK or the USA. Although her mother wanted France and her father wanted the USA, she chose the UK because she wanted to learn English and she wanted to remain in closer distance to the middle east (the USA was farther away). Since then, she has become a regular visitor to the USA (and France) where she has established working relationships that she values tremendously.

Professor Kamareddine is leading a distinguished and successful academic career at the interface of Mathematics, Logic and Computer Science as witnessed by her multiple learned fellowships and charters, her large number of worldwide consultancy assignments, especially on education issues, her many individual and network grants from all levels of institutions ranging from universities all the way up to the United Nations, her large number of positions as journal editor and memberships on programme committees and organisation and meetings. Equally, she frequently appears as invited speaker at worldwide international research as well as eductational events. Her experience in research, staff, and teaching administration is extensive and at least commensurate with her 12 years as full professor. Most notably, she has and is playing leading roles in the development, administration and implementation of interdisciplinary, international, and academia-industry collaborations and networks. Since 2001 she has acted as an expert evaluator, rapporteur and vice-chair for the MAT-ENG panels of the EU research frameworks (5, 6 and 7) of the European Union.

 

Research Interest

 

Professional Activities:

OFFICIAL UNIVERSITY EMPLOYMENT HISTORY

  • Full Professor (permanent position), Heriot-Watt University, School of Mathematical and Com-puter Sciences, since 1 August 1998.
  • Visiting professor, Universit de Savoie, Chambery, France, 21 May-11 June 2008 and 5 July-17 July 2008.
  • Reader (permanent position), Glasgow University, Computing Science, 1997{1998. Lecturer (permanent position), Glasgow University, Computing Science, 1987{1997.
  • Postdoctoral Researcher, Eindhoven University of Technology, Maths and Computing Sc., 1991{ 1992.
  • Mathematics Tutor, University of Edinburgh, Mathematics department, 1984{1987. Mathematics Lecturer, Lebanese University, Tyre, Lebanon, Autumn 1980.

VISITING RESEARCH PLACEMENTS

  • A number of short term visits to the University of T•ubingen (Professor Uwe M•onnich), Germany. Between 1989 and 1990.
  • Numerous lengthy spring/summer visits to Eindhoven University of Technology (Professors de Bruijn and Baeten and Dr Nederpelt), Eindhoven, the Netherlands. Between 1992 and 2002.
  • A number of short term visits to the University of Nijmegen (Professor Barendregt), the Nether-lands. Starting 1991.
  • A number of short term visits to the University of Amsterdam (Dr Inge Bethke) and to CWI (Professor Klop), Amsterdam, the Netherlands. Starting 1992.
  • A number of short term visits to Boston University (Professor Assaf Kfoury), USA, Between 1995 and 1998.
  • A number of short term visits to the Universit de Savoie (Professor Ren David and Drs Karim Nour and Christophe Ra alli), Chambery, France, since 1997.
  • A number of short term visits to the University of Brasilia (Professors Ayala-Rincon and de Moura), Brasilia, Brazil, since 1999.
  • A number of short term visits to Cornell University (Professor Robert Constable), Ithaca, NY, USA. 2009 and 2010.
  • A number of short term visits to the University of Tsukuba (Professor Tetsuo Ida), Tsukuba, Japan. 2008 and 2012.
  • Distinguished Professor, University of Lethbridge and University of Calgary, Canada, Jan-uary/February 2015.

 

Publications

JOURNAL PUBLICATIONS

  1. Fairouz Kamareddine, Karim Nour, Vincent Rahli and J.B. Wells, On Realisability Seman-tics for Intersection Types with Expansion Variables. Fundamenta Informatica Volume 121(1-4), Pages 153-184. 2012. ISSN 0169-2968, IOS Press.
  2. Fairouz Kamareddine, Vincent Rahli and J.B. Wells, Reducibility proofs in the lambda calculus. Fundamenta Informatica, Volume 121(1-4), Pages 121-152. 2012. ISSN 0169-2968, IOS Press.
  3. Daniel Ventura, Mauricio Ayala-Rincon and Fairouz Kamareddine, Explicit substitutions calculi with one step Eta-reduction decided explicitly. Logic Journal of the IGPL, Volume 17, issue 6, Pages 697-718. 2009. ISSN 1367-0751, Oxford University Press.
  4. Flavio de Moura, Mauricio Ayala-Rincon and Fairouz Kamareddine, Higher Order Uni ca-tion: A structural relation between Huet's method and the one based on explicit substitutions. The journal of Applied Logic, Volume 6, issue 1, Pages 71{108. Elsevier, North-Holland. ISSN 1570-8683. March 2008.
  5. Fairouz Kamareddine and Karim Nour. A completeness result for a realisability semantics for an intersection type system. Annals of Pure and Applied Logic, Volume 146, Pages 180-198, May 2007. ISSN: 0168-0072. Elsevier, North-Holland.
  6. Arbiser, Kamareddine and R os, The Weak Normalisation of the simply typed  se-calculus. the Logic Journal of the Interest Group of Pure and Applied Logic, Volume 15, issue 2, Pages 121-147, 2007. ISSN 1367-0751, Oxford University Press.
  7. Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel and Joe Wells. Digitised Math-ematics: Computerisation vs. Formalisation. Review of the National Centre for Digitisation, Volume 10, Pages 1{8, Belgrade, Serbia, 2007.
  8. de Moura, Ayala-Rincon, and Kamareddine, SUBSEXPL: A Tool for Simulating and Com-paring Explicit Substitutions Calculi. Journal of Applied Non-classical Logics Volume 16, issue 1-2, Pages 119-150, 2006. Editions Hermes-Lavoisier.
  9. Kamareddine, Typed -calculi with uni ed binders, Journal of Functional Programming. Volume 15, issue 5, Pages 71-796, September 2005. ISSN: 0956-7968, Cambridge University Press.
  10. Ayala-Rincon, de Moura and Kamareddine, Comparing and Implementing calculi of explicit substitutions with Eta reduction, Annals of Pure and Applied Logic. Volume 134, issue 1, Pages 5-41, June 2005. ISSN: 0168-0072. Elsevier, North-Holland.
  11. Kamareddine and Bloo, De Bruijn's syntax and reductional behaviour of lambda terms: the untyped case, Journal of Logic and Algebraic Programming. Volume 62, issue 1, Pages 109{131, January 2005. ISSN: 1567-8326. Elsevier, North-Holland.
  12. Kamareddine and Bloo, De Bruijn's syntax and reductional behaviour of lambda terms: the typed case, Journal of Logic and Algebraic Programming. Volume 62, issue 2, Pages 159-189, February 2005. ISSN: 1567-8326. Elsevier, North-Holland.
  13. Kamareddine and Nederpelt, A re nement of de Bruijn's formal language of mathematics. Journal of Logic, Language and Information, Volume 13, Number 3, Pages 287{340. June 2004. ISSN: 0925 8531, Kluwer Academic Publishers.
  14. Kamareddine, Monin and Ayala-Rincon, On automating the extraction of programs from proofs using product types, Journal of Revista Colombiana de Computacion (the Columbian Journal of Computation), Volume 4, Number 2, Pages 29{48. June 2004. ISSN 1657 2831.
  15. Ayala and Kamareddine, On Applying the  se-style of uni cation for simply-typed higher order uni cation, Mathematica Contemporanea, Volume 24, Pages 1-22. July 2003. INSS 0103-9059. Sociedade Brasileira de Matematica.
  16. Kamareddine and Qiao, Formalising strong normalisation proofs of explicit substitution calculi in ALF. Journal of Automated Reasoning, Volume 30, Pages 59-98, January 2003. ISSN 0168 7433. Kluwer Academic Publishers.
  17. Kamareddine, Laan and Nederpelt, Revisiting the notion of function, Journal of Logic and Algebraic Programming, Volume 54, issue 1-2, Pages 65-107, January 2003. ISSN: 1567-8326. Elsevier, North-Holland.
  18. Borghuis, Kamareddine and Nederpelt, Formalising belief revision in type theory, the Logic Journal of the Interest Group of Pure and Applied Logic, Volume 10, issue 5, Pages 461-500, September 2002, ISSN 1367-0751, Oxford University Press.
  19. Kamareddine and Monin, An extension of an automated termination method of recursive functions, International Journal of Foundations of Computer Science, Volume 13, Number 3, pages 361-386, June 2002. ISSN 0129-0541. World-Scienti c Publishing Company.
  20. Kamareddine and R os, Pure Type Systems with de Bruijn indices The Computer Journal, Volume 45(2), pages 187-201, ISSN 0010 4620, March 2002. Oxford University Press.
  21. Kamareddine, Laan and Nederpelt, Types in logic and mathematics before 1940, The Bulletin of Symbolic Logic, Volume 8, issue 2, pages 185-245, June 2002, Association for Symbolic Logic.
  22. Ayala and Kamareddine, Uni cation via  se-Style of Explicit Substitution, the Logic Journal of the Interest Group of Pure and Applied Logic Volume 9(4), pages 521-555, 2001, ISSN 1367-0751, Oxford University Press.
  23. Kamareddine and Laan, A Correspondence between Martin-L•of Type Theory, the Rami ed Theory of Types and Pure Type Systems Logic, Language and Information 10(3), pages 375-402, 2001, ISSN: 0925 8531, Kluwer Academic Publishers.
  24. Kamareddine, Reviewing the classical and de Bruijn notation in the -calculus and Pure Type Systems, the journal of Logic and Computation 11(3), pages 361-392, June 2001, ISSN 0955 792X, Oxford University Press.
  25. Kamareddine and R os, Relating the Lambda sigma and Lambda s styles of Explicit Sub-stitutions, the journal of Logic and Computation 10(3), pages 349-380, June 2000, ISSN 0955 792X, Oxford University Press.
  26. Kamareddine, A reduction relation for which postponment of K-contractions, Conservation and Preservation of Strong Normalisation hold, the journal of Logic and Computation 10(5), pages 721-738, ISSN 0955 792X, 2000, Oxford University Press.
  27. Kamareddine, Bloo and Nederpelt, On -conversion in the -cube and the combination with abbreviations, Annals of Pure and Applied Logics 97(1), 27-45, 1999, ISSN: 0168-0072, North-Holland.
  28. Kamareddine and R os, Bridging de Bruijn indices and variable names in explicit substitu-tions calculi, the Logic Journal of the Interest Group of Pure and Applied Logic 6(6), 843-874, 1998, ISSN 1367-0751, Oxford University Press.
  29. Kamareddine, The Soundness of Explicit Substitution with Nameless Variables, International Journal of Foundations of Computer Science 9(3), 321-349, 1998, ISSN: 0129-0541, World-Scienti c Publishing Company.
  30. Kamareddine, R os and Wells, Calculi of Generalised -Reduction and Explicit Substitutions: The Type free and Simply Typed Versions, the Journal of Functional and Logic Programming, Volume 1998, ISSN 1080-5230, MIT Press. Invited Publication.
  31. Kamareddine and R os, Extending a -calculus with explicit substitution which preserves strong normalisation into a con uent calculus on open terms. Functional Programming 7(4), 395-420, 1997, ISSN: 0956-7968, Cambridge University Press.
  32. Bloo, Kamareddine and Nederpelt, The Barendregt Cube with de nitions and generalised reduction, Information and Computation 126(2), 123-143, 1996, ISSN: 0890-5401, Academic Press.
  33. Kamareddine and Nederpelt, A useful -notation, Theoretical Computer Science 155, 85-109, 1996, ISSN: 0304-3975, North-Holland.
  34. Kamareddine and Nederpelt, Canonical Typing and -conversion in the Barendregt Cube, Functional Programming 6 (2), 245-267, 1996, ISSN: 0956-7968, Cambridge University Press.
  35. Kamareddine and Laan, A re ection on Russell's Rami ed Types and Kripke's Hierarchy of Truths, Interest Group of Pure and applied Logic 4(2), 195-213, 1996, ISSN 0945-9103, Oxford University Press.
  36. Kamareddine and Nederpelt, Re ning reduction in  -calculus, Functional Programming 5(4), 637-651, 1995, ISSN: 0956-7968, Cambridge University Press. Invited Publication.
  37. Kamareddine, A type free theory and collective/distributive predication, Logic, Language and Information 4 (2), 85-109, 1995, ISSN: 0925 8531, Kluwer Academic Publishers.
  38. Kamareddine, Important Issues in Foundational Formalisms, Interest Group of Pure and applied Logic 3 (2,3), 291-317, 1995, ISSN 0945-9103, Oxford University Press.
  39. Kamareddine and Nederpelt, A uni ed approach to type theory through a re ned -calculus, Theoretical Computer Science 136, 183-216, 1994, ISSN: 0304-3975, North-Holland.
  40. Kamareddine and Nederpelt, On stepwise explicit substitution, International Journal of Foundations of Computer Science 4 (3), 197-240, 1993, ISSN: 0129-0541, World Scienti c Pub-lishing Company.
  41. Kamareddine and Klein, Polymorphism, Type containment and Nominalization, Logic, Lan-guage and Information 2, 171-215, 1993, ISSN: 0925 8531, Kluwer Academic Publishers.
  42. Kamareddine, Set Theory and Nominalisation II, Logic and Computation 2 (6), 687-707, 1992, ISSN: 0955-792X, Oxford University Press.
  43. Kamareddine, Set Theory and Nominalisation I, Logic and Computation 2 (5), 579-604, 1992, ISSN: 0955-792X, Oxford University Press.
  44. Kamareddine, -terms, logic, determiners and quanti ers, Logic, Language and Information 1 (1), 79-103, 1992, ISSN: 0925 8531, Kluwer Academic Publishers.
  45. Kamareddine, A system at the cross roads of logic and functional programming, Science of Computer Programming 19, 239-279, 1992, ISSN: 0167-6423, North-Holland.

CHAPTERS IN BOOKS

  1. FairouzKamareddine, Laan and Nederpelt, A history of types. In Dov. M Gabbay, Francis Je ry Pelletier and John Woods, editors: Logic: A History of its Central Concepts. 11, HHL, : San Diego: North Holland, 2012, pages. 451-511.
  2. Fairouz Kamareddine, Twan Laan and Robert Constable. Russell's Orders in Kripke's Theory of Truth and Computational Type Theory. In Dov. M Gabbay, Akihiro Kanamori and John Woods, editors: Sets and Extensions in the Twentieth Century, Volume 6, HHL, : San Diego: North Holland, 2012, Pages. 801-845.
  3. Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel and Joe Wells. Gradual Computer-isation/Formalisation of mathematical texts into Mizar In From Insight to Proof, Festschrift in honour of Andrzej Trybulec, Roman Matuszewski and Anna Zalewska (eds), Studies in Logic, Grammar and Rhetoric, Volume 10(23), Pages 95-120, University of Bialystok, Polish Associa-tion for Logic and Philosophy of Science, 2007.
  4. Kamareddine, Laan and Nederpelt, De Bruijn's Automath and Pure Type Systems. In Thirty Five Years of Automating Mathematics, edited by Fairouz Kamareddine Kluwer Applied Logic series. Volume 28. Pages 71-123. November 2003. ISBN 1-4020-1656-5. Kluwer Academic Publishers.
  5. Kamareddine, Are types needed for Natural Language?, in Applied Logic: What and Why, edited by Laszlo Polos and Michael Masuch, Pages 79-120, 1995. Kluwer Academic Publishers, ISBN 0-7923-30951.

BOOKS

  1. Kamareddine, Laan and Nederpelt, A Modern Perspective on Type Theory From its Origins Until Today. Kluwer Academic Publishers. May 2004. ISBN 1-4020-2334-0.
  2. Nederpelt and Kamareddine, Logical Reasoning, a rst step. King's College Press. April 2004. ISBN 0-9543006-7-X.

EDITED ISSUES/BOOKS

  1. Adel Bouhoula, Tetsuo Ida and Fairouz Kamareddine editors. Proceedings of Symbolic Com-putation in Software Science 2012 (SCSS2012). EPTCS ?? 2013.
  2. Mauricio Ayala-Rincon, Elaine Pimentel and Fairouz Kamareddine editors. Proceedings of LSFA 2008 and LSFA 2009. Theoretical Computer Science 412(37), 151 pages. 2011.
  3. Mauricio Ayala-Rincon and Fairouz Kamareddine editors. Proceedings of the Fourth Work-shop on Logical and Semantic Frameworks with Applications LSFA'09. Electr. Notes Theor. Comput. Sci. 256: 135 pages. 2009.
  4. Kamareddine editor, Special issue on Variants of logics: from HOL to the calculus of con-structions to teaching mathematical proofs on computers. Journal of Applied Logic. Volume 2, issue 2, Pages 169{239. June 2004. ISSN 1570-8683. Elsevier, North-Holland.
  5. Kamareddine editor, Special issue on Mathematical Knowledge Management Symposium. Electronic Notes in Theoretical Computer Science 93, Pages 1{201, February 2004. ISBN 044451290X, Elsevier.
  6. Kamareddine editor, Thirty Five Years of Automating Mathematics. Edited book in the Kluwer Applied Logic series. Volume 28. 328 pages. November 2003. ISBN 1-4020-1656-5. Kluwer Academic Publishers.
  7. Geuvers and Kamareddine editors, Special issue on Mathematics, Logic and Computation (MLC), Electronic Notes in Theoretical Computer Science 85(7). 2003. ISBN 044451290X, Elsevier.
  8. Kamareddine editor, Special issue on Mechanising and Automating Mathematics: In honour of N.G. de Bruijn. Journal of Automated Reasoning. Volume 29, issues 3 and 4, Pages 183-418. 2002. ISSN 0168 7433. Kluwer Academic Publishers.
  9. Kamareddine editor, Special issue on rewriting and theorem proving. Journal of the Interest group of Pure and Applied Logic, 9(3), Pages 353{512, 2001. ISSN 1367-0751, Oxford University Press.
  10. Kamareddine editor, Special issue on Type and set theoretical foundation of computation. Journal of Logic and Computation. Volume 11, Issue 3, Pages 359{498, 2001. ISSN 0955 792X, Oxford University Press.
  11. Kamareddine and Klop, editors, Special issue on Type Theory and Term Rewriting. Journal of Logic and Computation. Volume 10, Issue 3, Pages 321{492, 2000. ISSN 0955 792X, Oxford University Press.

REFEREED CONFERENCE PUBLICATIONS

  1. Flavio de Moura A.V. Barbosa, Mauricio Ayala-Rinc?n and Fairouz Kamareddine. A Flex-ible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi. Fifth Brazilian Workshop on Logical and Semantic Frameworks, with Applications (LSFA2010) , Natal, Brazil. Electr. Notes Theor. Comput. Sci. 269: 41-54 (2011).
  2. Daniel Lima Ventura, Mauricio Ayala-Rincon and Fairouz Kamareddine, Intersection Type Systems and Explicit Substitutions Calculi Anuj Dawar, Ruy J. G. B. de Queiroz (Eds.): Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010, Brasilia, Brazil, July 6-9, 2010. Proceedings. Lecture Notes in Computer Science 6188, Pages 232-246. Springer 2010, ISBN 978-3-642-13823-2.
  3. Robert Lamar, Fairouz Kamareddine, J. B. Wells: MathLang Translation to Isabelle Syn-tax. Calculemus/MKM 2009, Jacques Carette, Lucas Dixon, Claudio Sacerdoti Coen, Stephen M. Watt (Eds.): Intelligent Computer Mathematics, 16th Symposium, Calculemus 2009, 8th International Conference, MKM 2009, Held as Part of CICM 2009, Grand Bend, Canada, July 6-12, 2009. Proceedings. Lecture Notes in Computer Science 5625 Springer 2009, ISBN 978-3-642-02613-3, Pages 373-388.
  4. Daniel Lima Ventura, Mauricio Ayala-Rincon and Fairouz Kamareddine, Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices Pro-ceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming. Electronic Proceedings in Theoretical Computer Science, Volume 15, DOI: 10.4204/EPTCS.15, ISSN: 2075-2180, January 2010.
  5. Fairouz Kamareddine and Vincent Rahli, Simpli ed Reducibility Proofs of Church-Rosser for - and -reduction. Third Workshop on Logical and Semantic Frameworks, with Applica-tions, Salvador, Bahia, Brasil, 26 August 2008. Electr. Notes Theor. Comput. Sci. 247: 85-101 (2009).
  6. Fairouz Kamareddine, Vincent Rahli, Karim Nour and J.B. Wells, A complete realisability semantics for intersection types and in nite expansion variables. In 5th International Collo-quium on Theoretical Aspects of Computing, ICTAC 2008, Lecture Notes in Computer Science volume 5160, Pages 171-185, J.S. Fitzgerald, A.E. Haxthausen and H. Yenigun (Eds.), Springer-Verlag, 1{3 September 2008, The Marmara, Istanbul, Turkey.
  7. Fairouz Kamareddine, Vincent Rahli and J.B. Wells, Reducibility proofs in the lambda calculus with intersection types. 4th Workshop on Intersection Types and Related Systems (ITRS '08) Torino, Italy, 25 March 2008.
  8. Fairouz Kamareddine, Vincent Rahli, Karim Nour and J.B. Wells, Realisability Semantics For Intersection Types and Expansion Variables. 4th Workshop on Intersection Types and Related Systems (ITRS '08) Torino, Italy, 25 March 2008.
  9. Daniel Lima Ventura, Mauricio Ayala-Rincon and Fairouz Kamareddine, Intersection Type Systems with de Bruijn Indices, CLE 30 anos/ XV EBL/XIV SLAM (30th Anniversary of the Centre for Logic, Epistemology and the History of Science, UNICAMP/15th Brazilian Logic Conference/ 14th Latin-American Symposium on Mathematical Logic), May 11-17, 2008, Paraty, RJ, Brazil.
  10. Daniel Lima Ventura, Mauricio Ayala-Rincon and Fairouz Kamareddine, Principal Typings for Explicit Substitutions calculi, Fourth Conference on Computability in Europe, Logic and Theory of Algorithms, 15-20 June 2008, Athens, Greece. Lecture Notes in Computer Science volume 5028. Pages 567-578. Arnold Beckmann and Costas Dimitracopoulos and Benedikt L•owe (editors). ISBN 978-3-540-69405-2. Springer-Verlag, 2008.
  11. Kamareddine and Wells, Computerising mathematical texts in MathLang, Second Workshop on Logical and Semantic Frameworks, with Applications, Ouro Preto, Minas Gerais, Brazil, 28 August 2007. ENTCS, volume 205, Pages 5-30, Ayala-Rincon and Heusler (editors). ISSN: 1571-0661, April 2008. Elsevier.
  12. Kamareddine, Maarek, Retel and Wells, Narrative structure of mathematical texts, Mathe-matical Knowledge Management, Sixth International Conference, MKM 2007, Lecture Notes in AI, 4573, Pages 296-312, M. Kauers, Manfred Kerber, Robert Miner and Wolfgang Windsteiger (Eds), ISBN 978-3-540-73083-5. Springer-Verlag, June 2007.
  13. Kamareddine, Lamar, Maarek and Wells, Restoring natural language as a computerised mathematics input method, Mathematical Knowledge Management, Sixth International Con-ference, MKM 2007, Lecture Notes in AI, 4573, Pages 280-295, M. Kauers, Manfred Kerber, Robert Miner and Wolfgang Windsteiger (Eds), ISBN 978-3-540-73083-5. Springer-Verlag, June 2007.
  14. Ventura, Ayala-Rincon, and Kamareddine, Explicit Substitutions Calculi with Explicit Eta rules which Preserve Subject Reduction, Brazilian Workshop on Logical and Semantic Frame-works, with Applications, Natal, Brazil, 17 September 2006.
  15. Kamareddine, Maarek and Wells, Toward an Object-Oriented Structure for Mathemati-cal Text, Mathematical Knowledge Management, Fourth International Conference, MKM 2005, Lecture Notes in AI 3863, Pages 217-233, Michael Kohlhase (Ed), Springer-Verlag, 2006.
  16. De Moura, Kamareddine and Ayala, Second-Order Matching via Explicit Substitution, 11th Intl. Conf. on Logic for Programming, Arti cial Intelligence and Reasoning, LPAR'04, March 14-18, 2005, Montevideo, Uruguay. Lecture Notes in Computer Science 3452, Pages 433-448, Franz Baader and Andrei Voronkov (Eds), ISBN: 3-540-25236-3 Springer-Verlag, February 2005.
  17. De Moura, Ayala and Kamareddine, SUBSEXPL: A Framework for Simulating and Compar-ing Explicit Substitution Calculi, 5th International Workshop on the Implementation of Logics, satellite workshop of LPAR 2004. Montevideo, Uruguay, 13 March 2005.
  18. Kamareddine, Maarek and Wells, Flexible encoding of mathematics on the computer, Mathe-matical Knowledge Management, Third International Conference, MKM 2004, Lecture Notes in Computer Science 3119, Pages 160{174. Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec (Eds), ISBN 3 540 23029 7. Springer-Verlag, September 2004.
  19. Kamareddine, Maarek and Wells, MathLang: An experience driven language of mathematics, In Mathematical Knowledge Management. Electronic Notes in Theoretical Computer Science 93, pages 138-160. February 2004. ISBN 044451290X, Elsevier.
  20. Wells, Plump and Kamareddine, Diagrams for Meaning Preservation, Rewriting Techniques and Applications RTA2003, Lecture Notes in Computer Science 2706, Pages 88{106, Nieuwen-huis, R (Ed.), ISBN 3-540-40254-3, Springer-Verlag, May 2003.
  21. Kamareddine and R os, Explicit Substitutions a la de Bruijn: the local and global way, ICALP'03 satellite workshop on Mathematics, Logic and Computation, July 2003, Eindhoven, NL. Electronic Notes in Theoretical Computer Science 85, 20 pages, ENTCS, Elsevier.
  22. Kamareddine, Laan and Nederpelt, Automath and Pure Type Systems, ICALP'03 satellite workshop on Mathematics, Logic and Computation, July 2003, Eindhoven, NL. Electronic Notes in Theoretical Computer Science 85, 20 pages, ENTCS, Elsevier.
  23. Kamareddine, Monin and Ayala, On automating the extraction of programs from proofs using product types, 9th Workshop on Logic, Language, Information and Computation, WoLLIC 2002 July 30 to August 2, 2002, Rio de Janeiro, Brazil. Electronic Notes in Theoretical Computer Science 67, 20 pages, ENTCS, Elsevier.
  24. Ayala, de Moura and Kamareddine, Comparing Calculi of Explicit Substitutions with Eta-reduction, 9th Workshop on Logic, Language, Information and Computation, WoLLIC 2002 July 30 to August 2, 2002, Rio de Janeiro, Brazil. Electronic Notes in Theoretical Computer Science 67, 20 pages, ENTCS, Elsevier.
  25. Kamareddine, On Functions and Types, Invited talk, 29th Annual Conference on Current Trends in Theory and Practice of Informatics, Lecture Notes in Computer Science 2540, Pages 74-93, Grosky, W. I. and Plasil, F. (Ed.), Springer-Verlag, 2002.
  26. Bloo, Kamareddine, Laan and Nederpelt, Parameters in Pure Type Systems, Latin American Theoretical INformatics Latin 2002, Cancun, Mexico. Lecture Notes in Computer Science 2286, Pages 371-385, Rajsbaum, S., (Ed.), Springer-Verlag, March 2002.
  27. Ayala and Kamareddine, On Applying the  se-Style of Uni cation for Simply-typed Higher Order Uni cation in the pure -calculus. 8th Workshop on Logic, Language, Information and Computation WoLLIC 2001 July 31 to August 3, 2001, Braslia, Brazil.
  28. Nederpelt and Kamareddine, Formalising the natural language of mathematics: A Math-ematical Vernacular. The Fourth International Tbilisi Symposium on Language, Logic and Computation September 23-28, 2001, Borjomi, Georgia.
  29. Borghuis, Kamareddine and Nederpelt, Belief Revision in Type Theory. The Second Asia-Paci c Conference on Intelligent Agent Technology, IAT 2001, Pages 69-73, 2001. World Scien-ti c.
  30. Kamareddine, Bloo and Nederpelt, De Bruijn's syntax and reductional equivalence of lambda terms. International Conference on Principles and Practice of Declarative Programming, PPDP 2001, Florence, Italy. ACM publications 1-58113-388-x/01/09, Pages 16-27, 2001.
  31. Kamareddine and Laan and Nederpelt, Re ning the Barendregt Cube using Parameters. Fifth International Symposium on Functional and Logic Programming, FLOPS 2001, Tokyo, Japan. Lecture Notes in Computer Science 2024, Pages 375{389, Springer-Verlag, 2001.
  32. Ayala-Rincon and Kamareddine, Strategies for Simply-Typed Higher Order Uni cation via lambda se Style of Explicit Substitution. In Third Int'l Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs, A Satellite workshop of RTA 2000, Norwich, UK, 2000.
  33. Ayala-Rincon and Kamareddine, Uni cation via lambda se-Style of Explicit Substitution. International Conference on Principles and Practice of Declarative Programming, PPDP 2000, Montreal, Canada. ACM Publications 1-58113-265-4/00/0009, Pages 163-174, 2000.
  34. Kamareddine and Monin, On Automating Inductive and Non-Inductive Termination Meth-ods, Lecture Notes in Computer Science 1742, Asian Computing Science Conference, ASIAN 1999, Pukhet, Thailand. Pages 177-189, Springer-Verlag, 1999. ISSN: 0302-9743.
  35. Kamareddine and Monin, On Formalised Proofs of Termination of Recursive Functions, Lecture Notes in Computer Science 1702, International Conference on Principles and Practice of Declarative Programming, PPDP 1999, Pages 29-46. Paris, France. Springer-Verlag, 1999.
  36. Kamareddine, Bloo and Nederpelt, An Approximation of Reductional Equivalence, Computer Science Logic, CSL 1997, Aarhus, Copenhagen.
  37. Barthe, Kamareddine and R os, Explicit substitutions for the calculus, Lecture Notes in Computer Science 1298, 6th international joint conference on Algebraic and Logic Programming and Higher Order Algebra, ALP-HOA 1997, Pages 209-223, Southampton, UK. Springer-Verlag, 1997.
  38. Kamareddine and R os, Generalised -reduction and Explicit substitution, Lecture Notes in Computer Science 1140, 8th international symposium on Programming Languages: Implemen-tations, Logics and Programs, PLILP 1996. Aachen, Germany. Pages 378-392, Springer-Verlag, 1996.
  39. Kamareddine and R os, -calculus a la de Bruijn & explicit substitution, Lecture Notes in Computer Science 982, 7th international symposium on Programming Languages: Implemen-tations, Logics and Programs, PLILP 1995, Pages 45-62, the Netherlands. Springer-Verlag, 1995.
  40. Kamareddine, Are types needed for Natural Language?, proceedings of the Applied Logic conference Logic at Work, 28 pages, December 17-19, Amsterdam, 1992.
  41. Kamareddine and Nederpelt, A uni ed approach to type theory through a re ned -calculus, Mathematical Foundations of Programming Semantics, Oxford, 1992.
  42. Kamareddine, Internal de nability and collection, proceedings of the conference on genericity in Natural Language, edited by Krifka, SNS, T•ubingen, Pages 199-219, 1988.

EDITORIALS

  1. Adel Bouhoula, Tetsuo Ida and Fairouz Kamareddine (2013). Preface. EPTCS ??
  2. Mauricio Ayala-Rincon, Elaine Pimentel and Fairouz Kamareddine (2011). Preface. The-oretical Computer Science 412(37): 4851-4852.
  3. Mauricio Ayala Rincon and Kamareddine (2009), Preface. Electr. Notes Theor. Comput. Sci. 256: 1-3.
  4. Kamareddine (2004), Editorial for the Special Issue on Variants of logics: from HOL to the calculus of constructions to teaching mathematical proofs on computers. Journal of Applied Logic. Volume 2, issue 2, Pages 169{172. June 2004. ISSN 1570-8683. Elsevier, North-Holland.
  5. Kamareddine (2004), Editorial for the Special Issue on Mathematical Knowledge Management Symposium. Electronic Notes in Theoretical Computer Science 93. Pages 1{4, February 2004. ISBN 044451290X, Elsevier.
  6. Geuvers and Kamareddine (2003), Editorial for the Special Issue on Mathematics, Logic and Computation (MLC), Electronic Notes in Theoretical Computer Science 85(7). 2003. ISBN 044451290X, Elsevier.
  7. Kamareddine (2003), Editorial for Thirty Five Years of Automating Mathematics. Edited book in the Kluwer Applied Logic series. Volume 28. Pages 1{8, November 2003. ISBN 1-4020-1656-5. Kluwer Academic Publishers.
  8. Kamareddine (2002), Editorial for the Special Issue on Mechanising and Automating Math-ematics: In honour of N.G. de Bruijn. Journal of Automated Reasoning. Volume 29, issues 3 and 4, Pages 183{188. 2002. ISSN 0168 7433. Kluwer Academic Publishers.
  9. Kamareddine (2001), Editorial for the Special issue on rewriting and theorem proving. Jour-nal of the Interest group of Pure and Applied Logic, 9(3), Pages 335{337, 2001, ISSN 1367-0751, Oxford University Press.
  10. Kamareddine (2001), Editorial for the Special issue on Type and set theoretical foundation of computation. Journal of Logic and Computation volume 11 (3), Pages 359{361, 2001, ISSN 0955 792X, Oxford University Press.
  11. Kamareddine and Klop (2000), Editorial for the Special issue on Type Theory and Term Rewriting. Journal of Logic and Computation volume 10 (3), Pages 321{322, 2000, ISSN 0955 792X, Oxford University Press.

 

Autoimmune Journal Flyer