Ranald Clouston

Preprints of Publications

Guarded Cubical Type Theory: Path Equality for Guarded Recursion
With Lars Birkedal, Aleš Bizjak, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi.
In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Jean-Marc Talbot and Laurent Regnier (eds.), Leibniz International Proceedings in Informatics vol. 62, © L. Birkedal, A. Bizjak, R. Clouston, H. B. Grathwohl, B. Spitters, A. Vezzosi, (2016). (pdf)

The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types
With Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal.
In Logical Methods in Computer Science, Special Issue: 18th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2015), Thomas Colcombet, Andrew M. Pitts, and Daniele Varacca (eds.), accepted, to appear (2016). (pdf)

Guarded Dependent Type Theory with Coinductive Types
With Aleš Bizjak, Hans Bugge Grathwohl, Rasmus E. Møgelberg, and Lars Birkedal.
In Foundations of Software Science and Computation Structures (19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings), Bart Jacobs and Christof Löding (eds.), Lecture Notes in Computer Science, vol. 9634, pp. 20-35, © Springer-Verlag (2016). (pdf)
Also available via arXiv: arXiv:1601.01586 [cs.LO]

Programming and Reasoning with Guarded Recursion for Coinductive Types
With Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal.
In Foundations of Software Science and Computation Structures (18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings), Andrew Pitts (ed.), Lecture Notes in Computer Science, vol. 9034, pp. 407-421, © Springer-Verlag (2015). (pdf)
Also available via arXiv: arXiv:1501.02925 [cs.PL]

Sequent Calculus in the Topos of Trees
With Rajeev Goré.
In Foundations of Software Science and Computation Structures (18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings), Andrew Pitts (ed.), Lecture Notes in Computer Science, vol. 9034, pp. 133-147, © Springer-Verlag (2015). (pdf)
Also available via arXiv: arXiv:1501.03293 [cs.LO]

From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic
With Jeremy E. Dawson, Rajeev Goré, and Alwen Tiu.
In Theoretical Computer Science: 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014 Proceedings. Josep Diaz, Ivan Lanese, and Davide Sangiorgi (eds.), Lecture Notes in Computer Science vol. 8705, pp. 250-264, © IFIP (2014). (pdf)

Proof Search for Propositional Abstract Separation Logics via Labelled Sequents
With Zhé Hóu, Rajeev Goré, and Alwen Tiu.
In POPL '14 Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Peter Sewell (ed.), ACM SIGPLAN Notices vol. 49 issue 1, pp. 465-476, © ACM (2014). (pdf)
Extended version available as arXiv preprint: arXiv:1307.5592 [cs.LO]

Nominal Lawvere Theories: A Category Theoretic Account of Equational Theories with Names
In Journal of Computer and System Sciences vol. 80, Issue 6, Special issue: 18th Workshop on Logic, Language, Information and Computation (WoLLIC 2011), Lev Beklemishev, Ruy de Queiroz and Andre Scedrov (eds.), pp. 1067-1086, © Elsevier (2014). (pdf)

Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic
With Jeremy Dawson, Rajeev Goré, and Alwen Tiu.
In Computer Science Logic 2013 (CSL 2013), Simona Ronchi Della Rocca (ed.), Leibniz International Proceedings in Informatics vol. 23, pp. 197 - 214, © R. Clouston, J. Dawson, R. Goré, A. Tiu (2013). (pdf)
Extended version available as arXiv preprint: arXiv:1307.0289 [cs.LO]

Generalised Name Abstraction for Nominal Sets
In Foundations of Software Science and Computation Structures (16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013, Proceedings). Frank Pfenning (ed.), Lecture Notes in Computer Science vol. 7794, pp. 434 - 449, © Springer-Verlag (2013). (pdf)

Nominal Logic with Equations Only.
In Proceedings of the Sixth International Workshop on Logical Frameworks and Meta-languages: Theory and Practice (LFMTP 2011), Nijmegen, The Netherlands, August 26, 2011. Herman Geuvers and Gopalan Nadathur (eds.), Electronic Proceedings in Theoretical Computer Science vol. 71, pp. 44 - 57, © R. Clouston (2011). (pdf)

Nominal Lawvere Theories.
In Logic, Language, Information and Computation: 18th International Workshop, WoLLIC 2011. Lev Beklemishev and Ruy de Queiroz (eds.) Lecture Notes in Computer Science vol. 6642, pp. 67 - 83, © Springer-Verlag (2011). (pdf)

Binding in Nominal Equational Logic.
In Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2010). Michael Mislove and Peter Selinger (eds.), Electronic Notes in Theoretical Computer Science vol. 265, pp 259 - 276, © Elsevier (2010). (pdf)

Nominal Equational Logic.
With Andrew M. Pitts. In Computation, Meaning and Logic: Articles dedicated to Gordon Plotkin. Luca Cardelli, Marcelo Fiore, and Glynn Winskel (eds.), Electronic Notes in Theoretical Computer Science vol. 172, pp 223 - 257, © Elsevier (2007). (pdf)

Covarieties of Coalgebras: Comonads and Coequations.
With Robert Goldblatt. In Theoretical Aspects of Computing - ICTAC 2005: Second International Colloquium, Hanoi, Vietnam, October 17-21, 2005, Proceedings. Dang Van Hung and Martin Wirsing (eds.), Lecture Notes in Computer Science vol. 3722, pp 288 - 302, © Springer-Verlag (2005). (pdf)

Theses

Equational Logic for Names and Binders.
Ph.D. thesis, University of Cambridge (2009). (pdf)

Comonads, Coequations and Behavioural Covarieties.
M.Sc. thesis, Victoria University of Wellington (2004). (pdf)

Unpublished notes

These are some notes relating to nominal rewriting that I've been asked to put online; please excuse any typos or other errors.

Closed Terms.
Unpublished notes (2007). (pdf)