12 found
Sort by:
Disambiguations:
Fairouz Kamareddine [18]Fairouz D. Kamareddine [1]
  1. Fairouz Kamareddine, Types and Functions Since Principia.
    Types were invented by Russell to solve the logical paradoxes that resulted from Frege’s generalisaton of the notion of function. Since, the past 100 years saw new formalisations of the notions of functions and types that extend and put to better use Frege’s and Russell’s inventions. Most such formalisations are extensions of Church’s simply typed λ-calculus (Church’s calculus of functions together with Ramsey’s simplification of Russell’s types). Currently, types and functions are the heart of logic and computation (...)
    No categories
    Translate to English
    | Direct download  
     
    My bibliography  
     
    Export citation  
  2. Fairouz Kamareddine & Karim Nour (2007). A Completeness Result for a Realisability Semantics for an Intersection Type System. Annals of Pure and Applied Logic 146 (2):180-198.
    In this paper we consider a type system with a universal type $omega$ where any term (whether open or closed, $beta$-normalising or not) has type $omega$. We provide this type system with a realisability semantics where an atomic type is interpreted as the set of $lambda$-terms saturated by a certain relation. The variation of the saturation relation gives a number of interpretations to each type. We show the soundness and completeness of our semantics and that for different notions of saturation (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Mauricio Ayala-Rincón, Flávio L. C. de Moura & Fairouz Kamareddine (2005). Comparing and Implementing Calculi of Explicit Substitutions with Eta-Reduction. Annals of Pure and Applied Logic 134 (1):5-41.
    The past decade has seen an explosion of work on calculi of explicit substitutions. Numerous works have illustrated the usefulness of these calculi for practical notions like the implementation of typed functional programming languages and higher order proof assistants. It has also been shown that eta-reduction is useful for adapting substitution calculi for practical problems like higher order unification. This paper concentrates on rewrite rules for eta-reduction in three different styles of explicit substitution calculi: λσ, λse and the suspension calculus. (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  4. Fairouz Kamareddine & Rob Nederpelt (2004). A Refinement of de Bruijn's Formal Language of Mathematics. Journal of Logic, Language and Information 13 (3):287-340.
    We provide a syntax and a derivation system fora formal language of mathematics called Weak Type Theory (WTT). We give the metatheory of WTT and a number of illustrative examples.WTT is a refinement of de Bruijn''s Mathematical Vernacular (MV) and hence:– WTT is faithful to the mathematician''s language yet isformal and avoids ambiguities.
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  5. Fairouz Kamareddine, Twan Laan & Rob Nederpelt (2002). Types in Logic and Mathematics Before 1940. Bulletin of Symbolic Logic 8 (2):185-245.
    In this article, we study the prehistory of type theory up to 1910 and its development between Russell and Whitehead's Principia Mathematica ([71], 1910-1912) and Church's simply typed λ-calculus of 1940. We first argue that the concept of types has always been present in mathematics, though nobody was incorporating them explicitly as such, before the end of the 19th century. Then we proceed by describing how the logical paradoxes entered the formal systems of Frege, Cantor and Peano concentrating on Frege's (...)
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  6. Fairouz Kamareddine, T. Nederpelt & R. Laan (2002). Types in Mathematics and Logic Before 1940. Bulletin of Symbolic Logic 8 (2).
     
    My bibliography  
     
    Export citation  
  7. Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information 10 (3):375-402.
    In Russell''s Ramified Theory of Types RTT, two hierarchical concepts dominate:orders and types. The use of orders has as a consequencethat the logic part of RTT is predicative.The concept of order however, is almost deadsince Ramsey eliminated it from RTT. This is whywe find Church''s simple theory of types (which uses the type concept without the order one) at the bottom of the Barendregt Cube rather than RTT. Despite the disappearance of orders which have a strong correlation with predicativity, predicative (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  8. Fairouz Kamareddine, Roel Bloo & Rob Nederpelt (1999). On Π-Conversion in the Λ-Cube and the Combination with Abbreviations. Annals of Pure and Applied Logic 97 (1-3):27-45.
    Typed λ-calculus uses two abstraction symbols which are usually treated in different ways: λx:*.x has as type the abstraction Πx:*.*, yet Πx:*.* has type □ rather than an abstraction; moreover, C is allowed and β-reduction evaluates it, but C is rarely allowed. Furthermore, there is a general consensus that λ and Π are different abstraction operators. While we agree with this general consensus, we find it nonetheless important to allow Π to act as an abstraction operator. Moreover, experience with AUTOMATH (...)
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  9. Fairouz Kamareddine (1995). A Type Free Theory and Collective/Distributive Predication. Journal of Logic, Language and Information 4 (2):85-109.
    The purpose of this paper is to provide a simple type-free set theory which can be used to give the various readings of collective/distributive sentences.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  10. Fairouz Kamareddine & Ewan Klein (1993). Nominalization, Predication and Type Containment. Journal of Logic, Language and Information 2 (3):171-215.
    In an attempt to accommodate natural language phenomena involving nominalization and self-application, various researchers in formal semantics have proposed abandoning the hierarchical type system which Montague inherited from Russell, in favour of more flexible type regimes. We briefly review the main extant proposals, and then develop a new approach, based semantically on Aczel's notion of Frege structure, which implements a version ofsubsumption polymorphism. Nominalization is achieved by virtue of the fact that the types of predicative and propositional complements are contained (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  11. Fairouz Kamareddine & Ewan Klein (1993). Polymorphism, Type Containment and Nominalization. Journal of Logic, Language and Information 2 (3):171-215.
     
    My bibliography  
     
    Export citation  
  12. Fairouz Kamareddine (1992). Λ-Terms, Logic, Determiners and Quantifiers. Journal of Logic, Language and Information 1 (1):79-103.
    In this paper, a theory T H based on combining type freeness with logic is introduced and is then used to build a theory of properties which is applied to determiners and quantifiers.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation