Bill Roscoe : Publications
-
[0]
Notes on Domain Theory
A. W. Roscoe
1989.
These notes were written for the Oxford Domain Theory course between 1984 and 1989. I originally planned to publish them as half of "Domains for denotational semantics".
Details about Notes on Domain Theory | BibTeX data for Notes on Domain Theory | Download (pdf) of Notes on Domain Theory
-
[1]
A theory of communicating sequential processes
A. W. Roscoe‚ S.D. Brookes and C. A. R. Hoare
No. PRG−16. Oxford University Computing Laboratory. May, 1981.
Details about A theory of communicating sequential processes | BibTeX data for A theory of communicating sequential processes | Download (pdf) of A theory of communicating sequential processes
-
[2]
A mathematical theory of communicating processes
A. W. Roscoe
PhD Thesis , type= D. Phil. Thesis. Oxford University. 1982.
Please note this is a 270 page‚ 118 Mb scanned file and will take some time to download.
Details about A mathematical theory of communicating processes | BibTeX data for A mathematical theory of communicating processes | Download (pdf) of A mathematical theory of communicating processes
-
[3]
Criteria for metrisability
A. W. Roscoe and P.J. Collins
In Proc. Amer. Math. Soc.. No. 90. Pages 631−640. April, 1984.
Details about Criteria for metrisability | BibTeX data for Criteria for metrisability | Link to Criteria for metrisability
-
[4]
A theory of communicating sequential processes
A. W. Roscoe‚ S.D. Brookes and C.A.R. Hoare
In Journal of the ACM. No. 3. Pages 560–599. July, 1984.
Details about A theory of communicating sequential processes | BibTeX data for A theory of communicating sequential processes | Download (pdf) of A theory of communicating sequential processes
-
[5]
Programs as executable predicates
A. W. Roscoe and C.A.R. Hoare
In Proceedings of FGCS84 (ICOT‚ editors). Pages 220–228. 1984.
Details about Programs as executable predicates | BibTeX data for Programs as executable predicates | Download (pdf) of Programs as executable predicates
-
[6]
Continuous analogues of axiomatised digital surfaces
A. W. Roscoe and T.Y. Kong
In Computer Vision‚ Graphics and Image Processing. No. 29. Pages 60–86. January, 1985.
Details about Continuous analogues of axiomatised digital surfaces | BibTeX data for Continuous analogues of axiomatised digital surfaces | Download (pdf) of Continuous analogues of axiomatised digital surfaces
-
[7]
A lattice of conditions on topological spaces
A. W. Roscoe‚ P.J. Collins‚ G.M. Reed and M.E. Rudin
In Proc. Amer. Math. Soc.. No. 94. Pages 487–496. July, 1985.
Details about A lattice of conditions on topological spaces | BibTeX data for A lattice of conditions on topological spaces | Link to A lattice of conditions on topological spaces
-
[8]
Proceedings of the Pittsburgh seminar on concurrency
A. W. Roscoe‚ S.D. Brookes and G. Winskel, editors
Details about Proceedings of the Pittsburgh seminar on concurrency | BibTeX data for Proceedings of the Pittsburgh seminar on concurrency | Link to Proceedings of the Pittsburgh seminar on concurrency
-
[9]
An improved failures model for communicating processes
A. W. Roscoe and S.D. Brookes
In Proceedings of the Pittsburgh seminar on concurrency. No. 197. Pages 281–305. Springer. 1985.
Details about An improved failures model for communicating processes | BibTeX data for An improved failures model for communicating processes | Download (pdf) of An improved failures model for communicating processes
-
[10]
Denotational semantics for occam
A. W. Roscoe
In Proceedings of the Pittsburgh seminar on concurrency. No. 197. Pages 306–329. Springer. 1985.
Details about Denotational semantics for occam | BibTeX data for Denotational semantics for occam | Download (pdf) of Denotational semantics for occam
-
[11]
Deadlock analysis in networks of communicating processes
A. W. Roscoe and S.D. Brookes
In K.R. Apt, editor, Logics and Models of Concurrent Systems. Vol. 13 of NATO ASI series F. Pages 305–324. Springer. 1985.
Details about Deadlock analysis in networks of communicating processes | BibTeX data for Deadlock analysis in networks of communicating processes
-
[12]
Characterisations of simply−connected finite polyhedra in 3−space
A. W. Roscoe and T.Y. Kong
In Bull. London Math. Soc.. No. 17. Pages 575–578. November, 1985.
Details about Characterisations of simply−connected finite polyhedra in 3−space | BibTeX data for Characterisations of simply−connected finite polyhedra in 3−space | Download (pdf) of Characterisations of simply−connected finite polyhedra in 3−space
-
[13]
A theory of binary digital pictures
A. W. Roscoe and T.Y. Kong
In Computer Vision‚ Graphics and Image Processing. No. 32. Pages 221–243. November, 1985.
Details about A theory of binary digital pictures | BibTeX data for A theory of binary digital pictures | Download (pdf) of A theory of binary digital pictures
-
[14]
Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification
A. W. Roscoe
In B.T. Denvir et al, editor, The Analysis of Concurrent Systems. No. 207. Pages 103–109. Springer. 1985.
Details about Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification | BibTeX data for Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification | Download (pdf) of Specifying problem one using the failures model for CSP and deriving CSP processes which meet this specification
-
[15]
A CSP solution to the trains problem
A. W. Roscoe
In B.T. Denvir et al, editor, The Analysis of Concurrent Systems. No. 207. Pages 384–388. Springer. 1985.
Details about A CSP solution to the trains problem | BibTeX data for A CSP solution to the trains problem | Download (pdf) of A CSP solution to the trains problem
-
[16]
Local symmetry and triangle laws are sufficient for metrisability
A. W. Roscoe and P.J. Collins
In Colloquia Mathematica Societatis Janos Bolyai 41. Pages 177–181. 1985.
Details about Local symmetry and triangle laws are sufficient for metrisability | BibTeX data for Local symmetry and triangle laws are sufficient for metrisability | Download (pdf) of Local symmetry and triangle laws are sufficient for metrisability
-
[17]
A timed model for communicating sequential processes
A. W. Roscoe and G.M. Reed
In Theoretical Computer Science. Vol. 58. Pages 249–261. 1988.
Details about A timed model for communicating sequential processes | BibTeX data for A timed model for communicating sequential processes | Download (pdf) of A timed model for communicating sequential processes
-
[18]
The pursuit of deadlock freedom
A. W. Roscoe and Naiem Dathi
In Information and Computation. Vol. 75. No. 3. Pages 289–327. December, 1987.
Details about The pursuit of deadlock freedom | BibTeX data for The pursuit of deadlock freedom | Link to The pursuit of deadlock freedom
-
[19]
Metric spaces as models for real−time concurrency
A. W. Roscoe and G.M. Reed
In Main et al, editor, Proceedings of the Third Workshop on the Mathematical Foundations of Programming Language Semantics (New Orleans‚ 1987). No. 298. Pages 331–343. Springer. 1988.
Details about Metric spaces as models for real−time concurrency | BibTeX data for Metric spaces as models for real−time concurrency | Download (pdf) of Metric spaces as models for real−time concurrency
-
[20]
Laws of programming
A. W. Roscoe‚ C.A.R. Hoare‚ He Jifeng‚ I.J. Hayes‚ C.C. Morgan‚ J.W. Sanders‚ I.H. Sorensen‚ J.M. Spivey and B.A. Sufrin
In Communications of the ACM. Vol. 30. No. 8. Pages 672–686. August, 1987.
Previously appeared as Oxford University Computing Laboratory Technical Report PRG−42.
Details about Laws of programming | BibTeX data for Laws of programming | Download (pdf) of Laws of programming
-
[21]
Routing messages through networks: an exercise in deadlock avoidance
A. W. Roscoe
In Muntean et al., editor, Programming of Transputer Based Machines: Proceedings of 7th occam User Group Technical Meeting. Amsterdam. 1987. IOS B.V..
Details about Routing messages through networks: an exercise in deadlock avoidance | BibTeX data for Routing messages through networks: an exercise in deadlock avoidance | Link to Routing messages through networks: an exercise in deadlock avoidance
-
[22]
Transforming occam programs
A. W. Roscoe and M.H. Goldsmith
In The Design and Application of Parallel Digital Processors. No. 298. 1988.
Details about Transforming occam programs | BibTeX data for Transforming occam programs | Download (pdf) of Transforming occam programs
-
[23]
A timed model for communicating sequential processes
A. W. Roscoe and G.M. Reed
In Proc.ICALP 86. No. 226. Pages 314–323. Springer. 1986.
Details about A timed model for communicating sequential processes | BibTeX data for A timed model for communicating sequential processes | Download (pdf) of A timed model for communicating sequential processes
-
[24]
The laws of occam programming
A. W. Roscoe and C.A.R. Hoare
In Theoretical Computer Science. Vol. 60. Pages 177–229. 1988.
Previously appeared as Oxford University Computing Laboratory Technical Report PRG−53‚ 1986.
Details about The laws of occam programming | BibTeX data for The laws of occam programming | Download (pdf) of The laws of occam programming
-
[25]
The decomposition of a rectangle into rectangles of minimal perimeter
A. W. Roscoe‚ T.Y. Kong and D.M. Mount
No. CAR−TR−169. University of Maryland Center for Automation Research. 1986.
Also SIAM Journal of Computing 17‚ 6 pp1215−1231.
Details about The decomposition of a rectangle into rectangles of minimal perimeter | BibTeX data for The decomposition of a rectangle into rectangles of minimal perimeter | Download (pdf) of The decomposition of a rectangle into rectangles of minimal perimeter
-
[26]
An Operational Semantics for CSP
A. W. Roscoe‚ S. D. Brookes and D. J. Walker
Oxford University Computing Laboratory. 1986.
Details about An Operational Semantics for CSP | BibTeX data for An Operational Semantics for CSP | Link to An Operational Semantics for CSP
-
[27]
An alternative order for the failures model
A. W. Roscoe
No. PRG−67. Oxford University Computing Laboratory. July, 1988.
in Two papers on CSP‚ Also appeared in Journal of Logic and Computation 2‚ 5 pp557−577
Details about An alternative order for the failures model | BibTeX data for An alternative order for the failures model | Link to An alternative order for the failures model
-
[28]
Unbounded nondeterminism in CSP
A. W. Roscoe
No. PRG−67. Oxford University Computing Laboratory. July, 1988.
in Two papers on CSP‚ Also appeared in Journal of Logic and Computation‚ Vol 3‚ No 2 pp131−172 (1993)
Details about Unbounded nondeterminism in CSP | BibTeX data for Unbounded nondeterminism in CSP | Link to Unbounded nondeterminism in CSP
-
[29]
Unbounded nondeterminism in CSP
A. W. Roscoe and G.Barrett
In Proceedings of MFPS89. No. 298. Springer. 1989.
Details about Unbounded nondeterminism in CSP | BibTeX data for Unbounded nondeterminism in CSP | Download (pdf) of Unbounded nondeterminism in CSP
-
[30]
Deadlock analysis in networks of communicating processes
A. W. Roscoe and S.D. Brookes
In Distributed Computing. No. 4. Pages 209–230. 1991.
Details about Deadlock analysis in networks of communicating processes | BibTeX data for Deadlock analysis in networks of communicating processes | Download (pdf) of Deadlock analysis in networks of communicating processes
-
[31]
A lattice of conditions on topological spaces II
A. W. Roscoe‚ P. Moody‚ G.M. Reed and P.J. Collins
In Fundamenta Mathematicae. No. 138. Pages 69–81. 1991.
Details about A lattice of conditions on topological spaces II | BibTeX data for A lattice of conditions on topological spaces II | Download (pdf) of A lattice of conditions on topological spaces II
-
[32]
The point−countable base problem
A. W. Rosoce‚ P.J. Collins and G.M. Reed
In G.M. Reed and J. van Mill, editors, Problems in Topology. Elsevier. 1990.
Details about The point−countable base problem | BibTeX data for The point−countable base problem | Download (pdf) of The point−countable base problem
-
[33]
Maintaining consistency in distributed databases
A. W. Roscoe
No. PRG−87. Oxford University Computing Laboratory. 1990.
Details about Maintaining consistency in distributed databases | BibTeX data for Maintaining consistency in distributed databases | Link to Maintaining consistency in distributed databases
-
[34]
Communication and correctness in Timed CSP
A. W. Roscoe‚ S.A. Schneider‚ J.W. Davies‚ D.M. Jackson and G.M. Reed
Esprit SPEC project. 1990.
Details about Communication and correctness in Timed CSP | BibTeX data for Communication and correctness in Timed CSP
-
[35]
A temporal logic for Timed CSP
D.M. Jackson‚ J.W. Davies‚ G.M. Reed and S.A. Schneider
Esprit SPEC project. 1990.
Details about A temporal logic for Timed CSP | BibTeX data for A temporal logic for Timed CSP
-
[36]
Topology‚ computer science and the mathematics of convergence
A. W. Roscoe
In G.M. Reed‚ A. W. Roscoe and R.F. Wachter, editors, Topology and Category Theory in Computer Science. OUP. 1991.
Details about Topology‚ computer science and the mathematics of convergence | BibTeX data for Topology‚ computer science and the mathematics of convergence | Link to Topology‚ computer science and the mathematics of convergence
-
[37]
Topology and category theory in computer science
A. W. Roscoe‚ G.M. Reed and R.F. Wachter, editors
proceedings of a special session at the 1989 Oxford Topology Conference
Details about Topology and category theory in computer science | BibTeX data for Topology and category theory in computer science
-
[38]
Analysing TM_FS: a study of nondeterminism in real−time concurrency
A. W. Roscoe and G.M. Reed
In Concurrency: Theory Language and Architecture. Vol. 491. 1991.
Details about Analysing TM_FS: a study of nondeterminism in real−time concurrency | BibTeX data for Analysing TM_FS: a study of nondeterminism in real−time concurrency | Link to Analysing TM_FS: a study of nondeterminism in real−time concurrency
-
[39]
CSP and timewise refinement
A. W. Roscoe‚ G. M. Reed and S. A. Schneider
In Proceedings of the BCS−FACS Refinement Workshop. LNCS. 1991.
Details about CSP and timewise refinement | BibTeX data for CSP and timewise refinement
-
[40]
Star covering properties
A. W. Roscoe‚ E.K. van Douwen‚ G.M. Reed and I.J. Tree
In Topology and its Applications. Vol. 39. Pages 71−103. 1991.
Details about Star covering properties | BibTeX data for Star covering properties | Download (pdf) of Star covering properties
-
[41]
Formal methods in the development of the H1 Transputer
A. W. Roscoe‚ A.D.B. Cox‚ M.H. Goldsmith and J.B. Scattergood
In Proceedings of Transputing 91. IOS. 1991.
Details about Formal methods in the development of the H1 Transputer | BibTeX data for Formal methods in the development of the H1 Transputer
-
[42]
Concepts of digital topology
A. W. Roscoe and T.Y. Kong
In Topology and its applications. Vol. 46. Pages 219–262. 1992.
Details about Concepts of digital topology | BibTeX data for Concepts of digital topology | Download (pdf) of Concepts of digital topology
-
[43]
Timed CSP: theory and practice
A. W. Roscoe‚ J.Davies‚ D.Jackson‚ G.M.Reed‚ J.Reed and S.A. Schneider
In Proceedings of REX Workshop. Vol. 600. LNCS. 1992.
Details about Timed CSP: theory and practice | BibTeX data for Timed CSP: theory and practice
-
[44]
Acyclic monotone normality
A. W. Roscoe and P. Moody
In Topology and its Applications. Vol. 47. Pages 53−67. 1992.
Details about Acyclic monotone normality | BibTeX data for Acyclic monotone normality | Download (pdf) of Acyclic monotone normality
-
[45]
Occam in the specification and verification of microprocessors
A. W. Roscoe
In Phil Trans R. Soc. Lond A. Vol. 339. Pages 137−151. 1992.
Also in Mechanised Reasoning and Hardware Design‚ M.J.C. Gordon and C.A.R. Hoare‚ eds (Prentice−Hall‚ 1992)‚ extended version available at http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/45ex.ps
Details about Occam in the specification and verification of microprocessors | BibTeX data for Occam in the specification and verification of microprocessors | Link to Occam in the specification and verification of microprocessors
-
[46]
A semantic model for occam II
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
In Proceedings of Transputing. Vol. 93. 1991.
Details about A semantic model for occam II | BibTeX data for A semantic model for occam II
-
[47]
Denotational semantics for occam II
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
No. PRG−108. Oxford University Computing Laboratory. 1993.
Details about Denotational semantics for occam II | BibTeX data for Denotational semantics for occam II | Download (pdf) of Denotational semantics for occam II
-
[48]
Developing and verifying protocols in CSP
A. W. Roscoe
In Proceedings of Mierlo workshop on protocols. TU Eindhoven. 1993.
Details about Developing and verifying protocols in CSP | BibTeX data for Developing and verifying protocols in CSP
-
[49]
Fixed points without completeness
A. W. Roscoe‚ M.W. Mislove and S.A. Schneider
In Theoretical Computer Science. Vol. 138. Chapter 2. Pages 273–314. 1993.
Details about Fixed points without completeness | BibTeX data for Fixed points without completeness
-
[50]
Model−checking CSP
A. W. Roscoe
In A Classical Mind: essays in Honour of C.A.R. Hoare. Chapter 21. Prentice−Hall. 1994.
Details about Model−checking CSP | BibTeX data for Model−checking CSP | Link to Model−checking CSP
-
[51]
A Classical Mind: essays in Honour of C.A.R. Hoare
A. W. Roscoe, editor
Prentice−Hall. 1994.
Details about A Classical Mind: essays in Honour of C.A.R. Hoare | BibTeX data for A Classical Mind: essays in Honour of C.A.R. Hoare
-
[52]
Denotational semantics for occam2‚ Part 1
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
In Transputer Communications. Vol. 1 of 2. Pages 65–91. 1994.
Details about Denotational semantics for occam2‚ Part 1 | BibTeX data for Denotational semantics for occam2‚ Part 1
-
[53]
Denotational semantics for occam2‚ Part 2
A. W. Roscoe‚ M.H. Goldsmith and B.G.O. Scott
In Transputer Communications. Vol. 2 of 1. Pages 25–67. 1994.
Details about Denotational semantics for occam2‚ Part 2 | BibTeX data for Denotational semantics for occam2‚ Part 2
-
[54]
Non−interference through determinism
A. W. Roscoe‚ J.C.P. Woodcock and L. Wulf
In Proceedings of ESORICS 94. 1994.
Details about Non−interference through determinism | BibTeX data for Non−interference through determinism | Download (pdf) of Non−interference through determinism
-
[55]
Non−interference through determinism
A. W. Roscoe‚ J.C.P. Woodcock and L. Wulf
In Journal of Computer Security. Vol. 4 of 1. Pages 27–54. 1996.
revised version of above
Details about Non−interference through determinism | BibTeX data for Non−interference through determinism | Download (pdf) of Non−interference through determinism
-
[56]
CSP and determinism in security modelling
1996
In Proceedings of 1995 IEEE Symposium on Security and Privacy. IEEE Computer Society Press. 1996.
Details about CSP and determinism in security modelling | BibTeX data for CSP and determinism in security modelling | Link to CSP and determinism in security modelling
-
[57]
Composing and decomposing systems under security properties
A. W. Roscoe and L. Wulf
In Proceedings of 1995 IEEE Computer Security Foundations Workshop. IEEE Computer Society Press. 1995.
Details about Composing and decomposing systems under security properties | BibTeX data for Composing and decomposing systems under security properties | Link to Composing and decomposing systems under security properties
-
[58]
Modelling and verifying key−exchange protocols using CSP and FDR
A. W. Roscoe
In Proceedings of 1995 IEEE Computer Security Foundations Workshop. IEEE Computer Society Press. 1995.
Details about Modelling and verifying key−exchange protocols using CSP and FDR | BibTeX data for Modelling and verifying key−exchange protocols using CSP and FDR | Link to Modelling and verifying key−exchange protocols using CSP and FDR
-
[59]
Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock
A. W. Roscoe‚ D.M.Jackson P.H.B. Gardiner M.H. Goldsmith J.R. Hulance and J.B. Scattergood
In Proceedings of TACAS 1995. BRICS. 1995.
also revised in a version of these proceedings published by LNCS
Details about Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock | BibTeX data for Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock | Download (pdf) of Hierarchical compression for model−checking CSP‚ or How to check 10^20 dining philosophers for deadlock
-
[60]
The timed failures−stability model for Timed CSP
A. W. Roscoe and G.M. Reed
No. PRG−119. Oxford University Computing Laboratory. 1996.
also appeared in Theoretical Computer Science‚ Vol 211 (1999)
Details about The timed failures−stability model for Timed CSP | BibTeX data for The timed failures−stability model for Timed CSP | Download (pdf) of The timed failures