Selected Publications by Fairouz Kamareddine

Fairouz
Kamareddine

Selected Publications by Fairouz Kamareddine
(see also American Mathematical Society Page and DBLP, Google Scholar and Research Gate)

IN PREPARATION

Fairouz Kamareddine and J.B. Wells (2017), Obtaining Intersection Types via Finite Set Declarations in the Pure Type System Cube

BOOKS/EDITED BOOKS

Fairouz Kamareddine and Jonathan Seldin. A Primer of Mathematical Analysis and the Foundations of Computation, Studies in Mathematics 8, College Publications, October 2023. Paperback 436 pages. ISBN 978-1-84890-443-9. Here are more details. Here you find the solutions to the exercises. These solutions are also accessible here. Here is the Amazon page.
Fairouz Kamareddine, A Century since Principia's Substitution Bedazzled Haskell Curry. In Honour of Jonathan Seldin's 80th Anniversary, College Publications (11 July 2023), Paperback 282 pages, ISSN-10 1848904363, ISBN 13 978-1848904361. Here is the list of contents
Fairouz Kamareddine, Claudio Sacerdoti Coen: Intelligent Computer Mathematics - 14th International Conference, CICM 2021, Timisoara, Romania, July 26-31, 2021, Proceedings. Lecture Notes in Computer Science 12833, Springer 2021, ISBN 978-3-030-81096-2
Bajwa, Imran Sarwar, Fairouz Kamareddine, Costa, Anna (Eds.) (2019) Intelligent Technologies and Applications, First International Conference, International Conference on Intelligent Technologies and Applications, INTAP 2018, Bahawalpur, Pakistan, October 23-25, 2018, Revised Selected Papers. 1st ed. 2019, XVIII, 853 pages. ISBN 978-981-13-6051-0
Fairouz Kamareddine, Jonathan P. Seldin (2016) Foundations of Combinatory Logic, by H.B.Curry: Translation into English. Haskell Curry, 1930, University of Goettingen, Grundlagen der kombinatorischen Logik (Foundations of Combinatory logic), PhD advisor: David Hilbert. College Publications. ISBN 978-1-84890-202-2. Front-Matter and Cover Page. Here is Amazon's page
Fairouz Kamareddine, Twan Laan and Rob Nederpelt (2004)
A Modern Perspective on Type Theory From its Origins Until Today.
Springer Academic Publishers, Applied Logic Series, Volume 29. 357 pages. May 2004. ISBN 1-4020-2334-0.
Here is a review of Henk Barendregt about it. Here is a review by Vladik Kreinovich about it. Here is the springer pointer to it.
Rob Nederpelt and Fairouz Kamareddine (2004)
Logical Reasoning: A first course.
College publications, Texts in Computing, Volume 3, 400 pages. April 2004. ISBN 0-9543006-7-X.
Here is the amazon pointer to it.
Here is college publications pointer to it.
Fairouz Kamareddine, editor (2003)
Thirty Five Years of Automating Mathematics.
Edited book in the Applied Logic series. Volume 28. 328 pages. Springer. November 2003. ISBN 1-4020-1656-5.
Here is the amazon pointer to it.
Here is the editorial in ps. Here is the editorial in pdf.
Here is a summary.

JOURNAL PAPERS

Fairouz Kamareddine and Jonathan Seldin (2022),
Using the History of Mathematics to Teach the Foundations of Mathematical Analysis: Second Paper, in "Research in History and Philosophy of Mathematics: The CSHPM 2019-2020 Volume", edited by Maria Zack and Dirk Schlimm, published by Birkhaeuser, pages 199-215.
Vincent Rahli, J.B. Wells, John Pirie, and Fairouz Kamareddine (2017)
Skalpel: A Constraint-Based Type Error Slicer for Standard ML Journal of Symbolic Computation 80. 164-208.
Fairouz Kamareddine, Jonathan P. Seldin and J.B. Wells (2016)
Bridging Curry and Church's typing style. Journal of Applied Logic 18, pages 42-70, November 2016. Elsevier, North Holland. DOI information: 10.1016/j.jal.2016.05.008
Here is a link to article on elsevier.
Daniel Lima Ventura, Fairouz Kamareddine, and Mauricio Ayala-Rincon (2015)
Explicit substitutions calculi with de Bruijn indices and intersection type systems .
the Logic Journal of the Interest Group of Pure and Applied Logic Volume 23, issue 2, Pages 295-340, 2015. ISSN 1367-0751, Oxford University Press.
Fairouz Kamareddine, Karim Nour, Vincent Rahli and J.B. Wells (2012)
On Realisability Semantics for Intersection Types with Expansion Variables .
For the extended version with proofs, click here. Fundamenta Informatica 121(1-4): 153-184 (2012).
Fairouz Kamareddine, Vincent Rahli and J.B. Wells (2012)
Reducibility proofs in the lambda calculus .
For the extended version with proofs, click here. Fundamenta Informatica 121(1-4): 121-152 (2012)
Daniel Lima Ventura, Mauricio Ayala-Rincón and Fairouz Kamareddine (2009)
Explicit substitutions calculi with one step Eta-reduction decided explicitly.
the Logic Journal of the Interest Group of Pure and Applied Logic Volume 17, issue 6, Pages 697-718, 2009. ISSN 1367-0751, Oxford University Press.
Flavio de Moura, Mauricio Ayala-Rincón and Fairouz Kamareddine (2008)
Higher Order Unification: A structural relation between Huet's method and the one based on explicit substitutions
The journal of Applied Logic, Volume 6, Issue 1, Pages 72-108, Elsevier, North-Holland. ISSN 1570-8683. March 2008.
Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel and Joe Wells (2007)
Digitised Mathematics: Computerisation vs. Formalisation. Review of the National Center for Digitization, Volume 10, pages 1-8, Faculty of Mathematics, Belgrade, Serbia, 2007.
Fairouz Kamareddine and Karim Nour (2007)
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.
Ariel Arbiser, Fairouz Kamareddine and Alejandro Rios (2007)
The Weak Normalisation of the simply typed $\lambda s_e$-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.
Flavio de Moura, Mauricio Ayala-Rincón and Fairouz Kamareddine (2006)
SUBSEXPL: A Tool for Simulating and Comparing Explicit Substitutions Calculi.
Journal of Applied Non-classical Logics Volume 16, issue 1-2, Pages 119-150, 2006. E'ditions Herm`es-Lavoisier.
Fairouz Kamareddine (2005)
Typed lambda calculi with unified binders .
Journal of Functional Programming Volume 15, no. (5), pages 771-796, September 2005, ISSN: 0956-7968. Cambridge University Press.
Mauricio Ayala-Rincón Flavio de Moura and Fairouz Kamareddine (2005)
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.
Fairouz Kamareddine and Roel Bloo (2005)
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.
Fairouz Kamareddine and Roel Bloo (2005)
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.
Fairouz Kamareddine and Rob Nederpelt (2004)
A refinement of de Bruijn's formal language of mathematics. Here is the pdf version.
Journal of Logic, Language and Information Volume 13, issue 3, pages 287-340, June 2004, Kluwer Academic Publishers. ISSN 0925-8531.
Fairouz Kamareddine, François Monin and Mauricio Ayala-Rincón, (2003)
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. December 2003. ISSN 1657 2831.
Mauricio Ayala-Rincón and Fairouz Kamareddine (2003)
On Applying the lambda se-style of unification for simply-typed higher order unification in the pure lambda calculus.
Mathematica Contemporanea. Volume 24, Pages 1-22. July 2003. Sociedade Brasileira de Matemática. INSS 0103-9059.
Fairouz Kamareddine and Haiyan Qiao (2003)
Formalising strong normalisation proofs of explicit substitution calculi in ALF.
Automated Reasoning. Volume 30, issues 1, Pages 59-98. January 2003. Kluwer Academic Publishers. ISSN 0168-7433.
Fairouz Kamareddine, Twan Laan and Rob Nederpelt (2003)
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.
Tijn Borghuis, Fairouz Kamareddine and Rob Nederpelt (2002)
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. Here is the pdf file.
Fairouz Kamareddine, Twan Laan and Rob Nederpelt (2002)
Types in logic and mathematics before 1940. Here is the journal unprintable version. Here is the pdf version.
The Bulletin of Symbolic Logic, Volume 8, issue 2, Pages 185-245, June 2002, Association for Symbolic Logic .
Fairouz Kamareddine and Alejandro Ríos (2002)
Pure Type Systems with de Bruijn indices
The Computer Journal, Volume 45(2), pages 187-201, March 2002. Copyright ©British Computer Society 2002. ISSN: 0010-4620. Oxford University Press.
Fairouz Kamareddine and François Monin (2002)
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-Scientific Publishing Company.
Mauricio Ayala-Rincón and Fairouz Kamareddine (2001)
Unification via lambda-s_e-Style of Explicit Substitution
the Logic Journal of the Interest Group of Pure and Applied Logic Volume 9(4), pages 521-555, July 2001, ISSN 0945-9103, Oxford University Press.
Fairouz Kamareddine (2001),
Reviewing the classical and the de Bruijn notation for $\lambda$-calculus and pure type systems
Logic and Computation volume 11 (3), pages 363-394, ISSN: 0955-792X, June 2001, Oxford University Press.
Fairouz Kamareddine and Twan Laan (2001),
A Correspondence between Martin-Loef Type Theory, the Ramified Theory of Types and Pure Type Systems .
Logic, Language and Information Volume 10(3), pages 375-402, Summer 2001, Kluwer Academic Publishers. ISSN 0925-8531.
Fairouz Kamareddine and Alejandro Ríos (2000)
Relating the Lambda-sigma and Lambda-s styles of Explicit Substitutions
Special issue on Type Theory and Term Rewriting.
Special issue in the Journal of Logic and Computation volume 10 (3), pages 349-380, ISSN: 0955-792X, June 2000, Oxford University Press.
Fairouz Kamareddine (2000)
Postponement, Conservation and Preservation of Strong Normalisation for Generalised Reduction
Logic and Computation volume 10 (5), pages 721-738, ISSN: 0955-792X, October 2000, Oxford University Press.
Fairouz Kamareddine, Roel Bloo and Rob Nederpelt (1999)
On $\Pi$-conversion in The $lambda$-cube and the combination with abbreviations
Annal of Pure and Applied Logics volume 97, no. 1-3, pages 27-45, 1999, Elsevier, North-Holland. ISSN: 0168-0072.
Fairouz Kamareddine, Alejandro Ríos and Joe Wells (1998)
Calculi of Generalised $\beta$-Reduction and Explicit Substitutions: The Type free and Simply Typed Versions Journal of Functional and Logic Programming, Volume 1998, article 5, pages 1-44, ISSN 1080-5230, MIT Press, 4 June 1998.
Fairouz Kamareddine and Alejandro Ríos (1998)
Bridging de Bruijn indices and variable names in explicit substitutions calculi
the Logic Journal of the Interest Group of Pure and Applied Logic no. 6(6), pages 843-874, 1998, ISSN 0945-9103, Oxford University Press.
Fairouz Kamareddine (1998)
The Soundness of Explicit Substitution with Nameless Variables
International Journal of Foundations of Computer Science 9(3), pages 321-349, 1998, ISSN 0129-0541. World-Scientific Publishing Company.
Fairouz Kamareddine and Alejandro Ríos (1997)
Extending a $\lambda$-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
Journal of Functional Programming volume 7, no. (4), pages 395-420, 1997, ISSN: 0956-7968. Cambridge University Press.
Fairouz Kamareddine and Rob Nederpelt (1996)
Canonical Typing and $\pi$-conversion in the Barendregt Cube
Journal of Functional Programming volume 6, no. (2), pages 245-267, 1996, ISSN: 0956-7968. Cambridge University Press.
Fairouz Kamareddine and Rob Nederpelt (1996)
A useful $\lambda$-notation
Theoretical Computer Science volume 155, No. 1, pages 85-109, 1996, ISBN 044451290X, Elsevier, North-Holland.
Fairouz Kamareddine and Twan Laan (1996)
A reflection on Russell's Ramified Types and Kripke's Hierarchy of Truths
The Logic Journal of the Interest Group of Pure and applied Logic volume 4, No. 2, pages 195-213, 1996, ISSN 0945-9103, Oxford University Press.
Roel Bloo, Fairouz Kamareddine and Rob Nederpelt (1996)
The Barendregt Cube with definitions and generalised reduction
Information and Computation, volume 126. No 2, pages 123-143, 1996, ISSN: 0890-5401, Academic Press.
Fairouz Kamareddine (1995)
A type free theory and collective/distributive predication
Logic, Language and Information volume 4 no. 2, pages 85-109, 1995, Kluwer Academic Publishers. ISSN 0925-8531.
Fairouz Kamareddine (1995)
Important Issues in Foundational Formalisms
The Logic Journal of the Interest Group of Pure and applied Logic, volume 3, no. 2-3, pages 291-317, 1995, ISSN 0945-9103, now Oxford University Press.
Fairouz Kamareddine and Rob Nederpelt (1995)
Refining reduction in the lambda-calculus
Journal of Functional Programming volume 5, no. 4, pages 637-651, 1995, ISSN: 0956-7968. Cambridge University Press.
Fairouz Kamareddine and Rob Nederpelt (1994)
A unified approach to type theory through a refined lambda-calculus
Selected papers of the Meeting on the Mathematical Foundations of Programming Semantics (MFPS '92), Part II (Oxford, 1992).
Theoretical Computer Science volume 136, no. 1, pages 183-216, 1994, ISBN 044451290X, Elsevier, North-Holland.
Fairouz Kamareddine and Ewan Klein (1993)
Polymorphism, Type containment and Nominalization
Logic, Language and Information volume 2, no. 3, pages 171-215, 1993, Kluwer Academic Publishers. ISSN 0925-8531.
Fairouz Kamareddine and Rob Nederpelt (1993)
On stepwise explicit substitution
International Journal of Foundations of Computer Science volume 4, no. 3, pages 197-240, 1993, ISSN: 0129-0541. World-Scientific Publishing Company.
Fairouz Kamareddine (1992)
$\lambda$-terms, logic, determiners and quantifiers
Logic, Language and Information volume 1, no. 1, pages 79-103, 1992, Kluwer Academic Publishers. Pages 79-103, 1992. ISSN 0925-8531.
Fairouz Kamareddine (1992)
Set Theory and Nominalisation I
Logic and Computation volume 2, no. 5, pages 579-604, 1992, ISSN: 0955-792X, Oxford University Press.
Fairouz Kamareddine (1992)
Set Theory and Nominalisation II
Logic and Computation volume 2, no. 6, pages 687-707, 1992, ISSN: 0955-792X, Oxford University Press.
Fairouz Kamareddine (1992)
A system at the cross roads of logic and functional programming
Science of Computer Programming volume 19(3), pages 239-279, 1992, ISSN: 0167-6423, Elsevier, North-Holland.

ARTICLES IN EDITED BOOKS

Fairouz Kamareddine (2023), Substitution in the lambda Calculus and the role of the Curry School. In Kamareddine editor: A Century since Principia's Substitution Bedazzled Haskell Curry. In Honour of Jonathan Seldin's 80th Anniversary. College Publications (11 July 2023), Paperback 282 pages, ISSN-10 1848904363, ISBN 13 978-1848904361. Here is the list of contents
Fairouz Kamareddine, Joe Wells, Christoph Zengler and Henk Barendregt (2014)
Computerising Mathematical Text In Joerg Siekmann, Dov. M Gabbay and John Woods, editors: Vol. 11 Logic and Computation in the 20th century HHL, : San Diego: North Holland, 2014, pp. 87-140. Here is the extended version for the MathLang part only, with the full encoding and formalisation into Coq of Landau's first chapter.
Fairouz Kamareddine, Twan Laan and Rob Nederpelt (2012)
A history of types. In Dov. M Gabbay, Francis Jeffry Pelletier and John Woods, editors: Logic: A History of its Central Concepts. 11, HHL, : San Diego: North Holland, 2012, pp. 451-511.
Fairouz Kamareddine, Twan Laan and Robert Constable (2012)
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, 6, HHL, : San Diego: North Holland, 2012, pp. 801-845.
Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel and Joe Wells (2007)
Gradual Computerisation/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 Association for Logic and Philosophy of Science, 2007. bibtex
Fairouz Kamareddine, Twan Laan and Rob Nederpelt (2003)
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. Kluwer Academic Publishers. November 2003. ISBN 1-4020-1656-5.
Fairouz Kamareddine (1995)
Are types needed for Natural Language?
inApplied Logic: What and Why, edited by L\'{a}szlo P\'{o}los and Michael Masuch, Kluwer Academic Publishers, pages 79-120, 1995. ISBN 0-7923-3095-1.

EDITED VOLUMES

I.S. Bajwa, Fairouz Kamareddine and P. Thangarajah editors. Intelligent Computing for Society. Journal of Universal Computer Science, 25(10). Pages 1219--1393. 2019.
Adel Bouhoula, Tetsuo Ida and Fairouz Kamareddine editors. Proceedings Fourth International Symposium on Symbolic Computation in Software Science, SCSS 2013, Gammarth, Tunisia, 15-17 December 2012. EPTCS 122, 2013
Mauricio Ayala-Rincon, Elaine Pimentel and Fairouz Kamareddine: Proceedings of LSFA 2008 and LSFA 2009. Theoretical Computer Science 412(37), 151 pages. (2011)
Mauricio Ayala-Rincon and Fairouz Kamareddine: Proceedings of the Fourth Workshop on Logical and Semantic Frameworks with Applications LSFA'09. Electr. Notes Theor. Comput. Sci. 256: 135 pages. (2009)
Fairouz Kamareddine, editor (2004)
Special Issue on Variants of logics: from HOL to the calculus of constructions to teaching mathematical proofs on computers.
Special issue in The journal of Applied Logic, Volume 2, issue 2, Pages 169-239, Elsevier, North-Holland. ISSN 1570-8683. June 2004.
Fairouz Kamareddine, editor (2004)
Mathematical Knowledge Management Symposium 2003, Electronic Notes in Theoretical Computer Science 93C, Mathematical Knowledge Management Symposium 2003. Pages 1-201. ENTCS, ISBN 044451290X, February 2004. Elsevier.
Fairouz Kamareddine, editor (2003)
Thirty Five Years of Automating Mathematics.
Edited book in the Kluwer Applied Logic series, volume 28. Kluwer Academic Publishers. November 2003. Volume 28. 328 pages. ISBN 1-4020-1656-5.
Here is the amazon pointer to it.
Here is the editorial in ps. Here is the editorial in pdf.
Here is a summary.
Here is the Kluwer information about it.
Herman Geuvers and Fairouz Kamareddine, editors (2003)
Mathematics, Logic and Computation, Electronic Notes in Theoretical Computer Science 85(7), Mathematics, Logic and Computation 2003. ENTCS.
Fairouz Kamareddine, editor (2002)
Special Issue Mechanizing and Automating Mathematics: In honour of N.G. de Bruijn.
Here is the editorial in ps. Here is the editorial in pdf.
Special issue in the Journal of Automated Reasoning. Volume 29, issues 3 and 4, Pages 183-418. 2002. Kluwer Academic Publishers. ISSN 0168-7433.
Fairouz Kamareddine, editor (2001)
Special issue on type and set theoretical foundations of Computation.
Special issue in the Journal of Logic and Computation volume 11 (3), Pages 359-498, ISSN: 0955-792X, June 2001, Oxford University Press.
Fairouz Kamareddine, editor (2001)
Special issue on rewriting and theorem proving.
Special issue in the Logic Journal of the Interest Group of Pure and Applied Logic no. 9(3), Pages 329-488, 2001, ISSN 0945-9103, Oxford University Press.
Here is the editorial in pdf.
Fairouz Kamareddine and Jan Willem Klop, editors (2000)
Special issue on Type Theory and Term Rewriting.
Special issue in the Journal of Logic and Computation volume 10 (3), Pages 321-492, ISSN: 0955-792X, June 2000, Oxford University Press.
Here is the editorial in pdf.

REFEREED CONFERENCE PAPERS

Fairouz Kamareddine, Joe B. Wells, Intersection Types via Finite-Set Declarations. WoLLIC 2024, Lecture Notes in Computer Science 14672. Pages 80-92, Springer 2024, Doi: 10.1007/978-3-031-62687-6\_6
Luka Vrecar, Joe B. Wells, Fairouz Kamareddine, Towards Semantic Markup of Mathematical Documents via User Interaction. CICM 2024: Pages 223-240, Lecture Notes in Computer Science 14960, Springer 2024, Doi: 10.1007/978-3-031-66997-2\_13.
Fairouz Kamareddine and Jonathan Seldin (2024),
The paradoxes and the infinite dazzled ancient mathematics and continue to do so today. The 25th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing SYNASC 2023, IEEE 2024. Doi: 10.1109/SYNASC61333.2023.00058
Ciaran Dunne, Joe B. Wells, Fairouz Kamareddine, Generating Custom Set Theories with Non-set Structured Objects. . CICM 2021: Pages 228-244, Lecture Notes in Computer Science 12833, Springer 2021, ISBN 978-3-030-81096-2
Hua Zhao, Fairouz Kamareddine, Alasdair J. G. Gray, Hind Zantout, A Novel Method That Identifies The Hidden Properties Of A Person's Name In Kanji Or Hanzi. MISNC 2021: 79-85.
Ciaran Dunne, Joe B. Wells, Fairouz Kamareddine, Adding an Abstraction Barrier to ZF Set Theory . CICM 2020: Pages 89-104, Lecture Notes in AI 12236, Springer 2020, DOI: https://doi.org/10.1007/978-3-030-53518-6_6
Dee Quinlan, Joe B. Wells, Fairouz Kamareddine, BNF-Style Notation as It Is Actually Used. CICM 2019: Pages187-204, Lecture Notes in Computer Science 11617, Springer 2019, ISBN 978-3-030-23249-8.
Hua Zhao, Fairouz Kamareddine, A Novel Phonetic Algorithm for Predicting Chinese Names using Chinese Pin Yin. Machine Learning and Data Mining in Pattern Recognition}, 15th International Conference on Machine Learning and Data Mining, MLDM 2019. New York, NY, USA, July 20-25, 2019, Proceedings, Volume I. Pages 78-92. ibai publishing 2019, ISBN 978-3-942952-62-0, 2019.
Hua Zhao, Fairouz Kamareddine, A Decision Tree Method on Fuzzy Name Identification from Chinese phonemic names to Chinese names. In 5th Annual Conf. on Computational Science \& Computational Intelligence (CSCI 2018), Las Vegas, USA. IEEE Computer Society ISBN-13: 978-1-7281-1360-9; DOI 10.1109/CSCI.2018. Paper Acceptance Rate: 19\%. 2018.
Hua Zhao and Fairouz Kamareddine, Hua Zhao, Fairouz Kamareddine, Recursion identify algorithm for Gender Prediction with Chinese names. In CSCE'18 - The 2018 World Congress in Computer Science, Computer Engineering, \& Applied Computing, Las Vegas, USA. 2018. ISBN: 1-60132-481-2 | Copyright © 2018 CSREA Press | United States of America.
Hua Zhao and Fairouz Kamareddine, Advance gender prediction tool of first names and its use in analying gender disparity in Computer Science in the UK, Malaysia and China. In 4th Annual Conf. on Computational Science \& Computational Intelligence (CSCI 2017), Las Vegas, USA. IEEE Computer Society ISBN-13: 978-1-5386-2652-8; DOI 10.1109/CSCI.2017.313. Paper Acceptance Rate: 21\% 2017.
David Feller, Fairouz Kamareddine and Lavinia Burski (2016) Using MathLang to Check the Correctness of Specifications in Object-Z. In Modern Mathematical Methods and High Performance Computing in Science and Technology: M3HPCST, Ghaziabad, India, December 2015, Editors Ezio Venturino, Hari Mohan Srivastava, Michael Resch, Vijay Gupta and V.K. Singh. Springer Proceedings in Mathematics and Statistics.
Fairouz Kamareddine, J.B. Wells and Daniel Lima Ventura, (2015) Automath type inclusion in Barendregt's Cube, Computer Science - Theory and Applications - 10th International Computer Science Symposium in Russia,
CSR 2015, LNCS 9139, Pages 262-282, Listvyanka, Russia, July 13-17, 2015. ISBN 978-3-319-20296-9
Daniel Lima Ventura, Mauricio Ayala-Rincón and Fairouz Kamareddine (2010)
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
Robert Lamar, Fairouz Kamareddine, and Joe Wells (2009)
MathLang Translation to Isabelle Syntax, 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.
Fairouz Kamareddine, Karim Nour, Vincent Rahli and J.B. Wells (2008)
A complete realisability semantics for intersection types and infinite expansion variables. ( slides-of-talk.pdf)
For the extended version with proofs, click here.
In 5th International Colloquium 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.
Daniel Lima Ventura, Mauricio Ayala-Rincón and Fairouz Kamareddine (2008)
Principal Typings for Explicit Substitutions calculi , (slides of talk)
Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Loewe (eds.): Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008, Athens, Greece, June 2008, Proceedings, Lecture Notes in Computer Science volume 5028, pages 567-578. ©Springer-Verlag.
Computability in Europe 2008 Logic and Theory of Algorithms, 15-20 June 2008, Athens, Greece.
Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel and Joe Wells (2007)
Narrative Structure of Mathematical Texts
Sixth International Conference on MATHEMATICAL KNOWLEDGE MANAGEMENT, 27-30 June, 2007, Linz, Austria. 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.
Here are the slides of the talk my PhD student Krzysztof Retel gave.
Fairouz Kamareddine, Robert Lamar, Manuel Maarek and Joe Wells (2007)
Restoring Natural Language as a Computerised Mathematics Input Method, the example supplement can be found here
Sixth International Conference on MATHEMATICAL KNOWLEDGE MANAGEMENT, 27-30 June, 2007, Linz, Austria. 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.
Here are the slides of the talk my PhD student Robert Lamar gave.
Fairouz Kamareddine, Manuel Maarek and Joe Wells (2006)
Toward an Object-Oriented Structure for Mathematical Text
Mathematical Knowledge Management, Third International Conference, MKM 2005, Lecture Notes in AI 3863, Pages 217-233, Michael Kohlhase (Ed), ISBN 3-540-31430-X. ©Springer-Verlag, September 2006.
Here are the slides of the talk my PhD student Manuel Maarek gave.
Here are some pictures of Manuel at his PhD graduation in 2007.
Flavio de Moura, Fairouz Kamareddine, and Mauricio Ayala-Rincón, (2005)
Second-Order Matching via Explicit Substitutions. Version pdf
Logic for Programming, Artificial Intelligence, and Reasoning: 11th International Conference, LPAR 2004, 14-18 March 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.
Fairouz Kamareddine, Manuel Maarek and Joe Wells (2004)
Flexible Encoding of Mathematics on the Computer
Mathematical 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.
Here are the slides of the talk my PhD student Manuel Maarek gave.
Joe Wells, Detlef Plump and Fairouz Kamareddine, (2003)
Diagrams for Meaning Preservation
14th International Conference on Rewriting Techniques and Applications, RTA2003, Valencia, Spain.
Lecture Notes in Computer Science 2706, Pages 88-106, Nieuwenhuis, R (Ed.), ISBN 3-540-40254-3, ©Springer-Verlag, June 2003.
Here are slides of the talk of Joe Wells.
Roel Bloo, Fairouz Kamareddine, Twan Laan and Rob Nederpelt (2002)
Parameters in Pure Type Systems
Latin American Theoretical INformatics Latin 2002, Cancun, Mexico, April 3-6 2002.
Lecture Notes in Computer Science 2286, Pages 371-385, Rajsbaum, S., (Ed.), ISBN 3-540-43400-3, ©Springer-Verlag, March 2002.
Here are the slides of the talk that I jointly presented with my co-author Roel Bloo.
Fairouz Kamareddine (2002)
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.), ISBN 3-540-00145-X, ©Springer-Verlag, Milovy, Czech Republic, 22-29 November 2002.
Here are the slides.pdf and slides.pdf of the invited talk I gave.
Fairouz Kamareddine, Roel Bloo and Rob Nederpelt (2001)
De Bruijn's syntax and reductional equivalence of lambda terms
International Conference on Principles and Practice of Declarative Programming, PPDP'01,
ACM publications 1-58113-388-x/01/09, Pages 16-27, 2001.
Here are the slides of the talk I gave.
Fairouz Kamareddine, Twan Laan and Rob Nederpelt (2001)
Refining the Barendregt Cube using Parameters
Fifth International Symposium on Functional and Logic Programming, FLOPS 2001,
Lecture Notes in Computer Science 2024, Pages 375-389, ©Springer-Verlag, 2001. ISSN 0302-9743.
Here are the slides of the talk I gave.
Tijn Borghuis, Fairouz Kamareddine and Rob Nederpelt (2001)
Belief Revision in Type Theory
The Second Asia-Pacific Conference on Intelligent Agent Technology, IAT'01, Pages 69-73, 2001.
World Scientific ISBN 981-02-4706-0.
Here are the slides of the talk I gave.
Mauricio Ayala-Rincón and Fairouz Kamareddine (2000)
Unification via lambda se-Style of Explicit Substitution
International Conference on Principles and Practice of Declarative Programming, PPDP'00,
ACM publications 1-58113-265-4/00/0009, Pages 163-174, 2000.
Here are the slides of the talk given by co-author Mauricio Ayala-Rincón.
Fairouz Kamareddine and François Monin (1999)
On Automating Inductive and Non-Inductive Termination Methods
Asian Computing Science Conference, ASIAN'99,
Lecture Notes in Computer Science 1742, Pages 177-189, ©Springer-Verlag, 1999. ISSN: 0302-9743.
Fairouz Kamareddine and François Monin (1999)
On Formalised Proofs of Termination of Recursive Functions
International Conference on Principles and Practice of PPDP'99,
Lecture Notes in Computer Science 1702, Pages 29-46, ©Springer-Verlag, 1999.
Fairouz Kamareddine, Roel Bloo and Rob Nederpelt (1997)
An Approximation of Reductional Equivalence
Computer Science Logic, CSL'97, Aarhus.
Gilles Barthe, Fairouz Kamareddine and Alejandro Ríos (1997)
Explicit substitutions for the $\lambda \Delta$ calculus Proceedings of the 6th international joint conference on Algebraic and Logic Programming (ALP'97) and the 3rd International Workshop on Higher-order Algebra, Logic and Term Rewriting (HOA'97), ALP-HOA'97.
Edited by Michael Hanus, Jan Heering and Karl Meinke. Lecture Notes in Computer Science 1298, Pages 209-223, ©Springer-Verlag, Southampton, 1997.
Fairouz Kamareddine and Alejandro Ríos (1996)
Generalised $\beta$-reduction and Explicit substitution
8th international symposium on Programming Languages: Implementations, Logics and Programs, PLILP '96,
Lecture Notes in Computer Science 1140, Pages 378-392, ©Springer-Verlag, 1996.
Fairouz Kamareddine and Alejandro Ríos (1995)
$\lambda$-calculus \`{a} la de Bruijn \& explicit substitution,
7th international symposium on Programming Languages: Implementations, Logics and Programs, PLILP '95,
Lecture Notes in Computer Science 982, Pages 45-62, ©Springer-Verlag, 1995.
Fairouz Kamareddine (1992)
Are types needed for Natural Language?
proceedings of the Applied Logic conference Logic at Work, 28 pages, December 17-19, Amsterdam, 1992.
Fairouz Kamareddine and Rob Nederpelt (1992)
A unified approach to type theory through a refined $\lambda$-calculus
Mathematical Foundations of Programming Semantics, Oxford, 1992.

EDITORIALS

Adel Bouhoula, Tetsuo Ida and Fairouz Kamareddine: Preface. Proceedings Fourth International Symposium on Symbolic Computation in Software Science, SCSS 2013, Gammarth, Tunisia, 15-17 December 2012. EPTCS 122, 2013
Mauricio Ayala-Rincon, Elaine Pimentel and Fairouz Kamareddine: Preface. Theoretical Computer Science 412(37): 4851-4852 (2011)
Mauricio Ayala-Rincon and Fairouz Kamareddine: Preface. Electr. Notes Theor. Comput. Sci. 256: 1-3 (2009)
Fairouz Kamareddine (2004)
Editorial on Special Issue on Variants of logics: from HOL to the calculus of constructions to teaching mathematical proofs on computers.
Special issue in The journal of Applied Logic, volume 2, issue , pages 169-172, Elsevier, North-Holland. ISSN 1570-8683. June 2004.
Fairouz Kamareddine (2004)
Editorial on the Mathematical Knowledge Management Symposium. Electronic Notes in Theoretical Computer Science 93C, pages 1-4. Mathematical Knowledge Management Symposium 2003. ENTCS, ISBN 044451290X, February 2004. Elsevier.
Herman Geuvers and Fairouz Kamareddine (2003)
Editorial on Mathematics, Logic and Computation. Electronic Notes in Theoretical Computer Science 85(7), Mathematics, Logic and Computation 2003. ENTCS, ISBN 044451290X, Elsevier. Here is the editorial and table of contents in html courtesy of ENTCS.
Fairouz Kamareddine (2003)
Editorial Preface on Thirty Five Years of Automating Mathematics.
Edited book in the Kluwer Applied Logic series. Volume 28. Pages 1-8. Kluwer Academic Publishers. November 2003. ISBN 1-4020-1656-5.
Here is the editorial in ps. Here is the editorial in pdf.
Fairouz Kamareddine (2002)
Editorial on Special Issue Mechanizing and Automating Mathematics: In honour of N.G. de Bruijn.
Special issue in the Journal of Automated Reasoning. Volume 29, issues 3 and 4, Pages 183-188, 2002. Kluwer Academic Publishers. ISSN 0168-7433.
Here is the editorial in ps. Here is the editorial in pdf.
Fairouz Kamareddine (2001)
Editorial on Special issue on type and set theoretical foundation of Computation
Special issue in the Journal of Logic and Computation volume 11 (3), Pages 359-361, ISSN: 0955-792X, June 2001, Oxford University Press.
Fairouz Kamareddine (2001)
Editorial on Special issue on rewriting and theorem proving.
Special issue in the Logic Journal of the Interest Group of Pure and Applied Logic No 9(3). Pages 335-337, 2001, ISSN 0945-9103, Oxford University Press.
Here is the editorial in pdf.
Fairouz Kamareddine and Jan Willem Klop (2000)
Editorial on Special issue on Type Theory and Term Rewriting.
Special issue in the Journal of Logic and Computation volume 10 (3), Pages 321-322, ISSN: 0955-792X, June 2000, Oxford University Press.
Here is the editorial in pdf.

AMS REVIEWS (of books and journal articles)

See here for reviews (of books and journal articles) I have written to the American Mathematical Society.

BOOK REVIEWS (NOT FOR AMS)

Fairouz Kamareddine (2008)
A review of Giuseppe Primiero, Information and Knowledge: A Constructive Type-Theoretical Approach. Logic, Epistemology, And The Unity Of Science 10, Springer. ISBN 978-1-4020-6169-1. History of Philosophy and Logic, 2008.
Fairouz Kamareddine (2007)
A review of Paul Gilmore, Logicism Renewed: Logical Foundations for Mathematics and Computer Science. Lecture Notes in Logic, ASL. 2005. History of Philosophy and Logic, 2007.
Fairouz Kamareddine (1990)
A review of K. Blaesius and H. Buerckert, Deduction system in Artificial intelligence, Chichester: Ellis Horwood, 1989. Journal of Expert systems for Information management, 3 (3), 235-239, 1990.

ABSTRACTS

Fairouz Kamareddine (1996)
Types in Natural Language 1 page abstract appears in Zentralblatt fuer Mathematik.
Fairouz Kamareddine (1992)
Themes in the lambda calculus
Abstracts of the 1992 European Summer Meeting of the ASL (Association of Symbolic Logic), 1 page abstract in J.Bolyai Mathematical Society, Algebraic Logic section, Veszprem, August 1992. Also, appears as an abstract in the Journal of Symbolic Logic.
Rob Nederpelt and Fairouz Kamareddine (1992)
A new framework for the lambda calculus
Abstracts of the 1992 European Summer Meeting of the ASL (Association of Symbolic Logic), 1 page abstract in J.Bolyai Mathematical Society, Computer Science Logic section, Veszprem, August 1992. Also, appears as an abstract in the Journal of Symbolic Logic.

SOME TECHNICAL REPORTS

Fairouz Kamareddine (1991)
$\lambda$-Terms, logic, determiners and quantifiers Glasgow-CSC-91-R7.
Fairouz Kamareddine and Rob Nederpelt (1992)
On Stepwise Explicit Substitution Eindhoven-CSN-92-08. Also, Glasgow-FM-93-05. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine (1992)
Set Theory and Nominalisation, Part I. Eindhoven-CSN-92-12. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine (1992)
Set Theory and Nominalisation, Part II. Eindhoven-CSN-92-13. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine (1992)
A System at the cross Roads of Logic and Functional Programming Eindhoven-CSN-92-15. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine and Rob Nederpelt (1992)
A Unified Approach to Type Theory Using a Refined $\lambda$-calculus Eindhoven-CSN-92-18. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands. Also, Glasgow-FM-93-04.
Fairouz Kamareddine(1992)
Are Types Needed for Natural Language? Eindhoven-CSN-92-20. Also, Glasgow-FM-94-01. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine(1992)
A Type Free Theory of Collective and Distributive Predication Eindhoven-CSN-92-23. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine and Rob Nederpelt (1993)
A Semantics for a Fine $\lambda$-calculus with de Bruijn Indices Eindhoven-CSN-93-28. Also, Glasgow-FM-93-09. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine and Rob Nederpelt (1993)
Canonical Typing and $\Pi$-conversion Eindhoven-CSN-94-02. Also, Glasgow-FM-93-10. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine and Rob Nederpelt (1994)
Refining Reduction in the $\lambda$-calculus Eindhoven-CSN-94-18. Also, Glasgow-FM-94-03. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Roel Bloo, Fairouz Kamareddine and Rob Nederpelt (1994)
Beyond $\beta$-Reduction in CHurch's $\lambda_\rightarrow$ Eindhoven-CSN-94-20. Also, Glasgow-FM-94-04. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Roel Bloo, Fairouz Kamareddine and Rob Nederpelt (1994)
The Barendregt Cube with Definitions and Generalised Reductions Eindhoven-CSN-94-34. Also, Glasgow-FM-94-08. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine and Rob Nederpelt (1994)
Canonical Typing and $\Pi$-conversion in the Barendregt Cube Eindhoven-CSN-94-36. Also, Glasgow-FM-94-10. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Roel Bloo, Fairouz Kamareddine and Rob Nederpelt (1994)
The $\lambda$-Cube with Classes which approximate reductional Equivalence Eindhoven-CS-94-46. Also, Glasgow-FM-94-12. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Roel Bloo, Fairouz Kamareddine and Rob Nederpelt (1994)
Term Reshuffling in the Barendregt Cube Glasgow-FM-94-09.
Fairouz Kamareddine and Twan Laan (1995)
A reflection on Russell's Ramified Types and Kripke's Hierarchy of Truths Eindhoven-CSN-95-18. Also, Glasgow-TR-95-10. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine and Twan Laan (1996)
A Correspondence between Nuprl, the Ramified Theory of Types and Pure Type Systems Eindhoven-CSN-96-12. Also, Glasgow-TR-96-18. Department of Mathematics and Computing Science, Eindhoven University of Technology, the Netherlands.
Fairouz Kamareddine (1994)
Important Issues in Foundational Formalisms Glasgow-FM-94-13.
Fairouz Kamareddine and Alejandro Ríos (1995)
A $\lambda$-calculus \`{a} la de Bruijn \& explicit substitution, Glasgow-TR-95-04.
Fairouz Kamareddine and Alejandro Ríos (1995)
A The $\lambda s$-calculus: its typed and extended versions Glasgow-TR-95-13.
Fairouz Kamareddine and Rob Nederpelt (1996)
A useful $\lambda$-notation Glasgow-TR-95-14.
Roel Bloo, Fairouz Kamareddine and Rob Nederpelt (1995)
Definitions and $\Pi$-conversion in Type Theory Glasgow-TR-95-15.
Fairouz Kamareddine (1996)
A Semantics for step-wise substitution and reduction Glasgow-TR-96-08.
Fairouz Kamareddine (1996)
Postponement, Conservation and Preservation of Strong Normalisation for Generalised Reduction Glasgow-TR-96-11.
Fairouz Kamareddine and Alejandro Ríos (1996)
The confluence of the $\lambda s_e$-calculus via a generalised interpretation method Glasgow-TR-96-19.
Fairouz Kamareddine and Alejandro Ríos (1996)
Bridging de Bruijn Indices and Variable Names in explicit substitutions calculi Glasgow-TR-96-20.
Fairouz Kamareddine and Alejandro Ríos (1996)
Generalised $\beta$-reduction and Explicit Substitutions Glasgow-TR-96-21.
Gilles Barthe, Fairouz Kamareddine and Alejandro Ríos (1996)
Explicit substitutions for the $\lambda \Delta$ calculus Glasgow-TR-96-26.
Fairouz Kamareddine and Alejandro Ríos (1996)
Efficiency of $\lambda$-calculi with explicit substitutions Glasgow-TR-96-30.
Fairouz Kamareddine and Twan Laan (1997)
A Correspondence between Nuprl, the Ramified Theory of Types and Pure Type Systems Glasgow-TR-97-09.
Fairouz Kamareddine and Alejandro Ríos(1997)
Bridging the $\lambda \sigma$ and $\lambda s$ styles of explicit substitutions Glasgow-TR-97-10.
Fairouz Kamareddine, Alejandro Ríos and Joe Wells (1997)
Calculi of Generalised $\beta$-Reduction and Explicit Substitutions: The Type free and Simply Typed Versions Glasgow-TR-97-11.
Fairouz Kamareddine, Roel Bloo and Rob Nederpelt (1997)
An Approximation of Reductional Equivalence Glasgow-TR-97-12.
Fairouz Kamareddine, Roel Bloo and Rob Nederpelt (1997)
On $\Pi$-conversion in the $\lambda$-cube and the combination with abbreviations Glasgow-TR-97-14.

Maintained by Fairouz Kamareddine ()

Selected Publications by Fairouz Kamareddine (see also American Mathematical Society Page and DBLP, Google Scholar and Research Gate)

IN PREPARATION

BOOKS/EDITED BOOKS

JOURNAL PAPERS

ARTICLES IN EDITED BOOKS

EDITED VOLUMES

REFEREED CONFERENCE PAPERS

REFEREED WORKSHOP/SYMPOSIUM PAPERS

NON-REFEREED WORKSHOP PAPERS

CAPSULE REVIEWS

EDITORIALS

AMS REVIEWS (of books and journal articles)

BOOK REVIEWS (NOT FOR AMS)

ABSTRACTS

SOME TECHNICAL REPORTS

Selected Publications by Fairouz Kamareddine
(see also American Mathematical Society Page and DBLP, Google Scholar and Research Gate)