activity
20092024
most citedPrincipal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices

2 citations · 2 across the 6 of their papers we have counts for

collaborators

7 papers

cs.CL2024

Towards Semantic Markup of Mathematical Documents via User Interaction

Luka Vrečar, Joe Wells, Fairouz Kamareddine

Mathematical documents written in LaTeX often contain ambiguities. We can resolve some of them via semantic markup using, e.g., sTeX, which also has other potential benefits, such…

cs.LO2024

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…

math.HO2024

The paradoxes and the infinite dazzled ancient mathematics and continue to do so today

Fairouz Kamareddine, Jonathan Seldin

This paper looks at how ancient mathematicians (and especially the Pythagorean school) were faced by problems/paradoxes associated with the infinite which led them to juggle two sy…

cs.LO2024

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…

cs.LO2020

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…

cs.LO2010★ 2 cited

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…