Warning - the bibtex entry below may be invalid: Missing 'booktitle' field @inproceedings{ISSR2009HUH, address = "Los Alamitos, CA, USA", author = "Jun Ho Huh and Andrew Martin", doi = "http://doi.ieeecomputersociety.org/10.1109/ISPA.2009.72", isbn = "978-0-7695-3747-4", journal = "Parallel and Distributed Processing with Applications, International Symposium on", pages = "425-431", publisher = "IEEE Computer Society", title = "Towards a Trustable Virtual Organisation", url = "http://personalpages.manchester.ac.uk/staff/wei.jie/conference/issr2009", volume = "0", year = "2009", } @inproceedings{APTC2008HUH, address = "Los Alamitos, CA, USA", author = "Jun Ho Huh and Andrew Martin", booktitle = "Asia-Pacific Trusted Infrastructure Technologies Conference", pages = "30-42.", publisher = "IEEE Computer Society", title = "Trusted Logging for Grid Computing", url = "http://doi.ieeecomputersociety.org/10.1109/APTC.2008.9", volume = "0", year = "2008", } @techreport{RR-08-11, author = "Andrew Martin", institution = "OUCL", month = "December", number = "RR-08-11", title = "The Ten Page Introduction to Trusted Computing", year = "2008", } @article{knight:variation, author = "Christopher G. Knight and Sylvia H. E. Knight and Neil Massey and Tolu Aina and Carl Christensen and Dave J. Frame and Jamie A. Kettleborough and Andrew Martin and Stephen Pascoe and Ben Sanderson and David A. Stainforth and Myles R. Allen", doi = "10.1073/pnas.0608144104", journal = "Proceedings of the National Academy of Sciences in the United States of America", month = "jul", number = "30", pages = "12259--12264", title = "Association of parameter, software, and hardware variation with large-scale behavior across 57,000 climate models", volume = "104", year = "2007", } @inproceedings{wenbo:tc, author = "{Wenbo Mao} and {Andrew Martin} and {Hai Jin} and {Huanguo Zhang}", booktitle = "Fourteenth International Workshop on Security Protocols", note = "To appear", publisher = "Springer-Verlag", series = "LNCS", title = "Innovations for Grid Security from Trusted Computing", year = "2006", } @article{Massey:CPDN, abstract = "climate\emph{prediction}.net is a large public resource distributed scientific computing project. Members of the public download and run a full-scale climate model, donate their computing time to a large perturbed physics ensemble experiment to forecast the climate in the 21st century and submit their results back to the project. The amount of data generated is large, consisting of tens of thousands of individual runs each in the order of tens of megabytes. The overall dataset is, therefore, in the order of terabytes. Access and analysis of the data is further complicated by the reliance on donated, distributed, federated data servers. This paper will discuss the problems encountered when the data required for even a simple analysis is spread across several servers and how webservice technology can be used; how different user interfaces with varying levels of complexity and flexibility can be presented to the application scientists, how using existing web technologies such as HTTP, SOAP, XML, HTML and CGI can engender the reuse of code across interfaces; and how application scientists can be notified of their analysis? progress and results in an asynchronous architecture.", author = "N. Massey and T. Aina and M. Allen and C. Christensen and D. Frame and D. Goodman and J Kettleborough and A. Martin and S. Pascoe and D. Stainforth", journal = "Advances in Geosciences", month = "jun", pages = "49--56", title = "Data access and analysis with distributed federated data servers in climate\emph{prediction}.net", url = "http://www.oerc.ox.ac.uk/image-library/adgeo-8-49-2006.pdf", volume = "8", year = "2006", } @inproceedings{APM:ac:grid, author = "Andrew Cooper and Andrew Martin", booktitle = "Sixth IEEE International Symposium on Cluster Computing and the Grid (CCGrid 2006), 16-19 May 2006, Singapore", isbn = "0-7695-2585-7", pages = "373-380", publisher = "IEEE Computer Society", title = "Towards a Secure, Tamper-Proof Grid Platform.", year = "2006", } @inproceedings{Spence:Shibgrid, author = "David Spence and Neil Geddes and Jens Jensen and Andrew Richards and Matthew Viljoen and Andrew Martin and Matthew Dovey and Mark Norman and Kang Tang and Anne Trefethen and David Wallom and Rob Allan and David Meredith", booktitle = "eScience 2006, Amsterdam", title = "{ShibGrid}: {Shibboleth} Access for the {UK} {National Grid Service}", year = "2006", } @article{DBLP:journals/entcs/ArenasDMM06, author = "Alvaro E. Arenas and Jin Song Dong and Andrew Martin and Brian Matthews", journal = "Electr. Notes Theor. Comput. Sci.", number = "2", pages = "1", title = "Preface.", volume = "151", year = "2006", } @inproceedings{Cooper:Delegation, author = "Andrew Cooper and Andrew Martin", booktitle = "The Second Workshop on Advances in Trusted Computing", title = "Trusted Delegation for Grid Computing", year = "2006", } @inproceedings{cooper:drm, address = "New York, NY, USA", author = "Andrew Cooper and Andrew Martin", booktitle = "DRM '06: Proceedings of the ACM workshop on Digital rights management", doi = "http://doi.acm.org/10.1145/1179509.1179525", isbn = "1-59593-555-X", location = "Alexandria, Virginia, USA", pages = "79--88", publisher = "ACM Press", title = "Towards an open, trusted digital rights management platform", year = "2006", } @techreport{Martlet:Middleware:OUCL, abstract = "This paper describes a distributed web service based middleware platform, written to support the abstracted parallelisation of functions. This abstraction is achieved through the combination of Martlet, a work-flow language that uses constructs from functional programming to abstract the parallelisation in computations away from the user, and the construction of supporting middleware. To build a middleware that supports this requires the middleware to be able to reason about the data structures it holds without restricting their nature. Issues covered in the development of this supporting middleware include being able to handle distributed data transfer and management, function deployment and execution.", author = "Daniel Goodman", institution = "Oxford University Computing Laboratory", month = "November", number = "RR-05-07", title = "Scientific middleware for abstracted parallelisation", year = "2005", } @inproceedings{MomtahanMartinRoscoe:Taxonomy, author = "Lee Momtahan and Andrew Martin and A. W. Roscoe", booktitle = "Proceedings of Web Languages and Formal Methods", title = "A Taxonomy of Web Services Using {CSP}", year = "2005", } @article{stainforthetal, author = "D. A. Stainforth and T. Aina and C. Christensen and M. Collins and N. Faull and D. J. Frame and J. A. Kettleborough and S. Knight and A. Martin and J. M. Murphy and C. Piani and D. Sexton and L. A. Smith and R. A. Spicer and A. J. Thorpe and M. R. Allen", journal = "Nature", pages = "403--406", title = "Uncertainty in the predictions of the climate response to rising levels of greenhouse gases", volume = "433", year = "2005", } @article{SPE-gridsec, author = "Howard Chivers and Andrew Martin", journal = "Software---Practice and Experience", month = "jul", number = "9", publisher = "Wiley InterScience", title = "Editorial, Guest Editors, Special issue on Grid Security", volume = "35", year = "2005", } @inproceedings{MartinEtAl:TwoKinds, author = "Andrew Martin and Tolu Aina and Carl Christensen and Jamie Kettleborough and David Stainforth", booktitle = "Proceedings of Fourth UK e-Science All Hands Meeting", title = "On two kinds of public-resource distributed computing", year = "2005", } @article{stainforthetal, author = "D. A. Stainforth and T. Aina and C. Christensen and M. Collins and N. Faull and D. J. Frame and J. A. Kettleborough and S. Knight and A. Martin and J. M. Murphy and C. Piani and D. Sexton and L. A. Smith and R. A. Spicer and A. J. Thorpe and M. R. Allen", journal = "Nature", pages = "403--406", title = "Uncertainty in the predictions of the climate response to rising levels of greenhouse gases", volume = "433", year = "2005", } @techreport{RR-04-22, abstract = "Terms such as conversational and stateless are widely used in the taxonomy of web services. We give formal definitions of these terms using the CSP process algebra. Within this framework we also define the notion of Service-Oriented Architecture. These definitions are then used to prove important scalability properties of stateless services. The use of formalism should allow recent debates, concerning how and whether web services provide standardized access to state, to progress more rigorously.", author = "Lee Momtahan and Andrew Martin and A. W. Roscoe", institution = "Oxford University Computing Laboratory", month = "October", number = "RR-04-22", title = "A taxonomy of web services using CSP", year = "2004", } @techreport{RR-04-26, abstract = "DataGrids seek to pool geographically disperse storage and computational resources to solve large-scale data-intensive problems. The EU-DataGrid is a large research project attempting to build one of the first such DataGrids. Effective job submission and scheduling in DataGrids is a significant challenge. We present an account of the EU-DataGrid scheduling architecture, some typical usage scenarios, and a discussion of some of the issues that arose when this architecture was used in practice. Some of these issues are generic, and likely to be of interest to future attempts to build a DataGrid, but also of a pragmatic nature, illuminated by experience as well as theory.", author = "Lee Momtahan and Andrew Martin", institution = "Oxford University Computing Laboratory", month = "February", number = "RR-04-26", title = "Object Models: Job Submission in DataGrids", year = "2004", } @inproceedings{Daviesetal, author = "Jim Davies and Andrew Simpson and Andrew Martin", booktitle = "Symposium on Teaching Formal Methods", editor = "C. Neville Dean and Raymond T. Boute", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", title = "Teaching Formal Methods in Context", volume = "3294", year = "2004", } @inproceedings{GoodmanMartin, author = "Daniel Goodman and Andrew Martin", booktitle = "GGF workshop on building Service-Based Grids, Honolulu, Hawaii", editor = "S. Newhouse and S. Parastatidis", organization = "Global Grid Forum", title = "Grid Style Web Services for ClimatePrediction.net", year = "2004", } @inproceedings{MartinCook, author = "Andrew Martin and Carl Cook", booktitle = "Grid Security Practice and Experience Workshop", editor = "Howard Chivers and Andrew Martin", publisher = "Computer Science Department, University of York, YCS-2004-380", title = "Grids and Private Networks are Anthitetical", year = "2004", } @inproceedings{stainforth:security, author = "Dave Stainforth and Andrew Martin and Andrew Simpson and Carl Christensen and Jamie Kettleborough and Tolu Aina and Myles Allen", booktitle = "13th IEEE International Workshops on Enabling Technologies (WETICE 2004), Infrastructure for Collaborative Enterprises, 14-16 June 2004, Modena, Italy", isbn = "0-7695-2183-5", pages = "319-324", publisher = "IEEE Computer Society", title = "Security Principles for Public-Resource Modeling Research.", year = "2004", } @techreport{RR-03-15, abstract = "Security in grid applications is a wide topic, touching many of the core issues in Information Security. We survey the distinctive features of grids from a security perspective, recording the principal security requirements which arise in some current projects we are engaged with, and in the literature. These include particular requirements on authentication, authorisation, revocation, confidentiality, distributed trust, integrity, and freshness. These requirements inform an analysis of existing technologies deployed in the European DataGrid, and we present an appraisal of the extent to which these meet the requirements presented. The paper includes an analysis of the key software engineering security issues which remain to be addressed.", author = "Philippa J. Broadfoot and Andrew P. Martin", institution = "Oxford University Computing Laboratory", month = "August", number = "RR-03-15", title = "A Critical Survey of Grid Security Requirements and Technologies", year = "2003", } @inproceedings{Simpson_and_Martin_2003, author = "Simpson, A.~C. and Martin, A.~P.", booktitle = "Proceedings of the BCS Teaching Formal Methods workshop", publisher = "BCS", title = "Supplementing the understanding of Z: a formal approach to database design", year = "2003", } @inproceedings{simpson:projects, author = "Simpson, A~C. and Martin, A.~P. and Gibbons, J. and Davies, J.~W. and McKeever, S.~W.", booktitle = "Proceedings of the 25th International Conference on Software Engineering (ICSE), Portland, Oregon, 3--10 May, 2003", pages = "628--633", publisher = "{IEEE} Computer Society Press", title = "On the supervision and assessment of part-time postgraduate software engineering projects", year = "2003", } @inproceedings{zml, author = "Mark Utting and Ian Toyn and Jing Sun and Andrew Martin and Jin Song Dong and Nicholas Daley and David W. Currie", booktitle = "ZB 2003: Formal Specification and Development in Z and B, Third International Conference of B and Z Users, Turku, Finland, June 4-6, 2003, Proceedings", editor = "Didier Bert and Jonathan P. Bowen and Steve King and Marina Wald{\'e}n", isbn = "3-540-40253-5", pages = "437-456", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "{ZML}: {XML} Support for {Standard Z}", volume = "2651", year = "2003", } @techreport{broadfootMartin:grid-sec, address = "Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK", author = "Philippa Broadfoot and Andrew Martin", institution = "Programming Research Group", number = "PRG-RR-03-15", title = "Grid Security: Requirements and Technologies A Survey of the State-of-the-art", type = "Research Report", year = "2003", } @inproceedings{DBLP:conf/icse/SimpsonMGDM03, author = "Andrew Simpson and Andrew Martin and Jeremy Gibbons and Jim Davies and Steve McKeever", booktitle = "Proceedings of the 25th International Conference on Software Engineering, May 3-10, 2003, Portland, Oregon, USA", pages = "628-633", publisher = "IEEE Computer Society", title = "On The Supervision and Assessment Of Part-Time Postgraduate Software Engineering Projects.", year = "2003", } @inproceedings{MartinSimpsonZDB, author = "Andrew Martin and Andrew Simpson", booktitle = "Proceedings of 10th Asia-Pacific Software Engineering Conference", note = "to appear", publisher = "IEEE press", title = "Generalizing the Schema Calculus: Database Schemas and Beyond", year = "2003", } @inproceedings{Stainforth_et_al_2002b, author = "Stainforth, D. and Kettleborough, J.~A. and Martin, A.~P. and Simpson, A.~C. and Martin, A.~P. and Gillis, R. and Akkas, A. and Gault, R. and Collins, M. and Gavaghan, D.~J. and Allen, M.", booktitle = "Proceedings of the 2002 UK e-Science All Hands Meeting", title = "climate\emph{prediction}.com: security and design planning", year = "2002", } @inproceedings{cpdn-arch, author = "Stainforth, D. and Kettleborough, J. and Martin, A. and Simpson, A. and Gillis, R. and Akkas, A. and Gault, R. and Collins, M. and Gavaghan, D. and Allen, M.", booktitle = "Proc. 14th IASTED conference on parallel and distributed computing systems.", title = "Climate\emph{prediction}.net: design principles for public resource modelling research.", year = "2002", } @misc{MartinMomtahan:Challenge, author = "Andrew Martin and Lee Momtahan", booktitle = "UK eScience All Hands Meeting", howpublished = "Poster", note = "UK eScience All Hands Meeting", title = "{e-Science}: A {Software Engineering Challenge}", year = "2002", } @inproceedings{MomtahanMartin:Experiences, author = "Lee Momtahan and Andrew Martin", booktitle = "Proc. Asia-Pacific Software Engineering Conference", pages = "269--275", publisher = "IEEE Press", title = "{e-Science} Experiences: {Software Engineering} Practice and the {EU DataGrid}", year = "2002", } @inproceedings{martinfidge:lifting, author = "A. Martin and C. Fidge", booktitle = "Proceedings of CATS'2001", number = "42", series = "Electronic Notes in Theoretical Computer Science", title = "Lifting in {Z}", year = "2001", } @article{APM:Relating-FACS, author = "A. P. Martin", journal = "Formal Aspects of Computing", pages = "199--209", title = "Relating {Z} and First-order logic", volume = "12", year = "2000", } @article{BrienMartin:Calculus, author = "Stephen Brien and Andrew Martin", journal = "J. Symbolic Computation", number = "1", pages = "63--91", title = "A calculus for schemas in {Z}", volume = "30", year = "2000", } @article{BM:schemas, author = "S. M. Brien and A. P. Martin", journal = "J. Symbolic Computation", number = "1", pages = "63--91", title = "A Calculus for Schemas in {Z}", volume = "30", year = "2000", } @incollection{declarative, address = "New York", author = "H. Glaser and P. H. Hartel and M. Leuschel and A. Martin", booktitle = "Encyclopaedia of Microcomputers", pages = "79--102", publisher = "Marcel Dekker Inc.", title = "Declarative languages in education", volume = "27", year = "2000", } @inproceedings{APM:Relating-FM, author = "Andrew Martin", booktitle = "FM'99 -- Formal Methods", editor = "Jeanette M. Wing and Jim Woodcock and Jim Davies", month = "sep", number = "1708,1709", pages = "1266--1280", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", title = "Relating {Z} and first-order logic", year = "1999", } @inproceedings{soton:tenmethods, abstract = "An abstract model of an industrial distributed data base application has been studied using process based, state based, and queueing theory based methods. The methods supported by graphical notations and/or integrated development environments were found to be easiest to work with. The methods supported by model checkers were the most successful in obtaining relevant information about the application. Applying a number of different methods to study one particular model encourages a problem to be viewed from different angles. This gives complementary information about the model. We report on a variety of problems of the model found through various routes. Our main conclusion is that asking experts to apply different methods and tools at a sufficiently abstract level can be done effectively revealing a broad range of information about the considered application.", address = "Trento, Italy", author = "P. Hartel and M. Butler and A. Currie and P. Henderson and M. Leuschel and A. Martin and A. Smith and U. Ultes-Nitsche and B. Walters", booktitle = "Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems", editor = "S. Gnesi and D. Latella", isbn = "88-7958-009-4", month = "July", organization = "ERCIM", pages = "179-203", publisher = "STAR/CNR, Pisa, Italy", title = "Questions and Answers About Ten Formal Methods", volume = "II", year = "1999", } @inproceedings{fkm98, abstract = "This paper shows how a formal program development environment, previously used only for sequential, non-real-time applications, can be exploited for designing parallel, real-time systems. A pragmatic approach is adopted, making best use of existing technologies, in order to quickly achieve useful results.", author = "C. J. Fidge and P. Kearney and A. P. Martin", booktitle = "Computer Science '98", editor = "C. McDonald", isbn = "981-3083-90-5", note = "Proc. 21st Australasian Computer Science Conference, Perth, 4-6 February 1998. Australian Computer Science Communications, Vol. 20, No. 1. Also available as technical report SVRC-TR-97-36.", pages = "367--378", publisher = "Springer-Verlag", title = "Applying the {Cogito} Program Development Environment to Real-Time System Design", url = "http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?97-36", year = "1998", } @inproceedings{fidge:mpc98, author = "C. J. Fidge and I. J. Hayes and A. P. Martin and A. K. Wabenhorst", booktitle = "Mathematics of Program Construction (MPC'98)", editor = "J. Jeuring", pages = "188--206", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", title = "A Set-Theoretic Model for Real-Time Specification and Reasoning", volume = "1422", year = "1998", } @inproceedings{Us:CogDev, address = "Berlin", author = "Owen Traynor and Dan Hazel and Peter Kearney and Andrew Martin and Ray Nickson and Luke Wildman", booktitle = "Algebraic Methodology and Software Technology", editor = "Michael Johnson", isbn = "3-540-63888-1", issn = "0302-9743", month = "dec", note = "6th International conference, AMAST'97, Sydney, Australia", pages = "586--591", publisher = "Springer-Verlag", series = "LNCS", title = "The {Cogito} development system", volume = "1349", year = "1997", } @inproceedings{HallMartin:WReconstructed, abstract = "An early version of the Z Standard included the deductive system ${\cal W}$ for reasoning about Z specifications. Later versions contain a different deductive system. In this paper we sketch a proof that $\cal W$ is \emph{relatively sound} with respect to this new deductive system. We do this by demonstrating a semantic basis for a correspondence between the two systems, then showing that each of the inference rules of $\cal W$ can be simulated as derived rules in the new system. These new rules are presented as tactics over the the inference rules of the new deductive system.", address = "Berlin Heidelberg", annote = "10th International Conference of Z Users, University of Reading, April 1997, Proceedings", author = "Jon Hall and Andrew Martin", booktitle = "{ZUM'97}: The {Z} Formal Specification Notation, 10th International Conference of {Z} Users, {Reading}, {UK}, April 1997, Proceedings", editor = "Jonathan P. Bowen and Michael G Hinchey and David Till", isbn = "3-540-62717-0", month = "apr", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", title = "W Reconstructed", volume = "1212", year = "1997", } @techreport{MNU:parallel, address = "The University of Queensland, QLD 4072, Australia", author = "Andrew Martin and Ray Nickson and Mark Utting", institution = "Software Verification Research Centre", number = "97-15", title = "Improving {Angel}'s Parallel Operator: {Gumtree}'s Approach", year = "1997", } @inproceedings{MNU:TacErgo, abstract = "A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on \emph{Angel}, for tactic programming, user interface, and proof representation. This paper describes the language as it is used in each of these cases, and explains the details of its implementation in Qu-Prolog. An example from classical propositional calculus is included.", address = "Singapore", author = "A. Martin and R. Nickson and M. Utting", booktitle = "Formal Methods Pacific '97", editor = "Lindsay Groves and Steve Reeves", isbn = "981-3083-31-X", keywords = "tactics,user interface", month = "jul", note = "Also appears as TR97-16, Software Verification Research Centre, The University of Queensland, QLD 4072, Australia", publisher = "Springer-Verlag", series = "Springer Series in Discrete Mathematics and Theoretical Computer Science", title = "A Tactic Language for {Ergo}", year = "1997", } @techreport{me:proof-is-hard, author = "Andrew Martin", institution = "Software Verification Research Centre", number = "97-34", title = "Why effective proof tool support for {Z} is hard", url = "http://svrc.it.uq.edu.au/Bibliography/svrc-tr.html?97-34", year = "1997", } @inproceedings{me:infinite, author = "Andrew Martin", booktitle = "Proceedings of Australian Refinement Workshop", publisher = "University of Queensland", title = "Infinite Lists for Specifying Functional Programs in {Z}", url = "http://www.it.uq.edu.au/MENU/WORKSHOPS-SEMINARS-CONFERENCES/WORKSHOPS/Martin.ps.gz", year = "1996", } @unpublished{Martin:Monads, author = "Andrew Philip Martin", note = "Work in progress", title = "Of Tactics and Monads", year = "1996", } @article{MGW:Tactics, author = "A. P. Martin and P. H. B. Gardiner and J. C. P. Woodcock", journal = "Formal Aspects of Computing", note = "An abridged version appears in the printed journal; the full version is available in the electronic supplement to Formal Aspects of Computing, 8E, pp244--285. http://link.springer.de/link/service/journals/00165/supp/list94\_96.htm", number = "4", pages = "479--489", publisher = "Springer--Verlag", title = "A Tactic Calculus", volume = "8", year = "1996", } @techreport{BM:tutorial, address = "Wolfson Building, Parks Road, Oxford, OX1 3QD, UK", author = "Stephen M. Brien and Andrew P. Martin", institution = "Programming Research Group, Oxford University Computing Laboratory", isbn = "0-902928-94-5", note = "Presented at ZUM'95", number = "PRG-120", title = "A Tutorial on Proof in {Standard Z}", type = "Technical Monograph", year = "1995", } @phdthesis{me:thesis, author = "Andrew Martin", month = "Michaelmas", note = "Also available as Technical Monograph PRG-121, ISBN 0-902928-95-3, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK", school = "University of Oxford", title = "Machine-Assisted Theorem-Proving for Software Engineering", type = "{D.Phil.}\ Thesis", year = "1994", } @unpublished{apm:infZ, author = "Andrew Martin", note = "Draft paper", title = "Infinite Lists in {Z}", year = "1993", } @inproceedings{apm:ew2o, author = "Andrew Martin", booktitle = "FME'93: Industrial-Strength Formal Methods", editor = "J. C. P. Woodcock and P. G. Larsen", isbn = "0-387-56662-7 and 3-540-56662-7", pages = "462--481", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", title = "{Encoding \Wlog : A Logic for Z in 2OBJ}", volume = "670", year = "1993", } @techreport{W&2OBJ:soundness, author = "Hendrik Hilberdink and Andrew Martin", institution = "OUCL(PRG)", month = "June", title = "{Soundness of an Encoding of \Wlog: A Logic for Z in 2OBJ}", type = "Draft Report", year = "1992", } @unpublished{monads-tactics, author = "Andrew Martin and Jeremy Gibbons", note = "Submitted to MPC2002", title = "A Monadic Interpretation of Tactics", }