An object-oriented dynamic logic with updates

@MASTERSTHESIS{Platzer_2004b,
	%pdf = {logic/Diplomath.pdf},
	%slides = {pub/odl-slides.pdf},
	%ref = {DBLP:conf/cade/BeckertP06},
	%refname = {IJCAR'06},

  author    = {Andr{\'e} Platzer},
  title     = {An Object-oriented Dynamic Logic with
               Updates},
  school    = {University of Karlsruhe, Department of
               Computer Science. Institute for Logic,
               Complexity and Deduction Systems},
  year      = {2004},
  month  = {Sep},
  pages     = {193},
  abstract  = {
    With the goal of this thesis being to create a dynamic
    logic for object-oriented languages, ODL is developed
    along with a sound and relatively complete calculus.
    The dynamic logic contains only the absolute logical
    essentials of object-orientation, yet still allows a
    ``natural'' representation of all other features of
    common object-oriented programming languages. ODL is an
    extension of a dynamic logic for imperative While
    programs by function modification and dynamic type
    checks. A generalisation of substitutions, called
    updates, constitute the central technical device for
    dealing with object aliasing arising from function
    modification and for retaining a manageable calculus in
    practical application scenarios. Further, object
    enumerators realise object creation in a natural yet
    powerful way. Finally, completeness is proven relative
    to first-order arithmetic. Along with the soundness
    result, this proof constitutes the central part of this
    thesis and even copes with states containing
    uncomputable functions.},
  pdf = {http://i12www.ira.uka.de/~key/doc/2004/odlMasterThesis.pdf},
  slides="pub/odl-slides.pdf",
  ref="DBLP:conf/cade/BeckertP06",
  refname="IJCAR'06",
}```