%----------------------------------------------------------------------


@string{AI="Acta Informatica"}
@string{AP="Academic Press"}
@string{CACM="Communications of the ACM"}
@string{CUP="Cambridge University Press"}
@string{FAC="Formal Aspects of Computing"}
@string{IC="Information and Computation"}
@string{IPL="Information Processing Letters"}
@string{JAR="J. Automated Reasoning"}
@string{JCSS="J. Computer and System Sciences"}
@string{JFP="J. Functional Programming"}
@string{JSC="J. Symbolic Computation"}
@string{JSL="J. Symbolic Logic"}
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
%@string{LNCS="LNCS"}
@string{LNAI="Lect.\ Notes in Art.\ Int."}
@string{OUP="Oxford University Press"}
@string{MIT="MIT Press"}
@string{PH="Prentice-Hall"}
@string{SCP="Science of Computer Programming"}
@string{Springer="Springer-Verlag"}
%@string{Springer="Springer"}
@string{TCS="Theoretical Computer Science"}
@string{TOPLAS="ACM Trans.\ Programming Languages and Systems"}


@inproceedings{Ortner-Schirmer-TPHOL05,
author={Veronika Ortner and Norbert Schirmer},
title={Verification of {BDD} Normalization},
pages={261--277},
crossref={TPHOL05}
}


@Proceedings{TPHOL05,
  editor={J. Hurd and T. Melham},
  title={Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005},
 booktitle={Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005},
  publisher=Springer,
  series=LNCS,
  volume=3603,
  year=2005,
}