2 citations · 2 across the 6 of their papers we have counts for
4 papers · 1 filter
Intersection Types via Finite-Set Declarations
Fairouz Kamareddine, Joe Wells
The lambda-cube is a famous pure type system (PTS) cube of eight powerful explicit type systems that include the simple, polymorphic and dependent type theories. The lambda-cube on…
Substitution in the lambda Calculus and the role of the Curry School
Fairouz Kamareddine
Substitution plays a prominent role in the foundation and implementation of mathematics and computation. In the lambda calculus, we cannot define alpha congruence without a form of…
Adding an Abstraction Barrier to ZF Set Theory
Ciarán Dunne, J. B. Wells, Fairouz Kamareddine
Much mathematical writing exists that is, explicitly or implicitly, based on set theory, often Zermelo-Fraenkel set theory (ZF) or one of its variants. In ZF, the domain of discour…
Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices
Daniel Ventura, Mauricio Ayala-Rincón, Fairouz Kamareddine
The lambda-calculus with de Bruijn indices assembles each alpha-class of lambda-terms in a unique term, using indices instead of variable names. Intersection types provide finitary…