New Foundations for Fixpoint Computations - Roy L. Crole; Andrew M. Pitts (LICS, 1990)

Programming metalogics with a fixpoint type. - Roy L. Crole (1991)

New Foundations for Fixpoint Computations: FIX-Hyperdoctrines and the FIX-Logic - Roy L. Crole; Andrew M. Pitts (Inf. Comput., 1992)

Categories for Types. - Roy L. Crole (Cambridge University Press, 1993)

Factoring an Adequacy Proof (Preliminary Report). - Roy L. Crole; Andrew D. Gordon 001 (Functional Programming, 1993)

Deriving Category Theory from Type Theory. - Roy L. Crole (Theory and Formal Methods, 1993)

A Sound Metalogical Semantics for Input/Output Effects. - Roy L. Crole; Andrew D. Gordon 001 (CSL, 1994)

An Internal Language for Interaction Categories. - Roy L. Crole; Simon J. Gay; Rajagopal Nagarajan (Theory and Formal Methods, 1994)

Computational Adequacy of the FIX-Logic. - Roy L. Crole (Theor. Comput. Sci., 1994)

On fixpoint objects and gluing constructions. - Roy L. Crole (Appl. Categorical Struct., 1996)

Mechanized Operational Semantics via (Co)Induction. - Simon Ambler; Roy L. Crole (TPHOLs, 1999)

Relating operational and denotational semantics for input/output effects. - Roy L. Crole; Andrew D. Gordon 001 (Math. Struct. Comput. Sci., 1999)

Introduction. - Roy L. Crole (Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, 2000)

Encoding FIX in object calculi. - Roy L. Crole (RAIRO Theor. Informatics Appl., 2000)

Completeness of Bisimilarity for Contextual Equivalence in Linear Theories. - Roy L. Crole (Log. J. IGPL, 2001)

Preface: Mechanised Reasoning about Languages with Variable Binding 2001. - Simon Ambler; Roy L. Crole; Alberto Momigliano (MERLIN, 2001)

Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. - Simon Ambler; Roy L. Crole; Alberto Momigliano (TPHOLs, 2002)

A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity. - Alberto Momigliano; Simon Ambler; Roy L. Crole (LFM, 2002)

Basic Category Theory for Models of Syntax. - Roy L. Crole (Generic Programming, 2003)

A definitional approach to primitivexs recursion over higher order abstract syntax. - S. J. Ambler; Roy L. Crole; Alberto Momigliano (MERLIN, 2003)

The representational adequacy of Hybrid. - Roy L. Crole (Math. Struct. Comput. Sci., 2011)

Alpha equivalence equalities. - Roy L. Crole (Theor. Comput. Sci., 2012)

Nominal Lambda Calculus: An Internal Language for FM-Cartesian Closed Categories. - Roy L. Crole; Frank Nebel (MFPS, 2013)

Canonical HybridLF: Extending Hybrid with Dependent Types. - Roy L. Crole; Amy Elizabeth Furniss (LSFA, 2015)

Equational Logic and Set-Theoretic Models for Multi-Languages. - Samuele Buro; Roy L. Crole; Isabella Mastroeni (ICTCS, 2020)

Equational Logic and Categorical Semantics for Multi-Languages. - Samuele Buro; Roy L. Crole; Isabella Mastroeni (MFPS, 2020)

The nominal/FM Yoneda Lemma. - Roy L. Crole (Math. Struct. Comput. Sci., 2020)

A Social Sensing Model for Event Detection and User Influence Discovering in Social Media Data Streams. - Lei-Lei Shi; Lu Liu 001; Yan Wu 009; Liang Jiang; John Panneerselvam; Roy L. Crole (IEEE Trans. Comput. Soc. Syst., 2020)

On multi-language abstraction: Towards a static analysis of multi-language programs. - Samuele Buro; Roy L. Crole; Isabella Mastroeni (Formal Methods Syst. Des., 2025)