12 found
Sort by:
  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.
    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.
    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