Combinatory Reduction Systems with Explicit Substitution that Preserve Strong Nomalisation. - Roel Bloo; Kristoffer Høgsbro Rose (RTA, 1996)

The Barendregt Cube with Definitions and Generalised Reduction. - Roel Bloo; Fairouz Kamareddine; Rob Nederpelt (Inf. Comput., 1996)

On Pi-Conversion in the lambda-Cube and the Combination with Abbreviations. - Fairouz Kamareddine; Roel Bloo; Rob Nederpelt (Ann. Pure Appl. Log., 1999)

Explicit Substitution On the Edge of Strong Normalization. - Roel Bloo; Herman Geuvers (Theor. Comput. Sci., 1999)

Semantical Aspects of an Architecture for Distributed Embedded Systems. - Roel Bloo; Jozef Hooman; Edwin D. de Jong (SAC (1), 2000)

De Bruijn's Syntax and Reductional Equivalence of Lambda-Terms. - Fairouz Kamareddine; Roel Bloo; Rob Nederpelt (PPDP, 2001)

Pure type systems with explicit substitution. - Roel Bloo (Math. Struct. Comput. Sci., 2001)

Parameters in Pure Type Systems. - Roel Bloo; Fairouz Kamareddine; Twan Laan; Rob Nederpelt (LATIN, 2002)

De Bruijn's syntax and reductional behaviour of lambda-terms: the untyped case. - Fairouz Kamareddine; Roel Bloo (J. Log. Algebraic Methods Program., 2005)

De Bruijn's syntax and reductional behaviour of lambda-terms: the typed case. - Fairouz Kamareddine; Roel Bloo (J. Log. Algebraic Methods Program., 2005)

On Explicit Substitution with Names. - Kristoffer Høgsbro Rose; Roel Bloo; Frédéric Lang (J. Autom. Reason., 2012)