@UNPUBLISHED{CROaee,
AUTHOR = {Roy L. Crole},
TITLE = {{$\alpha$-Equivalence Equalities}},
NOTE = {Submitted for journal publication},
YEAR = {2010}
}
@ARTICLE{CROrah,
AUTHOR = {Roy L. Crole},
TITLE = {{Representational Adequacy for Hybrid}},
JOURNAL = {Mathematical Structures in Computer Science},
YEAR = {2010},
OPTKEY = {},
OPTVOLUME = {},
OPTNUMBER = {},
OPTPAGES = {},
OPTMONTH = {},
NOTE = {To appear}
}
@UNPUBLISHED{CFuesame,
AUTHOR = {Roy L. Crole and Amy Furniss},
TITLE = {{Using Effect Systems to Automate Model Extraction}},
NOTE = {Presented at UREC 2010, King's College, London},
YEAR = {2010}
}
@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/~rlc3/papers/osamc-notes.pdf},
URL = {http://www.cs.le.ac.uk/~rlc3/papers/osamc-slides.pdf},
PDF = {http://www.cs.le.ac.uk/~rlc3/papers/osamc-slides-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/~rlc3/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/~rcrole/papers/cbslides.ps.gz},
URL = {http://www.cs.le.ac.uk/~rcrole/papers/cbslides.pdf},
PDF = {http://www.cs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/papers/bctms2006.pdf},
URL = {http://www.mcs.le.ac.uk/~rcrole/papers/bctms2006.ps.gz},
PDF = {http://www.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/papers/choasttpci.pdf},
HTTP = {http://www.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/papers/cltt.pdf},
URL = {http://www.mcs.le.ac.uk/~rcrole/papers/cltt-slides.pdf},
PDF = {http://www.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/papers/efoc.ps.gz}
}
@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.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/papers/csnotes11-04-2003.ps.gz},
URL = {http://www.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/papers/rodsioe.ps.gz}
}
@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.mcs.le.ac.uk/~rcrole/papers/semnotes11-04-2003.pdf.gz},
URL = {http://www.mcs.le.ac.uk/~rcrole/papers/semslides11-04-2003.pdf.gz}
}
@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.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/papers/coalg98.pdf},
URL = {http://www.mcs.le.ac.uk/~rcrole/papers/coalg98slides.pdf},
PS = {http://www.mcs.le.ac.uk/~rcrole/papers/coalg98.ps.gz},
PDF = {http://www.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/papers/ios97.ps.gz},
HTTP = {http://www.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/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/~rcrole/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
}
@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/~rcrole/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.mcs.le.ac.uk/~rcrole/papers/cafl.ps.gz},
URL = {http://www.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/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},
HTTP = {http://www.mcs.le.ac.uk/~rcrole/papers/rtvfpo.pdf}
}
@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.mcs.le.ac.uk/~rcrole/papers/thesis.ps.gz},
URL = {http://www.mcs.le.ac.uk/~rcrole/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.mcs.le.ac.uk/~rcrole/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