@string(AAAI="American Association for Artificial Intelligence")

@string(AAAIM="The AI Magazine")

@string(ACM="Association for Computing Machinery")

@string(ACMTOPLAS="Journal of Transactions on Programming Languages and Systems")

@string(AI="Artificial Intelligence")

@string(AIAI="Artificial Intelligence Applications Institute, Edinburgh")

@string(AISB="Society for the Study of

Artificial Intelligence and Simulation of Behaviour")

@string(ASE="Automated Software Engineering")

@string(CACM="Communications of the Association for Computing Machinery")

@string(CADE5="5th International Conference on Automated Deduction")

@string(CADE6="6th International Conference on Automated Deduction")

@string(CADE8="8th International Conference on Automated Deduction")

@string(CADE9="9th International Conference on Automated Deduction")

@string(CADE11="11th International Conference on Automated Deduction")

@string(CADE12="12th International Conference on Automated Deduction")

@string(CADE13="13th International Conference on Automated Deduction")

@string(CADE14="14th International Conference on Automated Deduction")

@string(CADE15="15th International Conference on Automated Deduction")

@string(CADE16="16th International Conference on Automated Deduction")

@string(CMU="Carnegie-Mellon University")

@string(CUP="Cambridge University Press")

@string(DAI="Dept.\ of Artificial Intelligence, University of Edinburgh")

@string(HCRC="Human Communication Research Centre, University of Edinburgh")

@string(ECAI="European Conference on Artificial Intelligence")

@string(EUP="Edinburgh University Press")

@string(IJCAI="International Joint Conference on Artificial Intelligence")

@string(IRIA="Institut de Recherche d'Informatique et d'Automatique")

@string(JACM="Journal of the Association for Computing Machinery")

@string(JAR="Journal of Automated Reasoning")

@string(JCSS="Journal of Computer and System Sciences")

@string(JLC="Journal of Logic and Computation")

@string(JLP="Journal of Logic Programming")

@string(JSL="Journal of Symbolic Logic")

@string(JSC="Journal of Symbolic Computation")

@string(LFCS="Laboratory for Foundations of Computer Science, University of Edinburgh")

@string(LNAI="Lecture Notes in Artificial Intelligence")

@string(LNCS="Lecture Notes in Computer Science")

@string(JAIR="Journal of Artificial Intelligence Research")

@string(MIT="The MIT Press")

@string(OUP="Oxford University Press")

@string(SPE="Software - Practice and Experience")

@string(TCS="Journal of Theoretical Computer Science")

@string(TODS="ACM Transactions on Database Systems")

@string{ RWTH = "Rheinisch Westf{\accent127 a}lische Technische

Hoch\-schule" }

@string{ RWTHLDFM = "Lehrstuhl D f{\accent127 u}r Mathematik,

Rheinisch Westf{\accent127 a}lische Technische

Hoch\-schule" }

@string{ RWTH-A = "Aachen, Germany" }

@comment{Marker for AAAaaa}

@techreport(KiebPl,

author = "Kieburtz, R.",

title = "P-logic: property verification for Haskell programs",

institution = "OGI",

year = 2002

)

@techreport(PTeam,

author = "The Programatica Team",

title = "Programatica tools for certifiable, auditable development of high-assurance systems in {H}askell",

institution = "OGI",

year = 2000

)

@article{holcf,

author = {Mueller, O. and Nipkow, T. and von Oheimb, D. and Slotosch, O.},

title = {{HOLCF} = {HOL} + {LCF}},

journal = {Journal of Functional Programming},

year = {1999}

}

@article{abram93,

author = {Abramsky, S.},

title = {Computational interpretation of linear logic},

journal = {Theoretical Computer Science},

year = {1993},

volume = {111}

}

@inproceedings(barber,

author = "Barber, A. and Gardner, P. and Hasegawa, M. and Plotkin, G.",

title = "From linear logic to action calculi",

booktitle = "CSL 97",

publisher = "Springer",

pages = "78--97",

year = 1997

)

@inproceedings(fleuriot,

author = "Fleuriot, J. D.",

title = "On the mechanisation of real analysis in {I}sabelle-{HOL}",

booktitle = "TPHOL 2000",

series = "LNCS",

number = "1869",

publisher = "Springer",

pages = "146--162",

year = 2000

)

@InProceedings{Stell97a,

author = {Stell, J. G. and Worboys, M. F.},

title = {The Algebraic Structure of Sets of Regions},

booktitle = {Proceedings of {COSIT'97} },

editor = {Stephen C. Hirtle and Andrew U. Frank},

volume = 1329,

series = {LNCS},

year = 1997,

publisher = {Springer},

pages = {163--174}

}

@inproceedings(TillHet,

author = "Mossakowski, T.",

title = "Heterogeneous theories and the heterogeneous tool set",

booktitle = "Semantic Interoperability and Integration",

publisher = "IBFI, Dagstuhl",

editor = "Kalfoglou, Y. and Schorlemmer, M. and Sheth, A. and Staab, S. and Uschold, M.",

year = 2005

)

@inproceedings(alur97,

author = "Alur, R. and Henzinger, T. A.",

title = "Modularity for timed and hybrid systems",

booktitle = "CONCUR 97",

publisher = "Springer Verlag",

year = 1997

)

@book{ksrm,

author = {Freitas, R. A. and Merkle, R. C.},

title = {Kinematic Self-Replicating Machines},

publisher = {Landes Bioscience},

year = {2004}

}

@book{manna95,

author = {Manna, Z. and Pnueli, A.},

title = {Temporal verification of reactive systems},

publisher = {Springer Verlag},

year = {1995}

}

@book{gould96,

author = {Gould, H. and Tobochnik, J.},

title = {Introduction to computer simulation methods},

publisher = {Addison-Wesley},

year = {1996}

}

@book{lakh04,

author = {Lakhtakia, A.},

title = {Handbook of

nanotechnology: nanometer structure theory, modeling, and simulation},

publisher = {ASME},

year = {2004}

}

@manuscript(feynman,

author = "Feynman, R. P",

title = "There's pleny of room at the bottom",

institution = "California Institute of Technology",

year = 1959

)

@article{drexler99,

author = {Drexler, K. E.},

title = {Building molecular machine systems},

journal = {Trends in Biotechnology},

volume = {17},

year = {1999}

}

@article{chao91,

author = {Chaochen, Z. and Hoare, C. A. R. and Ravn, A. P.},

title = {A calculus of durations},

journal = {Information processing letter},

volume = {40},

number= {5},

pages= {269--276},

year = {1991}

}

@article{ecell,

author = {Tomita, M. and Kenta, H. and Takahashi, K. and Shimuzu, T. S. and Matzuzaki, Y. and Saito, K. and Tanida, S. and Yugi, K. and Venter, J. C. and Hutchison, C. A.},

title = {E-{CELL}: software environment for whole-cell simulation},

journal = {Bioinformatics},

volume = {7},

pages = {72--84},

year = {1999}

}

@phdthesis{slot97,

author = {Slotosch, O.},

title = {Refinment in

HOLCF: implementation of reactive systems, {P}h{D} thesis},

year = {1997} }

@article{drexler94,

author = {Drexler, K. E.},

title = {Molecular machines: physical principles and implementation strategies},

journal = {Annual Review of Biophysics and Biomolecular Structures},

volume = {23},

pages = {337--405},

year = {1994}

}

@article{manna-wald,

author = {Manna, Z. and Waldinger, R.},

title = {A deductive approach to program synthesis},

journal = {{ACM} {TOPLAS}},

volume = {2},

pages = {90--121},

year = {1980}

}

@article{armando-smaill,

author = {Armando, A. and Smaill, A. and

Green, I.},

title = {Automatic synthesis of recursive programs: the

proof-planning paradigm},

journal = {Automated Software Engineering},

volume = 6,

number = 4,

pages = {329--356},

year = {1999} }

@inproceedings(PavSmith,

author = "Pavlovic, D. and Smith, D. R.",

title = "Program development by refinement",

booktitle = "10th Anniversary Colloquium of {UNU/IIST}",

pages = "267--286",

year = 2002

)

@inproceedings(shankar02,

author = "Shankar, N.",

title = "Verification by abstraction",

booktitle = "10th Anniversary Colloquium of {UNU/IIST}",

pages = "29--39",

year = 2002

)

@inproceedings{manna03,

author = "Manna, Z. and Zarba, C. G.",

title = "Combining decision procedures",

booktitle = "Formal

Methods at the Cross Roads",

publisher= "Springer",

year = "2003" }

@InProceedings(phh99,

author = "Peterson, J. and Hager, G. D. and Hudak, P.",

title = "A Language for Declarative Robotic Programming",

booktitle = "International Conference on Robotics and Automation",

year = 1999

)

@InProceedings{wan01rtfrp,

author = "Wan, Z. and Taha, W. and Hudak, P.",

title = "Real-Time {FRP}",

booktitle = "International Conference on Functional Programming

({ICFP'01})",

year = "2001"

}

@techreport(PSB,

author = "Pixley, C. and Strader, N. R. and Bruce, W. C. and Park,

J. and Kaufmann, M. and Shultz, K. and Burns, M. and Kumar, J. and

Yuan, J. and Nguyen, J.",

title = "Commercial verification: methodology and tools",

institution = "Motorola, Inc.",

type = "Research Paper",

year = 1996,

)

@article{BvHS91,

author = {Bundy, A and van Harmelen, F. and Hesketh, J. and

Smaill A.},

title = {Experiments with proof plans for

induction},

journal = {Journal of Automated Reasoning},

year = {1991}

}

@article{Atk68,

author = {Atkins, D. E.},

title = {Higher-radix division using estimates of the divisor and

partial remainders},

journal = {IEEE Transactions on Computers},

volume = {C-17, 10},

month = {October},

year = {1968}

}

@inproceedings(Pra95,

author = "Pratt, V.",

title = "Anatomy of the Pentium Bug",

booktitle = "TAPSOFT'95: Theory and Practice of Software Development",

publisher = "Springer-Verlag",

editor = "Mosses, P. D. and Nielsen, N. and Schwartxbach, M. I.",

pages = "97-107",

month = {May},

year = 1995,

)

@inproceedings(Tay81,

author = "Taylor, G. S.",

title = "Compatible hardware for division and square root",

booktitle = "Proceedings of the 5th Symposium on Computer Arithmetic",

publisher = "IEEE Computer Society Press",

pages = "127-134",

year = 1981,

)

@article{RSS,

author = {Ruess, H. and Shankar, N. and Srivas, M. K.},

title = {Modular Verification of {SRT} Division},

journal = {Formal Methods in System Design},

publisher = "Kluwer Academinc publishers",

volume = {14},

number = {1},

year = {1999}

}

@article{CGZ,

author = {Clarke, E. M. and German, S. M. and Xudong, Z.},

title = {Verifying the SRT division algorithm using theorem proving

techniques},

journal = {Formal Methods in System Design},

publisher = "Kluwer Academinc publishers",

volume = {14},

number = {1},

year = {1999}

}

@article{OZGS,

author = {O'Leary, J. and Zhao, X. and Gerth, R. and Seger,

C.-J. H.},

title = {Formally verifying IEEE compliance of floating-point hardware},

journal = {Intel Technology Journal},

volume = {Q1},

year = {1999}

}

@article{BK,

author = {Basin, D. and Klarlund, N.},

title = {Automata based symbolic reasoning in hardware verification},

journal = {Formal Methods in System Design},

publisher = "Kluwer Academinc publishers",

volume = {14},

number = {1},

year = {1999}

}

@article{irelandE04,

author = {Ireland, A. and Ellis, B. J. and Cook,A. and Chapman, R. and Barnes, J.},

title = {An integrated approach to porgram reasoning},

journal = {},

publisher = "",

volume = {},

number = {},

year = {}

}

@article{irelandS04,

author = {Ireland, A. and Stark, J.},

title = {Combining proof plans and partial order planning for imperative

program synthesis},

journal = {Journal of automated software

engineering (accepted)},

publisher = "Springer Verlag",

year = {2004}

}

@inproceedings{ellis04,

author = {Ellis, B. J. and Ireland, A.},

title = {An integration of program analysis and automated theorem proving},

booktitle = {IFM 04},

editors = {E. A. Boyten, J. Derrick, G. Smith},

publisher = "Springer Verlag",

year = {2004}

}

@inproceedings{cresswell99,

author = {Cresswell, S. and Smaill, A. and Richardson, J.},

title = {Deductive synthesis of recursive plans in linear logic},

booktitle = {Recent advances in {AI} planning, LNCS 1809},

pages = {252--264},

publisher = "Springer",

year = {1999}

}

@inproceedings{denney05,

author = {Denney, E and Fischer, B:},

title = {Certifiable program generation},

booktitle = {GPCE 05},

year = {2005}

}

@article{Rus99,

author = {Russinov, D. M.},

title = {A mechanically checked proof of correctness of the AMD K5

floating point square root microcode},

journal = {Formal Methods in System Design},

publisher = "Kluwer Academinc publishers",

volume = {14},

number = {1},

year = {1999}

}

@article{Toc58,

author = {Tocher, T. D.},

title = {Techniques of multiplication and division for automatic

binary computers},

journal = {Quart. J. Mech. App. Math.},

volume = {2, part 3},

year = {1958}

}

@article{leigh04,

author = {Hernandez, J. V. and Kay, E. R. and Leigh, D. A.},

title = {A reversible synthetic rotary molecular motor},

journal = {Science},

volume = {306:1532--1537},

year = {2004}

}

@techreport{Rob65,

author = {Robertson, T. D.},

title = {Methods of selection of quotient digits during digital division},

institution = {University of Illinois},

year = {1965}

}

@book{Mel93,

author = {Melham, T. F.},

title = {Higher order logic and hardware verification},

publisher = {Cambridge University Press},

year = {1993}

}

@book{bundy05,

author = {Bundy, A. and Basin, D. and Hutter, D. and Ireland, A.},

title = {Rippling: meta-level guidance for mathematical reasoning},

publisher = {Cambridge University Press},

year = {2005}

}

@book{Paulson94isa,

title = {Isabelle: a generic theorem prover},

author = {Paulson, L. C.},

collection = {LNCS},

volume = {828},

publisher = {Springer},

year = {1994}

}

@book{mansoori,

author = {Mansori, G. A.},

title = {Principles of nanotechnology},

publisher = {World Scientific Pub.},

year = {2005}

}

@book{Pau91,

author = {Paulson, L. C.},

title = {ML for the working programmer},

publisher = {Cambridge University Press},

year = {1991}

}

@book{Wil95,

author = {Wilson, F. A.},

title = {Understanding digital technology},

publisher = {Bernard Babani},

year = {1995}

}

@Manual(Fou88,

author = {Fourman, M. and others},

title = {Dialog reference manual},

publisher = {Abstract Hardware Ltd},

year = {1988},

)

@Manual{HSD,

author = {HOL sys.des.},

title = {The HOL system description - version 3 for HOL90.9},

publisher = {University of Cambridge - published electronically},

year = {1999}

}

@Manual{BGC,

author = {Birtwistle, B. G. and Graham, B. and Chin, S.-K.},

title = {newtheory HOL; An Introduction to Hardware

Verification in Higher Order Logic},

publisher = {published electronically},

year = {1994}

}

@Manual{holclam,

title = {The HOL/CLaM System - User's Guide, release 1.00},

author = {Boulton, R.},

year = {1998},

month = {August},

}

@book{holbook,

editor = "Gordon, M. J. C. and Melham, T. F.",

title = "Introduction to {HOL}:

A theorem proving environment for higher order logic",

publisher = "Cambridge University Press",

year = "1993"}

@InProceedings(boulton-tphols-98,

key = "Boulton @i<et. al.>",

author = "Boulton, R. and Slind, K. and Bundy, A. and Gordon,

M.",

title = "An Interface between {CLAM} and {HOL}",

booktitle = "Proceedings of the 11th International Conference on

Theorem Proving in Higher Order Logics (TPHOLs'98)",

year = 1998,

series = LNCS,

volume = 1479,

editor = "Grundy, J. and Newey, M.",

pages = "87--104",

publisher = "Springer",

address = "Canberra, Australia",

month = "September/October"

)

@article(pub567,

key = "Bundy @i<et. al.>",

author = "Bundy, A. and Stevens, A. and van Harmelen, F. and Ireland, A. and Smaill, A.",

title = "Rippling: A Heuristic for Guiding Inductive Proofs",

journal = AI,

volume = 62,

pages = "185-253",

year = 1993,

note = "Also available from Edinburgh as DAI Research Paper No. 567.")

@inproceedings(pub507,

key = "Bundy @i<et al>",

author = "Bundy, A. and van Harmelen, F. and Horn, C. and Smaill, A.",

title = "The {Oyster-Clam} system",

booktitle = "10th International Conference on Automated Deduction",

publisher = "Springer-Verlag",

editor = "Stickel, M. E.",

pages = "647-648",

year = 1990,

note = "Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.")

@article{BasinWalsh96,

author = "Basin, David and Toby Walsh",

title = "A calculus for and termination of rippling",

journal = JAR,

volume = 16,

number = "1--2",

pages = "147--180",

year = 1996

}

@inproceedings(pub828,

key = "FMCAD96",

author = "Francisco Cantu and Bundy, Alan and Smaill, Alan and

Basin, David",

title = "Experiments in Automating Hardware Verification using

Inductive Proof Planning",

booktitle = "Proceedings of the Formal Methods for Computer-Aided

Design Conference",

publisher = "Springer-Verlag",

SERIES = {Lecture Notes in Computer Science},

NUMBER = "1166",

editor = "Srivas, M. and Camilleri,A.",

pages = "94--108",

year = "1996")

@inproceedings{Leeds92a,

author = {Randell, D. A. and Cui, Z. and Cohn, A. G.},

booktitle = {Proc. 3rd Int. Conf. on

Knowledge Representation and Reasoning},

pages = {165-176},

publisher = {Morgan Kaufmann},

title = {A Spatial Logic Based on Regions and Connection},

year = {1992}

}

@Article{Bennett98constr,

author = {Bennett,B.},

title = {Determining Consistency of Topological Relations},

journal = {Constraints},

year = {1998},

month = {June},

volume = {3},

publisher = {Kluwer},

number = {{2\&3}},

pages = {213--225}

}

@article(AWE,

author = "Bortin, M. and Johnsen, E. B. and Lueth, C.",

title = "Structured Formal Development in {I}sabelle",

journal = "Nordic Journal of Computing",

type = "Research Paper",

voume = "13",

page = "1--20",

year = "2006"

)

@book{Hudak,

author = {Hudak, P.},

title = {The Haskell School of Expression},

publisher = {Cambridge University Press},

year = {2000}

}

@Manual{Hets,

author = {Mossakowski, T. and Maeder, C. and Luettich,

K. and Woelfl, S.},

title = {The {H}eterogeneous {T}ool {S}et},

publisher = {Universitaet Bremen},

year = {2003}

}

@techreport(Huff,

author = "Huffman, B. and Matthews, J. and White, P.",

title = "Axiomatic Constructor Classes in {I}sabelle-{HOLCF}",

institution = "OGI",

type = "Research Paper",

year = 2005

)

@book{HaskellRep,

title = {Haskell 98 Language and Libraries},

editor = {Peyton Jones, S.},

publisher = {Cambridge University Press},

year = {2003}

}

@techreport(HetsUG,

author = "Mossakowski, T.",

title = "Hets user guide",

institution = "Universitaet Bremen",

type = "Tutorial",

year = 2006

)

@techreport(Wenzel,

author = "Wenzel, M.",

title = "Using Axiomatic Type Classes in {I}sabelle",

institution = "TU Muenchen",

type = "Tutorial",

year = 2005

)

@habilitationthesis{MossaTh,

author = {Mossakowski, T.},

title = {Heterogeneous Specification and the Heterogeneous Tool Set, {H}abilitation {T}hesis},

year = {2005} }

@book{ThompsonB,

author = {Thompson, S.},

title = {The Craft of Functional Programming},

publisher = {Addison Wesley},

year = {1999}

}

@book{winskel,

author = "Winskel, G.",

title = "The Formal Semantics of Programming Languages",

publisher = "MIT Press", year = "1993"

}

@inproceedings{Thompson92,

author = {Thompson, S.},

booktitle = {Functional Programming},

editors = {J. Launchbury and P. M. Sansom},

publisher = {Springer},

title = {Formulating {H}askell},

year = {1992}

}

@Article{Thompson95,

author = {Thompson, S.},

title = {A Logic for {M}iranda, revisited},

journal = {Formal Aspects of Computing},

year = {1994},

volume = {3},

publisher = {BCS}

}

@Article{Thompson89,

author = {Thompson, S.},

title = {A Logic for {M}iranda},

journal = {Formal Aspects of Computing},

year = {1989},

volume = {1},

publisher = {BCS}

}

@inproceedings{Thompson95b,

author = {Hill, S. and Thompson, S.},

booktitle = {Proceedings of the first {I}sabelle users workshop},

editors = {L. C. Paulson},

publisher = {University of Cambridge Computer Laboratory},

series = {Technical Report},

number = {397},

title = {Miranda in {I}sabelle},

pages = {122--135},

year = {1995}

}

@inproceedings{Pollack,

author = {Longley, J. and Pollack, R.},

booktitle = {TPHOL 04},

editors = {K. Slind, A. Bunker, and G. Gopalakrishnan},

publisher = {Springer},

series = {LNCS},

number = {3223},

pages = {201--216},

title = {Reasoning about {C}{B}{V} programs in {I}sabelle-{H}{O}{L}},

year = {2004}

}

@inproceedings{Abel,

author = {Abel, A. and Benke, M. and Bove, A. and Hughes, J. and Norell, U.},

booktitle = {ACM-SIGPLAN 05},

editors = {},

publisher = {},

series = {},

number = {},

pages = {},

title = {Verifying {H}askell programs using constructive type theory},

year = {2005} }

@inproceedings(Lueth,

author = "Lueth, C.",

title = "Modular Modelling with Monads",

booktitle = "Methods of Category Theory in Software Engineering",

publisher = "Technische Universitaet Dresden",

year = 2005,

)

@inproceedings{Prog04,

author = {Hallgren, T. and Hook, J. and Jones, M. P. and Kieburtz, D.},

booktitle = {HCSS04},

title = {An Overview of the {P}rogramatica ToolSet},

year = {2004}

}