Ranald Clouston

Ranald Clouston is a Lecturer HDR Convener Computing Foundations MComp Co-Convener at The Australian National University, School of Computing. His research interests include creating new logics or adapting existing ones to solve problems in computer science, with a focus on logics for recursively defined infinite structures, mutable resources, and variable names. He is particularly interested in applying logics to type systems for ensuring well-behaved code and supporting formally checked mathematics. Clouston studied Logic and Computation as an undergraduate at Victoria University of Wellington and completed a PhD at the University of Cambridge in 2010. He worked as a research fellow at ANU, then as a postdoc and assistant lecturer at Aarhus University before returning to ANU in 2018.

Ranald Clouston is a Lecturer at the Australian National University, specializing in Logic, Semantics, and Type Theory. His research focuses on the intersection of modal logic, type theory, and formal semantics, with an emphasis on guarded recursion, coinductive types, and modal lambda calculi. He has contributed to the development of guarded dependent type theory, guarded cubical type theory, and Fitch-style modal lambda calculi. His work explores the semantics of intuitionistic modal logics, nominal equational logic, and the formalization of logical systems using sequent calculi and labelled sequents. Clouston's research also includes the study of binding and name management in equational logic and the application of these concepts to programming and reasoning.