[1] Roy L. Crole and Amy Furniss. Canonical HybridLF: Extending Hybrid with Dependent Types. To Appear in Logical and Semantic Frameworks and Applications (LSFA), Brazil, August/September 2015. [ bib | .pdf  .pdf ]
[2] Roy L. Crole and Frank Nebel. The Yoneda Lemma and Cartesian Closure in the FM-World. Submitted. [ bib ]
[3] Roy L. Crole. Category Theory. Five lectures on Category Theory for the Midlands Graduate School, Sheffield, 2015. [ bib | .pdf ]
[4] Roy L. Crole. Category Theory. Exercises on Category Theory for the Midlands Graduate School, Sheffield, 2015. [ bib | .pdf ]
[5] Roy L. Crole. Multi-Media and Computer Graphics. Slides on Image Effects in Java, 2014 and 2015. [ bib | .pdf ]
[6] Roy L. Crole. Multi-Media and Computer Graphics. Slides on Audio Effects in Java, 2014 and 2015. [ bib | .pdf ]
[7] Roy L. Crole. Multi-Media and Computer Graphics. Slides on SVG, 2014 and 2015. [ bib | .pdf ]
[8] Roy L. Crole. Multi-Media and Computer Graphics. Slides on Java3D Collision Detection in Java, 2014 and 2015. [ bib | .pdf ]
[9] Roy L. Crole and Frank Nebel. Nominal Lambda Calculus: An Internal Language for FM-Cartesian Closed Categories. In Michael Mislove, editor, Proceedings of Twenty-Ninth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXIX), New Orleans, LA, volume 298, pages 93--117. Electronic Notes in Theoretical Computer Science, November 2013. [ bib | DOI | .pdf ]
[10] Roy L. Crole. α-Equivalence Equalities. Theoretical Computer Science, 433:1--19, May 2012. [ bib | DOI | http ]
[11] Roy L. Crole. Representational Adequacy for Hybrid. Mathematical Structures in Computer Science, 21(3):585--646, March 2011. [ bib | DOI | .pdf | .pdf ]
[12] R. L. Crole. Computer Systems, 2011. Department of Computer Science Lecture Notes, LATEX format vi+121 pages with subject index. [ bib | .pdf | .pdf ]
[13] Roy L. Crole and Amy Furniss. Using Effect Systems to Automate Model Extraction. In M. Fernandez and K. Steinhofel, editors, Proceedings of URC10, King's College, London, volume 1. International Federation for Computational Logic, College Publications, December 2010. [ bib | .pdf | http ]
[14] Roy L. Crole. Categorical Type Theory. Lectures For a Course at Nanchang University, China, 2009. [ bib | .pdf | .pdf | .pdf ]
[15] Roy L. Crole et al. Essential Simultaneous Substitution. Unpublished notes, 2009. [ bib ]
[16] Roy L. Crole. Monads, Recursive Programme Schemes, and Fixpoint Objects. Unpublished notes, 2007. [ bib ]
[17] R. L. Crole. Operational Semantics, Abstract Machines and Correctness, 2006. Lecture Notes for the Midlands Graduate School in the Foundations of Computer Science, LATEX format 91 pages with subject and notation index, plus slides 1-up and 8-up. Revised 2007 and 2008. [ bib | .pdf | .pdf | .pdf ]
[18] R. L. Crole. Functional Programming, 2005. Department of Computer Science Lecture/Slide Notes. [ bib | .pdf | .pdf | .pdf ]
[19] S. J. Ambler, R. L. Crole, and A. Momigliano. A Combinator and Presheaf Topos Model for Primitive Recursion over Higher Order Abstract Syntax. Collegium Logicum, pages 83--90, 2004. CSL 2003 / 8th Kurt Godel Colloquium Poster Collection, Vienna, August, 2003. [ bib | .pdf ]
[20] S. J. Ambler, R. L. Crole, and Alberto Momigliano. A definitional approach to primitive recursion over higher order abstract syntax. In MERLIN '03: Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding, pages 1--11, New York, NY, USA, 2003. ACM Press. [ bib | DOI ]
[21] Roy L. Crole. Coinduction and Bisimulation. Lectures for the International Summer School on the Foundations of Security, University of Oregon, Eugene, USA, June 2003. [ bib | .ps.gz | .pdf | .pdf ]
[22] R. L. Crole. Basic Category Theory for Models of Syntax. In Roland Backhouse and Jeremy Gibbons, editors, Generic Programming International Summer School 2002, Oxford, UK, number 2793 in Lecture Notes in Computer Science, pages 133--177. Springer-Verlag, 2003. [ bib | .pdf | .ps.gz | .pdf ]
[23] S. J. Ambler, R. L. Crole, and A. Momigliano. Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction. In Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics, Hampton, VA, USA, volume 2410 of Lecture Notes in Computer Science, pages 13--30. Springer-Verlag, 2002. [ bib | .ps.gz | .pdf ]
[24] S. J. Ambler, R. L. Crole, and A. Momigliano. A Hybrid Encoding of Howe's Method for Establishing Congruence of Bisimilarity. (Extended Abstract). Electronic Notes in Theoretical Computer Science, 70(2), 2002. Proceedings of the Third International Workshop on Logical Frameworks and Meta-Languages (LFM'02). A FLoC'02 affiliated workshop, Copenhagen, Denmark, July 26, 2002. [ bib | .pdf ]
[25] R. Backhouse, R. L. Crole, and J. Gibbons, editors. Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, volume 2297 of Lecture Notes in Computer Science. Springer-Verlag, 2002. Revised lectures from an International Summer School and Workshop, Oxford, UK, April 2000. [ bib ]
[26] R. L. Crole. Introduction to Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, 2002. Appears in LNCS 2297. [ bib ]
[27] S. J. Ambler, R. L. Crole, and A. Momigliano, editors. Mechanized Reasoning about Languages with Variable Binding (MERLIN 2001), volume 58(1) of Electronic Notes In Theoretical Computer Science, 2001. Final papers of a workshop held in conjunction with the International Joint Conference on Automated Reasoning, IJCAR 2001, Siena, Italy. [ bib | http ]
[28] R. L. Crole. Categorical Logic and Type Theory. Proceedings of the BRICS International EEF Summer School on Logical Foundations, Aarhus, Denmark, June 2001. vi+109 pp with index. [ bib | .pdf | .pdf | .ps.gz ]
[29] A. Momigliano, S. J. Ambler, and R. L. Crole. A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle. In Richard J. Boulton and Paul B. Jackson, editors, Supplemental Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, pages 267--282, 2001. Report EDI-INF-RR-0046. [ bib | .pdf ]
[30] S. J. Ambler, R. L. Crole, and A. Momigliano, editors. Mechanized Reasoning about Languages with Variable Binding (MERLIN 2001). Published by the University of Leicester Department of Mathematics and Computer Science, Report 2001/26, June 2001. Proceedings of a Workshop held in conjunction with the International Joint Conference on Automated Reasoning, IJCAR 2001, Siena, Italy. v1+132pp. [ bib ]
[31] S. J. Ambler, R. L. Crole, and A. Momigliano. A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle. Technical Report 2001/7, Department of Mathematics and Computer Science, University of Leicester, 2001. [ bib | .pdf ]
[32] R. L. Crole. Completeness of Bisimilarity for Contextual Equivalence in Linear Theories. Electronic Journal of the IGPL, 9(1), January 2001. [ bib | http ]
[33] R. L. Crole. Encoding FIX in Object Calculi. RAIRO Journal of Theoretical Informatics and Applications, 34(1):15--38, 2000. [ bib | .pdf ]
[34] R. L. Crole. Review of Essential Visual J++ 6.0 Fast. The Computer Bulletin, page 31, March 2000. [ bib ]
[35] R. L. Crole. Review of Object Oriented Programming and Java. British Computer Society, 1999. [ bib | http ]
[36] S. J. Ambler and R. L. Crole. Mechanised Operational Semantics via (Co)Induction. In Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, Nice, France, volume 1690 of Lecture Notes in Computer Science, pages 221--238. Springer-Verlag, 1999. [ bib | .ps.gz ]
[37] R. L. Crole. Computer Systems, 1999. Department of Mathematics and Computer Science Lecture Notes, LATEX format 93 pages with subject index. Revised 2000, 2001, 2002. [ bib | .ps.gz | .ps.gz ]
[38] R. L. Crole and A. D. Gordon. Relating Operational and Denotational Semantics for Input/Output Effects. Mathematical Structures in Computer Science, 9:125--158, 1999. [ bib | .pdf ]
[39] R. L. Crole. Incompleteness of Linear Bisimilarity for Contextual Equivalence. Technical Report 1999/6, Department of Mathematics and Computer Science, University of Leicester, 1999. [ bib ]
[40] R. L. Crole. Operational Semantics, 1999. Department of Mathematics and Computer Science Lecture Notes, LATEX format 101 pages with subject and notation index. Revised 2000,2001,2003. [ bib | .pdf | .pdf ]
[41] R. L. Crole. Review of Key Java. BCS, 1999. [ bib | http ]
[42] S. J. Ambler and R. L. Crole. Mechanised Operational Semantics via (Co)Induction. Technical Report 1998/22, Department of Mathematics and Computer Science, University of Leicester, 1998. [ bib | .ps.gz ]
[43] R. L. Crole. Encoding FIX in Object Calculi. Technical Report 1998/18, Department of Mathematics and Computer Science, University of Leicester, 1998. [ bib ]
[44] R. L. Crole. Lectures on [Co]Induction and [Co]Algebras. Technical Report 1998/12, Department of Mathematics and Computer Science, University of Leicester, 1998. [ bib | .pdf | .pdf | .ps.gz | .ps.gz ]
[45] R. L. Crole. Modeling FIX in Recursive Object Calculi. Technical Report 1998/10, Department of Mathematics and Computer Science, University of Leicester, 1998. Paper accepted for the CSL/MFCS 98 FICS workshop, Brno, Czech-Republic, August 1998. [ bib ]
[46] R. L. Crole. Program Equivalences for Linear Theories. Technical Report 1998/3, Department of Mathematics and Computer Science, University of Leicester, 1998. [ bib ]
[47] R. L. Crole. Review of Mathematical Theory of Domains. Journal of Formal Aspects of Computing. [ bib ]
[48] R. L. Crole. Notes on the Theory of Objects. Lectured during a reading Group. Foils available from the author. [ bib ]
[49] R. L. Crole. Review of Locally Presentable and Accessible Categories. The Journal of Logic and Computation, 7(6):825--827, 1997. [ bib ]
[50] R. L. Crole. The KOREL Programming Language (Preliminary Report). Technical Report 1997/43, Department of Mathematics and Computer Science, University of Leicester, 1997. [ bib ]
[51] R. L. Crole. Implementing Operational Semantics (Preliminary Report). Technical Report 1997/42, Department of Mathematics and Computer Science, University of Leicester, 1997. [ bib | .pdf | .ps.gz ]
[52] R. L. Crole. How Linear is Howe? In G. McCusker, A. Edalat, and S. Jourdan, editors, Advances in Theory and Formal Methods 1996, pages 60--72. Imperial College Press, 1996. [ bib ]
[53] R. L. Crole. On Fixpoint Objects and Gluing Constructions. Applied Categorical Structures, 4(2 & 3):251--281, 1996. This volume is a Special Edition for the European Colloquium on Category Theory, Tours, France. [ bib ]
[54] R. L. Crole. On Fixpoint Objects and Gluing Constructions. Technical Report 1996/3, Department of Mathematics and Computer Science, University of Leicester, 1996. [ bib | .ps.gz ]
[55] R. L. Crole and A. D. Gordon. Relating Operational and Denotational Semantics for Input/Output Effects. Technical Report 1996/5, Department of Mathematics and Computer Science, University of Leicester, 1996. Submitted to the Journal of Mathematical Structures in Computer Science. [ bib ]
[56] R. L. Crole. How Linear is Howe? Technical Report 1996/17, Department of Mathematics and Computer Science, University of Leicester, 1996. [ bib | .ps.gz ]
[57] R. L. Crole. On Fixpoint Objects for Commutative Faithful Monads. Technical Report 1996/16, Department of Mathematics and Computer Science, University of Leicester, 1996. [ bib ]
[58] R. L. Crole. The Computing Science Research Strategy Group and the Theory Vertical. Article based on an invited address to the 1996 BCS-FACS Annual General Meeting, 1996. [ bib ]
[59] R. L. Crole and A. D. Gordon. A Sound Metalogical Semantics for Input/Output Effects. In L. Pacholski and J. Tiuryn, editors, Proceedings of Computer Science Logic 1994, volume 933 of Lecture Notes in Computer Science, pages 339--353. Springer-Verlag, 1995. [ bib ]
[60] R. L. Crole, S. J. Gay, and R. Nagarajan. An Internal Language for Interaction Categories. In C. L. Hankin, I. C. Mackie, and R. Nagarajan, editors, Theory and Formal Methods 1994, pages 85--104. Imperial College Press, 1995. [ bib | .pdf ]
[61] R. L. Crole. Modal Logic, 1995. Department of Mathematics and Computer Science Lecture Notes, LATEX format, iv+43 pages with index. [ bib | .pdf ]
[62] R. L. Crole. A Note on Tightly Separated Monotone Functions. Unpublished note, 1995. [ bib ]
[63] R. L. Crole. Functional Programming Theory, 1995. Department of Mathematics and Computer Science Lecture Notes, LATEX format iv+68 pages with index. [ bib | .pdf ]
[64] R. L. Crole. Discrete Structures, 1995. Department of Mathematics and Computer Science Lecture Notes, LATEX format iii+59 pages with index. [ bib ]
[65] R. L. Crole. A Guide to LATEX2ε, 1995. Department of Mathematics and Computer Science Lecture Notes. Copies of 53 foils, plus output of sample files. Soft copy of sample files and exercises available. [ bib ]
[66] R. L. Crole. Semantics of Programming Languages, 1995. Department of Mathematics and Computer Science Lecture Notes, LATEX format iii+97 pages with subject and notation index. [ bib | .pdf ]
[67] R. L. Crole. Discrete Structures, 1994. Department of Mathematics and Computer Science Lecture Notes, approx 100 pages, hand-written. [ bib ]
[68] R. L. Crole. Review of Computation and Reasoning. The Computer Journal, 37(6):552--553, 1994. [ bib ]
[69] R. L. Crole. Fixpoint Objects and Enriched Endofunctors. Unpublished note, 1994. [ bib ]
[70] R. L. Crole. Computational Adequacy of the FIX-Logic. Theoretical Computer Science, 136:217--242, 1994. [ bib | .ps.gz | .pdf ]
[71] R. L. Crole and A. D. Gordon. Factoring an Adequacy Proof. In C. J. van Rijsbergen, editor, FP'93 Glasgow Workshop on Functional Programming, Workshops in Computing, pages 9--25. Springer-Verlag, 1994. [ bib | .pdf ]
[72] R. L. Crole. Categories for Types. Cambridge Mathematical Textbooks. Cambridge University Press, 1993. xvii+335 pages, ISBN 0521450926HB, 0521457017PB. [ bib ]
[73] R. L. Crole and A. D. Gordon. Observational Equivalence via Generic Adequacy. Unpublished manuscript, 1993. [ bib ]
[74] R. L. Crole. Categories, Types and Semantics. Hand-written notes for a graduate lecture course, Imperial College Department of Computing, 88 pages, October 1993. [ bib ]
[75] R. L. Crole. Deriving Category Theory from Type Theory. In G. Burn, S. Gay, and M. Ryan, editors, Theory and Formal Methods 1993, Workshops in Computing, pages 15--26. Springer-Verlag, 1993. [ bib | .pdf ]
[76] R. L. Crole and A. M. Pitts. New Foundations for Fixpoint Computations: FIX Hyperdoctrines and the FIX Logic. Information and Computation, 98:171--210, 1992. LICS '90 Special Edition of Information and Computation. [ bib | .pdf ]
[77] R. L. Crole. Recursive Types via Fixpoint Objects. In CLICS Workshop, Aarhus University, Denmark. Aarhus University, 1992. DAIMI PB - 397 - II, May 1992. [ bib ]
[78] R. L. Crole. Programming Metalogics with a Fixpoint Type. Technical Report 247, University of Cambridge Computer Laboratory, 1992. Published version of Ph.D. Thesis. [ bib | .ps.gz | .pdf ]
[79] R. L. Crole. Programming Metalogics with a Fixpoint Type. PhD thesis, Computer Laboratory, University of Cambridge, 1991. [ bib ]
[80] R. L. Crole. Categories, Equational Logic and Typed Lambda Calculi. Hand-Written Notes for a Graduate Lecture Course, University of Cambridge Computer Laboratory, 236 pages, September 1990. [ bib ]
[81] R. L. Crole and A. M. Pitts. New Foundations for Fixpoint Computations. In 5th Annual Symposium on Logic in Computer Science, pages 489--497. I.E.E.E. Computer Society Press, 1990. [ bib | .pdf ]
[82] R. L. Crole and A. M. Pitts. New Foundations for Fixpoint Computations: FIX Hyperdoctrines and the FIX Logic. Technical Report 204, University of Cambridge Computer Laboratory, 1990. [ bib ]
[83] R. L. Crole. K-Theory. An essay submitted for Part III of the Mathematical Tripos, University of Cambridge. [ bib ]

This file was generated by bibtex2html 1.98.