roybib.bib

@UNPUBLISHED{CNylccfmw,
  AUTHOR = {Roy L. Crole and Frank Nebel},
  TITLE = {{The Yoneda Lemma and Cartesian Closure in the FM-World}},
  NOTE = {Submitted},
  YEAR = 2013
}

@INPROCEEDINGS{CNsccsnlc,
  AUTHOR = {Roy L. Crole and Frank Nebel},
  TITLE = {{An Internal Language for FM-Cartesian Closed Categories (The Nominal Lambda Calculus)}},
  OPTCROSSREF = {},
  OPTKEY = {},
  BOOKTITLE = {Proceedings of Mathematical Foundations of Programming Semantics (MFPS), New Orleans, LA},
  OPTPAGES = {},
  YEAR = {2013},
  EDITOR = {Michael Mislove},
  OPTVOLUME = {},
  OPTNUMBER = {},
  OPTSERIES = {},
  OPTADDRESS = {},
  OPTMONTH = {},
  OPTORGANIZATION = {},
  OPTPUBLISHER = {},
  NOTE = {To Appear},
  OPTANNOTE = {}
}

@ARTICLE{CROaee,
  AUTHOR = {Roy L. Crole},
  TITLE = {{$\alpha$-Equivalence Equalities}},
  JOURNAL = {Theoretical Computer Science},
  YEAR = {2012},
  VOLUME = {433},
  OPTNUMBER = {3},
  PAGES = {1-19},
  MONTH = {May},
  DOI = {10.1016/S0304397512000667},
  HTTP = {http://dx.doi.org/10.1016/j.tcs.2012.01.030}
}

@ARTICLE{CROrah,
  AUTHOR = {Roy L. Crole},
  TITLE = {{Representational Adequacy for Hybrid}},
  JOURNAL = {Mathematical Structures in Computer Science},
  YEAR = 2011,
  VOLUME = 21,
  NUMBER = 3,
  PAGES = {585-646},
  MONTH = {March},
  DOI = {10.1017/S0960129511000041},
  HTTP = {http://journals.cambridge.org/repo_A823bIeh},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/rah-slides.pdf}
}

@BOOKLET{CROcsRevisionN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Computer Systems}},
  NOTE = {Department of Computer Science Lecture Notes, 
        \LaTeX\ format vi+121~pages with subject 
        index.},
  YEAR = 2011,
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/csNotes-2011.pdf},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/csSlides-2011.pdf}
}

@INPROCEEDINGS{CFuesame,
  AUTHOR = {Roy L. Crole and Amy Furniss},
  TITLE = {{Using Effect Systems to Automate Model Extraction}},
  BOOKTITLE = {Proceedings of URC10, King's College, London},
  OPTPAGES = {},
  YEAR = {2010},
  EDITOR = {M. Fernandez and K. Steinhofel},
  VOLUME = {1},
  OPTNUMBER = {},
  MONTH = {December},
  ORGANIZATION = {International Federation for Computational Logic},
  PUBLISHER = {College Publications},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/uesame.pdf},
  URL = {http://www.collegepublications.co.uk/ifcolog/ifp/?00001}
}

@UNPUBLISHED{CROcttN,
  AUTHOR = {Roy L. Crole},
  TITLE = {{Categorical Type Theory}},
  NOTE = {Lectures For a Course at Nanchang University, China},
  YEAR = {2009},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cttNanchang-slides.pdf},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cttNanchang-slides-8up.pdf},
  PDF = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cttNanchang-exercises.pdf}
}

@UNPUBLISHED{CROess,
  AUTHOR = {Roy L. Crole et al},
  TITLE = {{Essential Simultaneous Substitution}},
  NOTE = {Unpublished notes},
  YEAR = {2009}
}

@UNPUBLISHED{CROmrpsfo,
  AUTHOR = {Roy L. Crole},
  TITLE = {{Monads, Recursive Programme Schemes, and Fixpoint Objects}},
  NOTE = {Unpublished notes},
  YEAR = 2007
}

@BOOKLET{CROosamcN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Operational Semantics, Abstract Machines and Correctness}},
  NOTE = {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},
  YEAR = {2006},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/osamc-notes.pdf},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/osamc-slides.pdf},
  PDF = {http://www.cs.le.ac.uk/people/rlc3/research/papers/osamc-slides-8up.pdf}
}

@BOOKLET{CROfpN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Functional Programming}},
  NOTE = {Department of Computer Science Lecture/Slide Notes},
  YEAR = {2005},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/fpnotes2005.pdf},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/fpnotes2005-4up.pdf},
  PDF = {http://www.cs.le.ac.uk/people/rlc3/research/papers/fpnotes2005-8up.pdf}
}

@ARTICLE{ACMcptmprhoas,
  AUTHOR = {S.~J.~Ambler and R.~L.~Crole and A.~Momigliano},
  TITLE = {{A Combinator and Presheaf Topos Model for Primitive Recursion over Higher Order Abstract Syntax}},
  JOURNAL = {{Collegium Logicum}},
  PUBLISHER = {Springer-Verlag},
  PAGES = {83-90},
  YEAR = {2004},
  NOTE = {CSL 2003 / 8th Kurt Godel Colloquium Poster Collection, Vienna, August, 2003. },
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cptmprhoas.pdf}
}

@INPROCEEDINGS{ACMdaprhoas,
  AUTHOR = {S. J. Ambler and R. L. Crole and Alberto Momigliano},
  TITLE = {A definitional approach to primitive recursion over higher order abstract syntax},
  BOOKTITLE = {MERLIN '03: Proceedings of the 2003 ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding},
  YEAR = {2003},
  ISBN = {1-58113-800-8},
  PAGES = {1--11},
  LOCATION = {Uppsala, Sweden},
  DOI = {http://doi.acm.org/10.1145/976571.976572},
  PUBLISHER = {ACM Press},
  ADDRESS = {New York, NY, USA}
}

@UNPUBLISHED{CROcb,
  AUTHOR = {Roy L. Crole},
  TITLE = {{Coinduction and Bisimulation}},
  NOTE = {Lectures for the International Summer School on the Foundations of Security, University of Oregon, Eugene, USA},
  MONTH = {June},
  YEAR = {2003},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cbslides.ps.gz},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cbslides.pdf},
  PDF = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cbslides-8up.pdf}
}

@INPROCEEDINGS{CRObctms,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Basic Category Theory for Models of Syntax}},
  BOOKTITLE = {{Generic Programming International Summer School 2002, Oxford, UK}},
  PAGES = {133-177},
  YEAR = {2003},
  EDITOR = {Roland Backhouse and Jeremy Gibbons},
  NUMBER = {2793},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/bctms2006.pdf},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/bctms2006.ps.gz},
  PDF = {http://www.cs.le.ac.uk/people/rlc3/research/papers/bctms2006-slides.pdf}
}

@INPROCEEDINGS{ACMchoasttpci,
  AUTHOR = {S.~J.~Ambler and R.~L.~Crole and A.~Momigliano},
  TITLE = {{Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction}},
  BOOKTITLE = {Proceedings of the 15th International Conference on 
             Theorem Proving in Higher Order Logics, Hampton, VA, USA},
  YEAR = {2002},
  PAGES = {13--30},
  PUBLISHER = {Springer-Verlag},
  VOLUME = {2410},
  SERIES = {Lecture Notes in Computer Science},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/choasttpci.pdf},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/choasttpci.ps.gz}
}

@ARTICLE{ACMmulch,
  AUTHOR = {S.~J.~Ambler and R.~L.~Crole and A.~Momigliano},
  TITLE = {{A Hybrid Encoding of Howe's Method for Establishing
         Congruence of Bisimilarity. (Extended Abstract)}},
  YEAR = 2002,
  VOLUME = 70,
  NUMBER = 2,
  JOURNAL = {Electronic Notes in Theoretical Computer Science},
  NOTE = {Proceedings of the Third International Workshop on
Logical Frameworks and Meta-Languages (LFM'02). A FLoC'02 affiliated workshop,
Copenhagen, Denmark, July 26, 2002.},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/hehmecb.pdf}
}

@PROCEEDINGS{CROacmmpc,
  TITLE = {{Algebraic and Coalgebraic Methods in the Mathematics of Program Construction}},
  YEAR = {2002},
  EDITOR = {R. Backhouse and R. L. Crole and J. Gibbons},
  VOLUME = 2297,
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag},
  NOTE = {Revised lectures from an International Summer School and Workshop, Oxford, UK, April 2000. }
}

@INPROCEEDINGS{CROacmmpci,
  AUTHOR = {R.~L.~Crole},
  BOOKTITLE = {{Algebraic and Coalgebraic Methods in the Mathematics of Program Construction}},
  TITLE = {{Introduction to Algebraic and Coalgebraic Methods in the Mathematics of Program Construction}},
  NOTE = {Appears in LNCS 2297.},
  YEAR = {2002}
}

@PROCEEDINGS{ACMmerlin,
  TITLE = {{Mechanized Reasoning about Languages with Variable Binding (MERLIN~2001)}},
  YEAR = 2001,
  EDITOR = {S.~J.~Ambler and R.~L.~Crole and A.~Momigliano},
  SERIES = {Electronic Notes In Theoretical Computer Science},
  VOLUME = {58(1)},
  NOTE = {{Final papers of a workshop held in conjunction with
the International Joint Conference on Automated Reasoning, IJCAR
2001, Siena, Italy}},
  HTTP = {http://www.elsevier.com/gej-ng/31/29/23/90/27/show/Products/notes/index.htt}
}

@BOOKLET{CRObrics,
  TITLE = {{Categorical Logic and Type Theory}},
  AUTHOR = {R.~L.~Crole},
  HOWPUBLISHED = {{Proceedings of the BRICS International EEF Summer School on Logical Foundations, Aarhus, Denmark}},
  MONTH = {{June}},
  YEAR = 2001,
  NOTE = {vi+109~pp with index},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cltt.pdf},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cltt-slides.pdf},
  PDF = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cltt.ps.gz}
}

@INPROCEEDINGS{ACMcfmlvbi,
  AUTHOR = {A.~Momigliano and S.~J.~Ambler and R.~L.~Crole},
  TITLE = {{A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle}},
  BOOKTITLE = {Supplemental Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics},
  EDITOR = {Richard J. Boulton and Paul B. Jackson},
  YEAR = 2001,
  PAGES = {267--282},
  NOTE = {Report EDI-INF-RR-0046},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cfmtlvbi.pdf}
}

@PROCEEDINGS{ACMpmTR,
  TITLE = {{Mechanized Reasoning about Languages with Variable Binding (MERLIN~2001)}},
  YEAR = 2001,
  EDITOR = {S.~J.~Ambler and R.~L.~Crole and A.~Momigliano},
  PUBLISHER = {Published by the University of Leicester Department of Mathematics and Computer Science, Report~2001/26},
  MONTH = {June},
  NOTE = {{Proceedings of a Workshop held in conjunction with the International Joint Conference on Automated Reasoning, IJCAR 2001, Siena, Italy. v1+132pp.}}
}

@TECHREPORT{ACMcfmlvbiTR,
  AUTHOR = {S.~J.~Ambler and R.~L.~Crole and A.~Momigliano},
  TITLE = {{A Comparison of Formalizations of the Meta-Theory of a Language with Variable Bindings in Isabelle}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 2001,
  NUMBER = {2001/7},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cfmtlvbi.pdf}
}

@ARTICLE{CROcbcelt,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Completeness of Bisimilarity for Contextual Equivalence in
Linear Theories}},
  JOURNAL = {{Electronic Journal of the IGPL}},
  YEAR = 2001,
  MONTH = {{January}},
  VOLUME = 9,
  NUMBER = 1,
  HTTP = {http://www3.oup.co.uk/igpl/Volume_09/Issue_01/}
}

@ARTICLE{CROefoc,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Encoding FIX in Object Calculi}},
  JOURNAL = {{RAIRO Journal of Theoretical Informatics and Applications}},
  YEAR = 2000,
  VOLUME = 34,
  NUMBER = 1,
  PAGES = {15--38},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/efoc.pdf}
}

@ARTICLE{CROevj++REV,
  AUTHOR = {R. L. Crole},
  TITLE = {{Review of \emph{Essential Visual J++ 6.0 Fast}}},
  JOURNAL = {The Computer Bulletin},
  YEAR = 2000,
  MONTH = {{March}},
  PAGES = {31}
}

@ARTICLE{CROoopjREV,
  AUTHOR = {R. L. Crole},
  TITLE = {{Review of \emph{Object Oriented Programming and Java}}},
  JOURNAL = {British Computer Society},
  YEAR = 1999,
  HTTP = {http://www.bcs.org.uk/books/java.htm}
}

@INPROCEEDINGS{ACmosci,
  AUTHOR = {S.~J.~Ambler and R.~L.~Crole},
  TITLE = {{Mechanised Operational Semantics via (Co)Induction}},
  BOOKTITLE = {Proceedings of the 12th International Conference on 
             Theorem Proving in Higher Order Logics, Nice, France},
  YEAR = 1999,
  PAGES = {221--238},
  PUBLISHER = {Springer-Verlag},
  VOLUME = 1690,
  SERIES = {Lecture Notes in Computer Science},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/tphols99.ps.gz}
}

@BOOKLET{CROcsN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Computer Systems}},
  NOTE = {Department of Mathematics and Computer Science Lecture Notes, 
        \LaTeX\ format 93~pages with subject 
        index. Revised 2000, 2001, 2002.},
  YEAR = 1999,
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/csnotes11-04-2003.ps.gz},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/csslides11-04-2003.ps.gz}
}

@ARTICLE{CGrrodsioe,
  AUTHOR = {R.~L.~Crole and A.~D.~Gordon},
  TITLE = {{Relating Operational and Denotational Semantics for Input/Output
        Effects}},
  JOURNAL = {Mathematical Structures in Computer Science},
  VOLUME = {9},
  PAGES = {125--158},
  YEAR = {1999},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/rodsioe.pdf}
}

@TECHREPORT{CROsibceTR,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Incompleteness of Linear Bisimilarity for 
          Contextual Equivalence}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1999,
  NUMBER = {1999/6}
}

@BOOKLET{CROosN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Operational Semantics}},
  NOTE = {Department of Mathematics and Computer Science Lecture Notes, 
        \LaTeX\ format 101~pages with subject 
        and notation index. Revised 2000,2001,2003.},
  YEAR = 1999,
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/semnotes11-04-2003.pdf},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/semslides11-04-2003.pdf}
}

@ARTICLE{CROkjREV,
  AUTHOR = {R. L. Crole},
  TITLE = {{Review of \emph{Key Java}}},
  JOURNAL = {BCS},
  YEAR = 1999,
  HTTP = {http://www.bcs.org.uk/books/program.htm#java}
}

@TECHREPORT{ACmosciTR,
  AUTHOR = {S.~J.~Ambler and R.~L.~Crole},
  TITLE = {{Mechanised Operational Semantics via (Co)Induction}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1998,
  NUMBER = {1998/22},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/mosci98.ps.gz}
}

@TECHREPORT{CROefocTR,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Encoding FIX in Object Calculi}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1998,
  NUMBER = {1998/18}
}

@TECHREPORT{CROlacTR,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Lectures on [Co]Induction and [Co]Algebras}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1998,
  NUMBER = {1998/12},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/coalg98.pdf},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/coalg98slides.pdf},
  PS = {http://www.cs.le.ac.uk/people/rlc3/research/papers/coalg98.ps.gz},
  PDF = {http://www.cs.le.ac.uk/people/rlc3/research/papers/coalg98slides.ps.gz}
}

@TECHREPORT{CROmfroc,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Modeling FIX in Recursive Object Calculi}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1998,
  NUMBER = {1998/10},
  NOTE = {Paper accepted for the CSL/MFCS~98 FICS workshop, 
          Brno, Czech-Republic, August 1998}
}

@TECHREPORT{CROpeltTR,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Program Equivalences for Linear Theories}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1998,
  NUMBER = {1998/3}
}

@UNPUBLISHED{CROmtdREV,
  AUTHOR = {R. L. Crole},
  TITLE = {{Review of \emph{Mathematical Theory of Domains}}},
  NOTE = {Journal of Formal Aspects of Computing}
}

@UNPUBLISHED{CROtooN,
  AUTHOR = {R. L. Crole},
  TITLE = {{Notes on the Theory of Objects}},
  NOTE = {Lectured during a reading Group. Foils available from the author.}
}

@ARTICLE{CROlpacREV,
  AUTHOR = {R. L. Crole},
  TITLE = {Review of \emph{Locally Presentable and Accessible Categories}},
  JOURNAL = {The Journal of Logic and Computation},
  VOLUME = {7},
  NUMBER = {6},
  PAGES = {825--827},
  YEAR = {1997}
}

@TECHREPORT{CROkplTR,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{The KOREL Programming Language (Preliminary Report)}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1997,
  NUMBER = {1997/43}
}

@TECHREPORT{CROiosTR,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Implementing Operational Semantics (Preliminary Report)}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1997,
  NUMBER = {1997/42},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/ios97.ps.gz},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/ios97.pdf}
}

@INPROCEEDINGS{CROhlh,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{How Linear is Howe?}},
  BOOKTITLE = {Advances in Theory and Formal Methods 1996},
  YEAR = 1996,
  PAGES = {60-72},
  EDITOR = {G.~McCusker and A.~Edalat and S.~Jourdan},
  PUBLISHER = {Imperial College Press}
}

@ARTICLE{CROfogc,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{On Fixpoint Objects and Gluing Constructions}},
  JOURNAL = {Applied Categorical Structures},
  YEAR = 1996,
  VOLUME = 4,
  NUMBER = {2 \& 3},
  PAGES = {251--281},
  NOTE = {This volume is a Special Edition for the European Colloquium on 
          Category Theory, Tours, France}
}

@TECHREPORT{CROfogcTR,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{On Fixpoint Objects and Gluing Constructions}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1996,
  NUMBER = {1996/3},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/fogc.ps.gz}
}

@TECHREPORT{CGrodsioeTR,
  AUTHOR = {R.~L.~Crole and A.~D.~Gordon},
  TITLE = {{Relating Operational and Denotational Semantics for Input/Output
        Effects}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1996,
  NUMBER = {1996/5},
  NOTE = {Submitted to the Journal of Mathematical Structures in Computer 
          Science}
}

@TECHREPORT{CROhlihTR,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{How Linear is Howe?}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1996,
  NUMBER = {1996/17},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/hlih.ps.gz}
}

@TECHREPORT{CROfocfmTR,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{On Fixpoint Objects for Commutative Faithful Monads}},
  INSTITUTION = {Department of Mathematics and Computer Science, University of 
Leicester},
  YEAR = 1996,
  NUMBER = {1996/16}
}

@UNPUBLISHED{CROcsrsgtv,
  AUTHOR = {R.~ L.~ Crole},
  TITLE = {{The Computing Science Research Strategy Group and the 
           \emph{Theory Vertical}}},
  JOURNAL = {BCS-FACS Newsletter},
  YEAR = 1996,
  NOTE = {Article based on an invited address to the 
          1996 BCS-FACS Annual General Meeting}
}

@INPROCEEDINGS{CGrodsioe,
  AUTHOR = {R. L. Crole and A. D. Gordon},
  TITLE = {{A Sound Metalogical Semantics for Input/Output Effects}},
  BOOKTITLE = {Proceedings of Computer Science Logic 1994},
  YEAR = 1995,
  EDITOR = {L.~Pacholski and J.~Tiuryn},
  PAGES = {339--353},
  PUBLISHER = {Springer-Verlag},
  VOLUME = 933,
  SERIES = {Lecture Notes in Computer Science}
}

@INPROCEEDINGS{CGNilic,
  AUTHOR = {R.~L.~Crole and S.~J.~Gay and R.~Nagarajan},
  TITLE = {{An Internal Language for Interaction Categories}},
  BOOKTITLE = {Theory and Formal Methods 1994},
  YEAR = 1995,
  EDITOR = {C.~L.~Hankin and I.~C.~Mackie and R.~Nagarajan},
  PAGES = {85--104},
  PUBLISHER = {Imperial College Press}
}

@BOOKLET{CROmlN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Modal Logic}},
  NOTE = {Department of Mathematics and Computer Science Lecture Notes, 
        \LaTeX\ format, iv+43~pages with index},
  YEAR = 1995,
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/modallogicnotes1996.pdf}
}

@UNPUBLISHED{CROtsmf,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{A Note on Tightly Separated Monotone Functions}},
  NOTE = {Unpublished note},
  YEAR = 1995
}

@BOOKLET{CROfptN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Functional Programming Theory}},
  NOTE = {Department of Mathematics and Computer Science Lecture Notes, 
        \LaTeX\ format iv+68~pages with index},
  YEAR = 1995,
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/fptnotes1996.pdf}
}

@BOOKLET{CROdsN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Discrete Structures}},
  NOTE = {Department of Mathematics and Computer Science Lecture Notes, 
        \LaTeX\ format iii+59~pages with index},
  YEAR = 1995
}

@BOOKLET{CROglN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{A Guide to \LaTeX$2\epsilon$}},
  NOTE = {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},
  YEAR = 1995
}

@BOOKLET{CROsplN,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Semantics of Programming Languages}},
  NOTE = {Department of Mathematics and Computer Science Lecture Notes, 
        \LaTeX\ format iii+97~pages with subject 
        and notation index},
  YEAR = 1995,
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/spl-notes.pdf}
}

@BOOKLET{CROdsHW,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Discrete Structures}},
  NOTE = {Department of Mathematics and Computer Science Lecture Notes, 
        approx~100 pages, hand-written},
  YEAR = 1994
}

@ARTICLE{CROcrREV,
  AUTHOR = {R. L. Crole},
  TITLE = {{Review of \emph{Computation and Reasoning}}},
  JOURNAL = {The Computer Journal},
  YEAR = 1994,
  VOLUME = 37,
  NUMBER = 6,
  PAGES = {552--553}
}

@UNPUBLISHED{CROfoee,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Fixpoint Objects and Enriched Endofunctors}},
  NOTE = {Unpublished note},
  YEAR = 1994
}

@ARTICLE{CROLcafl,
  AUTHOR = {R. L. Crole},
  TITLE = {{Computational Adequacy of the FIX-Logic}},
  JOURNAL = {Theoretical Computer Science},
  YEAR = 1994,
  VOLUME = 136,
  PAGES = {217--242},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cafl.ps.gz},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/cafl.pdf}
}

@INPROCEEDINGS{CGfap,
  AUTHOR = {R. L. Crole and A. D. Gordon},
  TITLE = {{Factoring an Adequacy Proof}},
  BOOKTITLE = {FP'93 Glasgow Workshop on Functional Programming},
  YEAR = 1994,
  EDITOR = {C.~J. van~Rijsbergen},
  PUBLISHER = {Springer-Verlag},
  PAGES = {9--25},
  SERIES = {Workshops in Computing},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/fap.pdf}
}

@BOOK{CROct,
  AUTHOR = {R. L. Crole},
  TITLE = {{Categories for Types}},
  PUBLISHER = {Cambridge University Press},
  YEAR = 1993,
  SERIES = {Cambridge Mathematical Textbooks},
  NOTE = {xvii+335 pages, ISBN 0521450926HB, 0521457017PB}
}

@UNPUBLISHED{CROGORoega,
  AUTHOR = {R. L. Crole and A. D. Gordon},
  TITLE = {{Observational Equivalence via Generic Adequacy}},
  NOTE = {Unpublished manuscript},
  YEAR = 1993
}

@UNPUBLISHED{CROctsN,
  AUTHOR = {R. L. Crole},
  TITLE = {{Categories, Types and Semantics}},
  YEAR = 1993,
  MONTH = {October},
  NOTE = {Hand-written notes for a graduate lecture course,
          Imperial College Department of Computing, 88~pages}
}

@INPROCEEDINGS{BGRtfm93,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{Deriving Category Theory from Type Theory}},
  BOOKTITLE = {Theory and Formal Methods 1993},
  YEAR = 1993,
  EDITOR = {G.~Burn and S.~Gay and M.~Ryan},
  PAGES = {15--26},
  PUBLISHER = {Springer-Verlag},
  SERIES = {Workshops in Computing},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/dcttt.pdf}
}

@ARTICLE{CPfhfl,
  AUTHOR = {R. L. Crole and A. M. Pitts},
  TITLE = {{New Foundations for Fixpoint Computations: \mbox{FIX}
		 Hyperdoctrines and the \mbox{FIX} Logic}},
  JOURNAL = {Information and Computation},
  YEAR = 1992,
  VOLUME = 98,
  PAGES = {171--210},
  NOTE = {LICS '90 Special Edition of Information and Computation},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/nffc-IC.pdf}
}

@INPROCEEDINGS{CROrtfo,
  AUTHOR = {R. L. Crole},
  TITLE = {{Recursive Types via Fixpoint Objects}},
  BOOKTITLE = {CLICS Workshop, Aarhus University, Denmark},
  YEAR = 1992,
  PUBLISHER = {Aarhus University},
  NOTE = {DAIMI~PB~-~397~-~II, May 1992}
}

@TECHREPORT{CROpmfptTR,
  AUTHOR = {R. L. Crole},
  TITLE = {{Programming Metalogics with a Fixpoint Type}},
  INSTITUTION = {University of Cambridge Computer Laboratory},
  YEAR = 1992,
  NUMBER = {247},
  NOTE = {Published version of Ph.D. Thesis},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/thesis.ps.gz},
  URL = {http://www.cs.le.ac.uk/people/rlc3/research/papers/thesis.pdf}
}

@PHDTHESIS{CROLphd,
  AUTHOR = {R. L. Crole},
  TITLE = {{Programming Metalogics with a Fixpoint Type}},
  SCHOOL = {Computer Laboratory, University of Cambridge},
  YEAR = 1991
}

@UNPUBLISHED{CROLcetN,
  AUTHOR = {R. L. Crole},
  TITLE = {{Categories, Equational Logic and Typed Lambda Calculi}},
  NOTE = {Hand-Written Notes for a Graduate Lecture Course, 
                University of Cambridge Computer Laboratory, 236 pages},
  YEAR = 1990,
  MONTH = {September}
}

@INPROCEEDINGS{CPnffc,
  AUTHOR = {R. L. Crole and A. M. Pitts},
  TITLE = {{New Foundations for Fixpoint Computations}},
  BOOKTITLE = {5th Annual Symposium on Logic in Computer Science},
  YEAR = 1990,
  PAGES = {489--497},
  PUBLISHER = {I.E.E.E. Computer Society Press},
  HTTP = {http://www.cs.le.ac.uk/people/rlc3/research/papers/nffc.pdf}
}

@TECHREPORT{CROfhflTR,
  AUTHOR = {R. L. Crole and A. M. Pitts},
  TITLE = {{New Foundations for Fixpoint Computations: \mbox{FIX}
		 Hyperdoctrines and the \mbox{FIX} Logic}},
  INSTITUTION = {University of Cambridge Computer Laboratory},
  YEAR = 1990,
  NUMBER = {204}
}

@UNPUBLISHED{CROktccs,
  AUTHOR = {R.~L.~Crole},
  TITLE = {{K-Theory}},
  NOTE = {An essay submitted for Part~III of the Mathematical Tripos, 
          University of Cambridge}
}


This file has been generated by bibtex2html 1.80