Covarieties of Coalgebras: Comonads and Coequations. - Ranald Clouston; Robert Goldblatt (ICTAC, 2005)

Nominal Equational Logic. - Ranald Alexander Clouston; Andrew M. Pitts (Computation, Meaning, and Logic, 2007)

Binding in Nominal Equational Logic. - Ranald Clouston (MFPS, 2010)

Equational logic for names and binders. - Ranald Alexander Clouston (2010)

Nominal Lawvere Theories. - Ranald Clouston (WoLLIC, 2011)

Nominal Logic with Equations Only - Ranald Clouston (LFMTP, 2011)

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. - Ranald Clouston; Jeremy E. Dawson; Rajeev Goré; Alwen Tiu (CSL, 2013)

Generalised Name Abstraction for Nominal Sets. - Ranald Clouston (FoSSaCS, 2013)

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic - Extended Version. - Ranald Clouston; Jeremy E. Dawson; Rajeev Goré; Alwen Tiu (CoRR, 2013)

From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic. - Jeremy E. Dawson; Ranald Clouston; Rajeev Goré; Alwen Tiu (IFIP TCS, 2014)

Proof search for propositional abstract separation logics via labelled sequents. - Zhe Hou; Ranald Clouston; Rajeev Goré; Alwen Tiu (POPL, 2014)

Nominal Lawvere Theories: A category theoretic account of equational theories with names. - Ranald Clouston (J. Comput. Syst. Sci., 2014)

Programming and Reasoning with Guarded Recursion for Coinductive Types. - Ranald Clouston; Ales Bizjak; Hans Bugge Grathwohl; Lars Birkedal (FoSSaCS, 2015)

Sequent Calculus in the Topos of Trees. - Ranald Clouston; Rajeev Goré (FoSSaCS, 2015)

Guarded Cubical Type Theory: Path Equality for Guarded Recursion. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (CSL, 2016)

Guarded Dependent Type Theory with Coinductive Types. - Ales Bizjak; Hans Bugge Grathwohl; Ranald Clouston; Rasmus Ejlers Møgelberg; Lars Birkedal (FoSSaCS, 2016)

Separata: Isabelle tactics for Separation Algebra. - Zhe Hou; David Sanán; Alwen Tiu; Rajeev Goré; Ranald Clouston (Arch. Formal Proofs, 2016)

The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. - Ranald Clouston; Ales Bizjak; Hans Bugge Grathwohl; Lars Birkedal (Log. Methods Comput. Sci., 2016)

Fitch-Style Modal Lambda Calculi. - Ranald Clouston (FoSSaCS, 2018)

Modal Dependent Type Theory and Dependent Right Adjoints. - Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters (CoRR, 2018)

Modular Labelled Sequent Calculi for Abstract Separation Logics. - Zhe Hou; Ranald Clouston; Rajeev Goré; Alwen Tiu (ACM Trans. Comput. Log., 2018)

Guarded Cubical Type Theory. - Lars Birkedal; Ales Bizjak; Ranald Clouston; Hans Bugge Grathwohl; Bas Spitters; Andrea Vezzosi (J. Autom. Reason., 2019)

Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents. - Tim S. Lyon; Alwen Tiu; Rajeev Goré; Ranald Clouston (CSL, 2020)

Modal dependent type theory and dependent right adjoints. - Lars Birkedal; Ranald Clouston; Bassel Mannaa; Rasmus Ejlers Møgelberg; Andrew M. Pitts; Bas Spitters (Math. Struct. Comput. Sci., 2020)

Semantical Analysis of Intuitionistic Modal Logics between CK and IK. - Jim de Groot; Ian Shillito; Ranald Clouston (CoRR, 2024)