Richard Banach: Some recent journal publications

Most of these are held in the directory http://www.cs.man.ac.uk/~banach/some.pubs (refered to below as . . .) in both ps.gz and pdf forms.

Note that the ps.gz and pdf forms can differ slightly in inessential formatting detail due to the pdf having been produced using later releases of the document processing software in some cases, and/or ps2pdf vagaries.

Last Updated: 08.08.11


Academic Journal Papers

R. Banach, M. Bozzano  34pp.,
Form. Asp. Comp.,  (to appear),
`The Mechanical Generation of Fault Trees for Reactive Systems
via Retrenchment I: Combinational Circuits.'
Preprint: .../Retrench.FT.ReaSys.I.Comb.ps.gz  .../Retrench.FT.ReaSys.I.Comb.pdf

R. Banach, M. Bozzano  49pp.,
Form. Asp. Comp.,  (to appear),
`The Mechanical Generation of Fault Trees for Reactive Systems
via Retrenchment II: Clocked and Feedback Circuits.'
Preprint: .../Retrench.FT.ReaSys.II.TimCy.ps.gz  .../Retrench.FT.ReaSys.II.TimCy.pdf

R. Banach, C. Jeske, A. Hall, S. Stepney  26pp.,
Form. Asp. Comp.,  (to appear),
`Atomicity Failure and the Retrenchment Atomicity Pattern.'
Preprint: .../Retrench.At.Fail.At.Patt.ps.gz  .../Retrench.At.Fail.At.Patt.pdf

R. Banach, C. Jeske 2011
J. Log. Alg. Prog.,  80,  453-480,
`Simple Feature Engineering via Neat Default Retrenchments.'
Preprint: .../Retrench.Feature.ps.gz  .../Retrench.Feature.pdf

R. Banach  2011
Form. Asp. Comp.,  23,  113-131,
`Retrenchment for Event-B: UseCase-wise Development and Rodin Integration.'
Preprint: .../Retrench.EventB.UC.ps.gz  .../Retrench.EventB.UC.pdf

R. Banach, C. Jeske  2010
J. Log. Alg. Prog.,  79,  215-232,
`Stronger Compositions for Retrenchments.'
Preprint: .../Retrench.Strong.Comp.ps.gz  .../Retrench.Strong.Comp.pdf
Preprint including full proofs: .../Retrench.Strong.Comp.FULL.ps.gz  .../Retrench.Strong.Comp.FULL.pdf

R. Banach, G. Schellhorn  2010
Form. Asp. Comp.,  22,  33-61,
`Atomic Actions and their Refinements to Isolated Protocols.'
Preprint: .../Refine.At.Act.Prot.ps.gz  .../Refine.At.Act.Prot.pdf

R. Banach, C. Jeske, M. Poppleton  2008
J. Log. Alg. Prog.,  75,  209-229,
`Composition Mechanisms for Retrenchment.'
Preprint: .../Retrench.Composition.ps.gz  .../Retrench.Composition.pdf

R. Banach, M. Poppleton, C. Jeske, S. Stepney  2007
Sci. Comp. Prog.,  67,  301-329,
`Engineering and Theoretical Underpinnings of Retrenchment.'
Preprint: .../Retrench.Underpin.ps.gz  .../Retrench.Underpin.pdf

R. Banach, C. Jeske, M. Poppleton, S. Stepney  2007
Fund. Inf.,  77,  29-69,
`Retrenching the Purse: The Balance Enquiry Quandary,
and Generalised and (1,1) Forward Refinements.'
Preprint: .../Retrench.Mondex.Bal.ps.gz  .../Retrench.Mondex.Bal.pdf

R. Banach, J-P. Bodeveix, M. Filali, M. Poppleton  2005
Ann. Math., Comp. and Teleinf.,  1,  18-26,
`Dynamic Aspects of Retrenchments through Temporal Logic.'
Preprint: .../Retrench.Dyn.Asp.TL.ACMT.ps.gz  .../Retrench.Dyn.Asp.TL.ACMT.pdf

R. Banach, M. Poppleton  2003
Req. Eng. J.,  8,  266-288,
`Retrenching Partial Requirements into System Definitions:
A Simple Feature Interaction Case Study.'
Preprint: .../Retrench.Partial.Req.ps.gz  .../Retrench.Partial.Req.pdf

R. Banach, F. Arbab, G.A. Papadopoulos, J.R.W. Glauert  2003   
J. Univ. Comp. Sci.,  9,  2-33,
`A Multiply Hierarchical Automaton Semantics for the IWIM Coordination Model.'
http://www.iicm.edu/jucs
Preprint: .../IWIM.Medium.ps.gz  .../IWIM.Medium.pdf

R. Banach, M. Poppleton  1999
Form. Asp. Comp.,  11,  498-540,
`Sharp Retrenchment, Modulated Refinement, and Simulation.'
Preprint: .../Sharp.Retrench.ps.gz  .../Sharp.Retrench.pdf

R. Banach  1997
J. Univ. Comp. Sci.,  3,  1283-1336,
`MONSTR V --- Transitive Coercing Semantics and the Church-Rosser Property.'
http://www.iicm.edu/jucs
Preprint: .../MONSTR-V.ps.gz  .../MONSTR-V.pdf

R. Banach, G.A. Papadopoulos  1997
J. Prog. Lang.,  5,  201-231,
`A Study of Two Graph Rewriting Formalisms: Interaction Nets and MONSTR.'
http://www.chapmanhall.com/jp/
Preprint: .../Study.IN.MONSTR.ps.gz  .../Study.IN.MONSTR.pdf

R. Banach  1997
J. Univ. Comp. Sci.,  3,  755-801,
`MONSTR II --- Suspending Semantics and Independence.'
http://www.iicm.edu/jucs
Preprint: .../MONSTR-II.ps.gz  .../MONSTR-II.pdf

R. Banach  1996
Inf. Proc. Lett.,  60,  109-114,
`Transitive Term Graph Rewriting.'
Preprint: .../Trans.TGR.ps.gz  .../Trans.TGR.pdf

R. Banach  1996
J. Univ. Comp. Sci.,  2,  164-216,
`MONSTR I --- Fundamental Issues and the Design of MONSTR.'
http://www.iicm.edu/jucs
Preprint: .../MONSTR-I.ps.gz  .../MONSTR-I.pdf
(Corrigendum: Vol. 2 No. 12)
.../MONSTR-I.corr.ps.gz  .../MONSTR-I.corr.pdf

R. Banach  1995
Sci. Comp. Prog.,  24,  221-248,
`On Regularity in Software Design.'
Preprint: .../Regularity.Sw.Des.ps.gz  .../Regularity.Sw.Des.pdf

R. Banach  1995
Theor. Comp. Sci.,  152,  305-320,
`Locating the Contractum in the Double Pushout Approach.'

R. Banach, J. Balazs, G.A. Papadopoulos  1995
J. Univ. Comp. Sci., 1, 335-394,
`A Translation of the Pi-Calculus into MONSTR.'
http://www.iicm.edu/jucs
Preprint: .../Pi.MONSTR.ps.gz  .../Pi.MONSTR.pdf

R. Banach  1995
Ann. Pure App. Logic,  73,  277-295,
`Sequent Reconstruction in LLM: A Sweepline Proof.'

R. Banach  1994
Theor. Comp. Sci.,  131,  29-94,  Fundamental Study, 
`Term Graph Rewriting and Garbage Collection Using Opfibrations.'

R. Banach  1994
Theor. Comp. Sci.,  129,  187-192,
`Regular Relations and Bicartesian Squares.'

R. Banach  1993
J. Pure App. Alg.,  86,  7-22,
`Weak Fibrations.'