Subversion Repositories TPPL

Rev

Rev 61 | Blame | Compare with Previous | Last modification | View Log | RSS feed

%WN120727 not used in TPPL-formlos.tex, but in predecessors.
%
% \cite{Wenzel-11:doc-orient}.
% \cite{cafeOBJ-98}

@Article{ballarin-paulson-ca-99,
  author =       {Ballarin, C. and Paulson, L.C.},
  title =        {A pragmatic approach to extending provers by computer algebra -- with applications to coding theory},
  journal =      {Fundamenta Informaticae},
  year =         {1999},
  volume =       {39},
  number =       {1--2},
  pages =        {1--20}
}

@Article{harr:HOL-maple,
  author =       {Harrison, John and Th\`ery, Laurent},
  title =        {A sceptic's approach to combining {HOL} and {Maple}},
  journal =      {J. of Automated Reasoning},
  year =         {1998},
  volume =       {21},
  pages =        {279-294},
  pnote={},status={cited},source={calculemus00..64},location={}  
}

@InProceedings{broker-archi-01,
  author =       {Alessandro Armando and Daniele Zini},
  title =        {Interfacing Computer Algebra and Deduction Systems
via the Logic Broker Architecture},
  booktitle = {Symbolic Computation and Automated Reasoning – The CALCULEMUS-2000 Symposium},
  pages =        {49--64},
  year =         {2001},
  editor =       {Manfred Kerber and Michael Kohlhase},
  address =      {St. Andrews, UK},
  month =        {August 6--7},
  publisher = {AK Peters, Natick, MA, USA}
}

@Book{meyer-contract-09,
  author =       {Bertrand Meyer},
  title =        {Touch Of Class: Learning to Program Well with Objects and Contracts},
  publisher =    {Springer},
  year =         {2009}
}

@Article{lazard-rioboo-trager-90,
  author =       {D. Lazard and R. Rioboo},
  title =        {Integration of Rational Functions --- Rational Computa-
tion of the Logarithmic Part},
  journal =      {J. Symbolic Comp.},
  year =         {1990},
  number =       {9},
  pages =        {113--115}
}

@ARTICLE{Mulders97anote,
    author = {Thom Mulders},
    title = {A Note on Subresultants and the Lazard/Rioboo/Trager Formula in Rational Function Integration},
    journal = {J. Symbolic Comput},
    year = {1997},
    volume = {24},
    pages = {45--50}
}

@Article{risch-1st-69,
  author =       {Robert H. Risch},
  title =        {The problem of integration in finite terms},
  journal =      {Trans. Amer. Math. Soc.},
  year =         {1969},
  number =       {139},
  pages =        {167--189}
}

@Unpublished{calculemus-report-05,
  key    =       {R36},
  author =       {Christoph Benzm{\"u}ller and Corinna Hahn},
  title =        {The CALCULEMUS Final Report},
  note =         {Final report of the Marie Curie Research Training Network CALCULEMUS within the EU 5th framework},
  year =         2004,
  pages =        {1--57},
  url =          {www.ags.uni-sb.de/~chris/papers/R36.pdf}
}

@InProceedings{guarded-expr-97,
  author =       {Dolzmann, A. and Sturm, T.},
  title =        {Guarded expressions in practice},
  booktitle = {Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation},
  pages =        {376--383},
  year =         {1997},
  editor =       {K\"uchlin, W.W.},
  address =      {Maui, Hawaii, USA},
  month =        {21–23 July 1997},
  organization = {ISSAC 97},
  publisher = {ACM Press}
}

@article{Armando:2005:REM:1740741.1740840,
 author = {Armando, Alessandro and Ballarin, Clemens},
 title = {A reconstruction and extension of Maple's assume facility via constraint contextual rewriting},
 journal = {J. Symb. Comput.},
 issue_date = {May, 2005},
 volume = {39},
 number = {5},
 month = may,
 year = {2005},
 issn = {0747-7171},
 pages = {503--521},
 numpages = {19},
 url = {http://dx.doi.org/10.1016/j.jsc.2004.12.010},
 doi = {10.1016/j.jsc.2004.12.010},
 acmid = {1740840},
 publisher = {Academic Press, Inc.},
 address = {Duluth, MN, USA},
 keywords = {Combination of reasoning specialists, Computer algebra, Constraints, Contextual rewriting, Simplification},
}

@InProceedings{assume-maple-92,
  author =       {Weibel,T. and Gonnet,G.H.},
  title =        {An Assume Facility for {CAS} with a Sample Implementation for {Maple}},
  booktitle = {Proc. DISCO ’92},
  pages =        {95--103},
  year =         {1993},
  editor =       {J.P. Fitch},
  number =       {721},
  series =       {Springer Lecture Notes in Computer Science},
  publisher = {Springer-Verlag}
}

@InProceedings{Collins:75,
  author =       "G. E. Collins",
  title =        {{Quantifier Elimination for Real Closed Fields by
                  Cylindrical Algebraic Decomposition}},
  volume =       33,
  series =       "LNCS",
  pages =        "134-183",
  booktitle =    "Second GI Conference on Authomata Theory and Formal Languages",
  year =         1975,
  publisher =    "Springer-Verlag, Berlin"
}

@article{Collins:1976:QER:1093390.1093393,
 author = {Collins, George E.},
 title = {Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition: a synopsis},
 journal = {SIGSAM Bull.},
 issue_date = {February 1976},
 volume = {10},
 number = {1},
 month = feb,
 year = {1976},
 issn = {0163-5824},
 pages = {10--12},
 numpages = {3},
 url = {http://doi.acm.org/10.1145/1093390.1093393},
 doi = {10.1145/1093390.1093393},
 acmid = {1093393},
 publisher = {ACM},
 address = {New York, NY, USA},
}

 @Manual{codegen-man-12,
  title =        {Code generation from {Isabelle/HOL} theories},
  author =       {Florian Haftmann},
  organization = {University of Technology},
  address =      {Munich},
  year =         {2012},
  note =         {Contained in the Isabelle distribution}
}

@Book{winkler:poly,
  author =       {Winkler, Franz},
  title =        {Polynomial algorithms in computer algebra},
  publisher =    {Springer},
  year =         {1996},
  annote =       {cited in DA stefan karnel}
}

@incollection{immler2012ode,
  author = {Immler, Fabian and H\"olzl, Johannes},
  title = {Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL},
  booktitle = {Interactive Theorem Proving (ITP2012)},
  series = {Lecture Notes in Computer Science},
  editor = {Beringer, Lennart and Felty, Amy},
  pages = {377--392},
  volume = {7406},
  doi = {10.1007/978-3-642-32347-8_26},
  year = {2012}
}

@INPROCEEDINGS{Beaumont02towardsbetter,
    author = {James Beaumont and Russell Bradford and James H. Davenport and Bath Ba Ay England},
    title = {Towards better simplification of elementary functions},
    booktitle = {ACM International Symposium on Symbolic and Algebraic Computation},
    year = {2002},
    pages = {15--22},
    publisher = {ACM Press}
}

@Article{zangl:auto-ect-11,
  author =       {Schlegl, Thomas and Bretterklieber, Thomas and Neumayer, Markus and Zangl Hubert},
  title =        {Combined Capacitive and Ultrasonic Distance Measurement for Automotive Applications},
  journal =      {IEEE sensors journal},
  year =         {2011},
  volume =       {11},
  number =       {11},
  pages =        {2636-2642},
  month =        {November},
  doi =          {10.1109/JSEN.2011.2155056},
  annote =       {IEEE_Sensors_original.pdf}
}

@Unpublished{zangl:ect-precomp-12,
  author =       {Hubert Zangl and Daniel Watzenig and Gerald Steiner and Anton Fuchs and Hannes Wegleitner},
  title =        {Non-iterative Reconstruction for {Electrical Capacitance Tomography} using Low Order Approximations},
  note =         {Institute of Electrical Measurement and Measurement Signal Processing, Graz University of Technology},
  month =        {November},
  year =         {2012},
  annote =       {ECT_reco_unpublished.pdf}
}

@Article{isa-robot-12,
  author =       {Holger T\"aubig and Udo Frese and Christoph Hertzberg and Christoph L\"uth  and Stefan Mohr},
  title =        {Guaranteeing Functional Safety: Design for Provability and
Computer-Aided Verification},
  journal =      {Autonomous Robots},
  year =         {2012},
  volume =       {32},
  number =       {3},
  pages =        {303-331},
  month =        {April},
  doi =          {10.1007/s10514-011-9271-y}
}

@incollection{Ru99a,
   author = {Rump, {S.M.}},
   title = {{INTLAB - INTerval LABoratory}},
   editor = {Tibor Csendes},
   booktitle = {{Developments~in~Reliable Computing}},
   publisher = {Kluwer Academic Publishers},
   address = {Dordrecht},
   pages = {77--104},
   year = {1999},
   note = {\url{http://www.ti3.tu-harburg.de/rump/}}
}

@Article{non-shannon-01,
  author =       {Yeung, R.W. and Zhang, Z.},
  title =        {A class of non-{S}hannon-type inequalities and their applications},
  journal =      {Communications in Information and Systems},
  year =         {2001},
  volume =       {1},
  number =       {1},
  pages =        {87-100}
}

@Book{info-thy-06,
  author =       {Thomas M. Cover and Joy A. Thomas},
  title =        {Elements of Information Theory},
  publisher =    {Wiley Interscience},
  year =         {2006},
  edition =      {2},
  month =        {September},
  annote =       {640 pages}
}

@Book{vdm-09,
  author =       {John Fitzgerald and Peter Gorm Larsen},
  title =        {Modelling Systems: Practical Tools and Techniques for Software Development},
  publisher =    {Cambridge University Press},
  year =         {2009}
}

@Book{fm-03,
  author =       {Jean Francois Monin and Michael G. Hinchey},
  title =        {Understanding formal methods},
  publisher =    {Springer},
  year =         {2003}
}

@article{davenport-10:multivalued,
          volume = {6167 },
           month = {July},
          author = {James Davenport},
            note = {Invited talk at Artificial Intelligence and Symbolic Computation 2010, part of the Conferences in Intelligent Mathematics 2010, 4-10 July 2010. Paris, France.},
           title = {The Challenges of Multivalued "Functions"},
       publisher = {Springer-Verlag},
         journal = {Lecture Notes in Computer Science},
           pages = {1--12},
            year = {2010},
             url = {http://opus.bath.ac.uk/18792/},
             doi = {10.1007/978-3-642-14128-7\_1}
}

@inproceedings{hoelzl09realineequalities,
  author    = {Johannes H{\"o}lzl},
  title     = {Proving Inequalities over Reals with Computation in {Isabelle/HOL}},
  booktitle = {Proceedings of the {ACM SIGSAM 2009}
               International Workshop on Programming Languages for Mechanized
               Mathematics Systems ({PLMMS'09})},
  editor    = {Gabriel Dos Reis and Laurent Th{\'e}ry},
  pages     = {38--45},
  month     = {August},
  address   = {Munich},
  year      = {2009}
}

@Book{meta-ML-79,
  author =       {Gordon,M. and Milner,R.  and Wadsworth,C. P.},
  title =        {Edinburgh LCF: A Mechanised Logic of Computation},
  publisher =    { Springer-Verlag},
  year =         {1979},
  volume =       {78},
  series =       {Lecture Notes in Computer Science}
}

@Book{Nipkow-Paulson-Wenzel:2002,
  author        = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title         = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
  publisher     = {Springer},
  series        = {LNCS},
  volume        = 2283,
  doi = {10.1007/3-540-08766-4\_8},
  year          = {2002}
}

@InProceedings{nitpick-10,
  author =       {Jasmin C. Blanchette and Tobias Nipkow},
  title =        {Nitpick: A counterexample generator for higher-order logic based on a relational model finder},
  booktitle = {First International Conference on Interactive Theorem Proving (ITP 2010)},
  pages =        {131-146},
  year =         {2010},
  editor =       {Kaufmann, M. and Paulson, L. C.},
  number =       {6172},
  series =       {LNCS},
  publisher = {Springer}
}

@Unpublished{sledgehammer-10,
  author =       {Lawrence C. Paulson and Jasmin C. Blanchette},
  title =        {Three years of experience with Sledgehammer, a practical link between automated and interactive theorem provers},
  note =         {Invited talk at the 8th International Workshop on the Implementation of Logics (IWIL-2010)}
}

@Book{kurzweil-henstock:integral-00,
  author =       {Kurzweil, Jaroslav},
  title =        {Henstock-Kurzweil Integration: Its Relation to Topological Vector Spaces},
  publisher =    { World Scientific Publishing Company},
  year =         {2000},
  number =       {7},
  series =       {Series in Real Analysis}
}

@InProceedings{harrison:hol-light,
  author =       {Harrison, John},
  title =        {HOL Light: An Overview},
  booktitle = {Proceedings of TPHOLs},
  pages =        {60-66},
  year =         {2009},
  volume =       {5674},
  series =       {LNCS},
  publisher = {Springer}
}
@book{Gordon:93,
        title={Introduction to {HOL}: a theorem proving environment for
                  higher order logic},
        author={Gordon, M.J.C. and Melham, T.F.},
        publisher={Cambridge University Press},
        year={1993},
        volume={},series={},address={},edition={},month={},
        note={},status={},source={ref.Harrison:Metath},location={-}
       
}  

@Book{moore:acl2-00,
  author =       {Matt Kaufmann and Panagiotis Manolios and and J. Strother Moore},
  title =        {Computer-Aided Reasoning: An Approach},
  publisher =    {Kluwer Academic Publishers},
  year =         {2000},
  month =        {June}
}

@Book{cafeOBJ-98,
  author =       {Razen Diaconescu and Kokichi Futatsugi},
  title =        {CafeOBJ Report. The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification},
  publisher =    {World Scientific},
  year =         {1998},
  volume =       {6},
  series =       {Amast Series in Computing}
}

@Misc{nipkow-prog-prove,
  author =       {Nipkow, Tobias},
  title =        {Programming and Proving in {Isabelle/HOL}},
  howpublished = {contained in the Isabelle distribution},
  month =        {May 22},
  year =         {2012}
}
@Book{pl:hind97,
  author =       {J. Roger Hindley},
  title =        {Basic Simple Type Theory},
  publisher =    {Cambridge University Press},
  year =         1997,
  editor =       {S. Abramsky and P. H. Aczel and others},
  number =       42,
  series =       {Cambridge Tracts in Theoretical Computer Science},
  address =      {Cambridge},
  annote =       {97bok308}
}
@Article{Milner-78,
  author =       {Milner, R.},
  title =        {A Theory of Type Polymorphism in Programming},
  journal =      {Journal of Computer and System Science (JCSS)},
  year =         {1978},
  number =       {17},
  pages =        {348-374}
}
@incollection {haftm-nipkow-code-gen-HRS-10,
   author = {Haftmann, Florian and Nipkow, Tobias},
   affiliation = {Institut für Informatik, Technische Universität München},
   title = {Code Generation via Higher-Order Rewrite Systems},
   booktitle = {Functional and Logic Programming},
   series = {Lecture Notes in Computer Science},
   editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germán},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-12250-7},
   keyword = {Computer Science},
   pages = {103-117},
   volume = {6009},
   url = {http://dx.doi.org/10.1007/978-3-642-12251-4_9},
   doi = {10.1007/978-3-642-12251-4_9},
   year = {2010}
}
@InCollection{krauss:partial06,
  author =       {Alexander Krauss},
  title =        {Partial recursive functions in higher-order logic},
  booktitle =    {Automated Reasoning (IJCAR 2006)},
  pages =        {589-603},
  publisher = {Springer Verlag},
  year =         {2006},
  editor =       {Ulrich Furbach and Natarajan Shankar},
  volume =       {4130},
  series =       {Lecture Notes in Artificial Intelligence},
  doi = {10.1007/11814771_48}
}
@article{krauss-fun-def-10,
  author    = {Alexander Krauss},
  title     = {Partial and Nested Recursive Function Definitions in Higher-order
               Logic},
  journal   = {J. Autom. Reasoning},
  volume    = {44},
  number    = {4},
  year      = {2010},
  pages     = {303-336},
  ee        = {http://dx.doi.org/10.1007/s10817-009-9157-2},
  doi       = {10.1007/s10817-009-9157-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@InProceedings{nipkow-krauss:07-find-lex-orders,
  author =       {Bulwahn, L. and Krauss, A. and Nipkow, T.},
  title =        {Finding lexicographic orders for termination proofs in {Isabelle/HOL}},
  booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2007)},
  pages =        {38-53},
  year =         {2007},
  editor =       {K. Schneider and J. Brandt},
  volume =       {4732},
  series =       {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@InProceedings{Krauss:07-size-terminat,
  author =       {Krauss, A.},
  title =        {Certified size-change termination},
  booktitle = {Automated Deduction (CADE-21)},
  pages =        {460-476},
  year =         {2007},
  editor =       {F. Pfenning},
  volume =       {4603},
  series =       {Lecture Notes in Computer Science},
  publisher = {Springer Verlag}
}
@incollection {krauss-sternagl-11:terminat-rewrite,
   author = {Krauss, Alexander and Sternagel, Christian and Thiemann, Ren\'e and Fuhs, Carsten and Giesl, J\"urgen},
   affiliation = {Institut für Informatik, Technische Universität München, Germany},
   title = {Termination of {Isabelle} Functions via Termination of Rewriting},
   booktitle = {Interactive Theorem Proving},
   series = {Lecture Notes in Computer Science},
   editor = {van Eekelen, Marko and Geuvers, Herman and Schmaltz, Julien and Wiedijk, Freek},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-642-22862-9},
   keyword = {Computer Science},
   pages = {152-167},
   volume = {6898},
   url = {http://dx.doi.org/10.1007/978-3-642-22863-6_13},
   doi = {10.1007/978-3-642-22863-6_13},
   year = {2011}
}
@Book{progr-mathematica-2012,
  author =       {Maeder, Roman E.},
  title =        {Programming in Mathematica},
  publisher =    {Addison-Wesley},
  address =      {Reading, Mass.},
  year =         {2012},
  edition =      {3rd}
}
@Book{prog-maple06,
  author =       {Aladjav, Victor and Bogdevicius, Marijonas},
  title =        {Maple: Programming, Physical and Engineering Problems},
  publisher =    {Fultus Corporation},
  year =         {2006},
  month =        {February 27},
  annote =       {ISBN: 1596820802}
}
@Article{plmms10,
  author =       {Florian Haftmann and Cezary Kaliszyk and Walther Neuper},
  title =        {{CTP}-based programming languages~? Considerations about an experimental design},
  journal =      {ACM Communications in Computer Algebra},
  doi = {10.1145/1838599.1838621},
  year =         {2010},
  volume =       {44},
  number =       {1/2},
  pages =        {27-41}
}
@Book{db:SW-engIII,
  author =       {Bj{\o}rner, Dines},
  title =        {Software Engineering},
  publisher =    {Springer},
  year =         {2006},
  volume =       {3},
  series =       {Texts in Theoretical Computer Science},
  address =      {Berlin, Heidelberg}
}
@Book{db:dom-eng,
  author =       {Bj{\o}rner, Dines},
  title =        {Domain Engineering. Technology Management, Research and Engineering},
  publisher =    {JAIST Press},
  year =         {2009},
  month =        {Feb},
  series =       {COE Research Monograph Series},
  volume =       {4},
  address =      {Nomi, Japan}
}
@INPROCEEDINGS{Hansen94b,
  KEY           = "Hansen94",
  AUTHOR        = "Kirsten Mark Hansen",
  EDITOR        = "M. Naftalin, T. Denvir, M. Bertran",
  TITLE         = "Validation of a Railway Interlocking Model",
  BOOKTITLE     = "FME'94: Industrial Benefit of Formal Methods",
  PUBLISHER     = "Springer-Verlag",
  YEAR          = "1994",
  MONTH         = "October",
  PAGES         = "582-601",
  ANNOTE        = "",
  COMMENT       = "PGL has got the proceedings. ADN"
}
@INPROCEEDINGS{Dehbonei&94,
  KEY           = "Dehbonei\&94",
  AUTHOR        = "Dehbonei, Babak and Mejia, Fernando",
  EDITOR        = "M. Naftalin, T. Denvir, M. Bertran",
  TITLE         = "Formal Methods in the Railways Signalling Industry",
  BOOKTITLE     = "FME'94:Industrial Benefit of Formal Methods",
  PUBLISHER     = "Springer-Verlag",
  YEAR          = "1994",
  MONTH         = "October",
  PAGES         = "26-34",
  ANNOTE        = "",
  COMMENT       = "Peter has got the proceedings. ADN"
}
@Book{harr:book,
  author =       {Harrison, John R.},
  title =        {Theorem proving with the real numbers},
  publisher =    {Springer},
  year =         {1998},
  doi =          {10.1007/978-1-4471-1591-5},
  series =       {Distinguished Dissertations}
}
@techreport{harr:thesis,
  author={Harrison, John R.},
  title={Theorem proving with the real numbers},
  institution={University of Cambridge, Computer Laboratory},year={1996},
  type={Technical Report},number={408},address={},month={November},
  note={},status={},source={},location={loc?}
}  
@inproceedings{casproto,
  author    = {Cezary Kaliszyk and
               Freek Wiedijk},
  title     = {Certified Computer Algebra on Top of an Interactive Theorem
               Prover},
  booktitle = {Calculemus},
  year      = {2007},
  pages     = {94-105},
  doi       = {10.1007/978-3-540-73086-6\_8},
  crossref  = {DBLP:conf/mkm/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@InCollection{mw:isar07,
  author =       {Wenzel Makarius},
  title =        {Isabelle/{I}sar --- a generic framework for human-readable proof documents},
  booktitle =    {From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec},
  year =         {2007},
  editor =       {Matuszewski,R. and Zalewska,A.},
  volume =       {10},
  number =       {23},
  series =       {Studies in Logic, Grammar, and Rhetoric},
  address =      {University of Bialystok}
}
@Misc{mak:isar-ml-scala,
  author =       {Wenzel, Makarius},
  title =        {The languages of {I}sabelle: {I}sar, {ML}, and {S}cala},
  howpublished = {Slides Lausanne},
  month =        {September},
  year =         {2009},
  note =         {http://www4.informatik.tu-muenchen.de/~wenzelm/papers/lausanne2009.pdf}
}
@incollection {nipkow-bergh-code-gen-02,
   author = {Berghofer, Stefan and Nipkow, Tobias},
   affiliation = {Technische Universität München Institut für Informatik Arcisstraße 21 80290 München Germany},
   title = {Executing Higher Order Logic},
   booktitle = {Types for Proofs and Programs},
   series = {Lecture Notes in Computer Science},
   editor = {Callaghan, Paul and Luo, Zhaohui and McKinna, James and Pollack, Robert and Pollack, Robert},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-540-43287-6},
   keyword = {Computer Science},
   pages = {725-725},
   volume = {2277},
   url = {http://dx.doi.org/10.1007/3-540-45842-5_2},
   doi = {10.1007/3-540-45842-5_2},
   year = {2002}
}
@Manual{isa-codegen,
  title =        {Code generation from Isabelle/HOL theories},
  author =       {Florian Haftmann},
  organization = {TU Munich},
  year =         {2012},
  note =         {with contributions from Lukas Bulwahn}
}
@Manual{isar-impl,
  title =        {The {Isabelle/Isar} Implementation},
  author =       {Makarius Wenzel},
  month =        {30 January},
  year =         {2011},
  address =      {(included in the {Isabelle} distribution)},
  note =         {With contributions by Florian Haftmann and Larry Paulson}
}
 @InProceedings{nipkow-06:java-like,
  author =       {Gerwin Klein and Tobias Nipkow},
  title =        {A Machine-Checked Model for a Java-Like Language, Virtual Machine and Compiler},
  booktitle = {TOPLAS},
  pages =        {619-695},
  year =         {2006}
}
@incollection {imperative-functional-08,
   author = {Bulwahn, Lukas and Krauss, Alexander and Haftmann, Florian and Erkök, Levent and Matthews, John},
   affiliation = {Technische Universität München Institut für Informatik Boltzmannstraße 3 85748 Garching Germany},
   title = {Imperative Functional Programming with {Isabelle/HOL}},
   booktitle = {Theorem Proving in Higher Order Logics},
   series = {Lecture Notes in Computer Science},
   editor = {Mohamed, Otmane and Muñoz, César and Tahar, Sofiène},
   publisher = {Springer Berlin / Heidelberg},
   isbn = {978-3-540-71065-3},
   keyword = {Computer Science},
   pages = {134-149},
   volume = {5170},
   url = {http://dx.doi.org/10.1007/978-3-540-71067-7_14},
   doi = {10.1007/978-3-540-71067-7_14},
   year = {2008}
}
@Book{jones-haskell-03,
  author =       {Jones, Simon Peyton },
  title =        {Haskell 98 language and libraries: the Revised Report},
  publisher =    {Cambridge University Press},
  year =         {2003}
}
@InProceedings{makarius:isa-scala-jedit,
  author =       {Makarius Wenzel},
  title =        {Asyncronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
  booktitle = {User Interfaces for Theorem Provers (UITP 2010)},
  year =         {2010},
  editor =       {C. Sacerdoti Coen and D. Aspinall},
  address =      {Edinburgh, Scotland},
  month =        {July},
  organization = {FLOC 2010 Satellite Workshop},
  note =         {http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf}
}
@InProceedings{Makarius-09:parall-proof,
  author =       {Wenzel, Makarius},
  title =        {Parallel Proof Checking in {Isabelle/Isar}},
  booktitle = {ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS)},
  year =         {2009},
  editor =       {Dos Reis and L. Th\'ery},
  address =      {Munich},
  month =        {August},
  publisher = {ACM Digital library}
}
@InProceedings{parallel-ML,
  author =       {David C. J. Matthews and Makarius Wenzel},
  title =        {Efficient Parallel Programming in {Poly/ML} and {Isabelle/ML}},
  booktitle = {Proceedings of the ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming},
  year =         {2010},
  address =      {Madrid, Spain},
  month =        {January},
  organization = {DAMP 2010 co-located with POPL},
  note =         {http://www4.in.tum.de/~wenzelm/papers/parallel-ml.pdf}
}
@inproceedings{Wenzel-11:doc-orient,
 author = {Wenzel, Makarius},
 title = {Isabelle as document-oriented proof assistant},
 booktitle = {Proceedings of the 18th Calculemus and 10th international conference on Intelligent computer mathematics},
 series = {MKM'11},
 year = {2011},
 isbn = {978-3-642-22672-4},
 location = {Bertinoro, Italy},
 pages = {244--259},
 numpages = {16},
 url = {http://dl.acm.org/citation.cfm?id=2032713.2032732},
 acmid = {2032732},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
}
@InCollection{makarius-jEdit-12,
  author =       {Makarius Wenzel},
  title =        {{Isabelle/jEdit — a Prover IDE within the PIDE framework}},
  booktitle =    {Conference on Intelligent Computer Mathematics (CICM 2012)},
  publisher = {Springer},
  year =         {2012},
  editor =       {J. Jeuring et-al},
  series =       {LNAI},
  note =         {to appear}
}
@InProceedings{mini-maple-12,
  author =       {Muhammad Taimoor Khan and Wolfgang Schreiner},
  title =        {Towards the Formal Specification and Verification of Maple Programs},
  booktitle = {Intelligent Computer Mathematics},
  pages =        {231-247},
  year =         {2012},
  volume =       {7362},
  series =       {Lecture Notes in Computer Science},
  doi =          {10.1007/978-3-642-31374-5\_16}
}
@InProceedings{eventml-12,
  author =       {Mark Bickford, Vincent Rahli, and Robert L. Constable},
  title =        {The Logic of Events, a framework to reason about distributed systems},
  booktitle = {Languages for Distributed Algorithms (LADA)
wohop},
  pages =        {23-24},
  year =         {2012},
  address =      {Philadelphia, USA},
  month =        {January},
  annote =       {TODO similar talk at CICM'12}
}
@InProceedings{focal-08,
  author =       {P. Ayrault and M. Carlier and D. Delahaye and C. Dubois and D. Doligez and L. Habib and T. Hardin and M. Jaume and C. Morisset, F. Pessaux, R. Rioboo and P. Weis},
  title =        {Trusted Software within {FoCaL}},
  booktitle = {C\&ESAR 2008 - Trusting Trusted Computing?},
  year =         {2008},
  address =      {Rennes},
  month =        {December}
}
@InCollection{vdm-tools-08,
  author =       {J. S. Fitzgerald and P. G. Larsen and S. Sahara},
  title =        {{VDMTools}: advances in support for formal modeling in {VDM}},
  booktitle =    {ACM Sigplan Notices},
  year =         {2008},
  volume =       {43},
  number =       {2},
  month =        {February}
}
@Book{fm-03,
  author =       {Jean Francois Monin and Michael G. Hinchey},
  title =        {Understanding formal methods},
  publisher =    {Springer},
  year =         {2003}
}
@Misc{coq-team-10,
  author =       {Coq development team},
  title =        {Coq 8.3 Reference Manual},
  howpublished = {http://coq.inria.fr/reman},
  year =         {2010},
  note =         {INRIA}
}

@InProceedings{coq-logics-93,
  author =       {Paulin-Moring, C.},
  title =        {Inductive definitions in the system {Coq} -- rules and properties},
  booktitle =    {Typed Lambda Calculi and Applications (TLCA 1993)},
  pages =        {328-345},
  publisher = {Springer Verlag},
  year =         {1993},
  volume =       {664},
  series =       {LNCS}
}

@Misc{agda-wiki,
  author =       {Agda},
  title =        {Agda wiki},
  howpublished = {http://wiki.portal.chalmers.se/agda/agda.php}
}

@PhdThesis{adga-phd-07,
  author =       {Norell, U.},
  title =        {Towards a practical programming language based on dependent type theory},
  school =       {{Chalmers University of Technology}},
  year =         {2007}
}

@Proceedings{FME-97,
  title =        {FME’97: Industrial Applications and Strengthened Foundations of Formal Methods},
  year =         {1997},
  number =       {1313},
  series =       {LNCS},
  address =      {Graz, Austria},
  month =        {September}
}

@Proceedings{FME-96,
  title =        {FME’96: Industrial Benefit and Advances in Formal Methods},
  year =         {1996},
  number =       {1051},
  series =       {LNCS},
  address =      {Oxford, UK},
  month =        {March}
}
@proceedings{DBLP:conf/mkm/2007,
  editor    = {Manuel Kauers and
               Manfred Kerber and
               Robert Miner and
               Wolfgang Windsteiger},
  title     = {Towards Mechanized Mathematical Assistants, 14th Symposium,
               Calculemus 2007, 6th International Conference, MKM 2007,
               Hagenberg, Austria, June 27-30, 2007, Proceedings},
  booktitle = {Calculemus/MKM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4573},
  year      = {2007},
  isbn      = {978-3-540-73083-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

% TO BE INSORTED

@inproceedings{DBLP:conf/ascm/Gonthier07,
  author    = {Georges Gonthier},
  title     = {The Four Colour Theorem: Engineering of a Formal Proof},
  booktitle = {ASCM},
  year      = {2007},
  pages     = {333},
  ee        = {http://dx.doi.org/10.1007/978-3-540-87827-8_28},
  crossref  = {DBLP:conf/ascm/2007},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/ascm/2007,
  editor    = {Deepak Kapur},
  title     = {Computer Mathematics, 8th Asian Symposium, ASCM 2007, Singapore,
               December 15-17, 2007. Revised and Invited Papers},
  booktitle = {ASCM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {5081},
  year      = {2008},
  isbn      = {978-3-540-87826-1},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@phdthesis{Chaieb-PhD,
  author = {Amine Chaieb},
  title = {Automated methods for formal proofs in simple arithmetics and  algebra},
  school = {Technische Universit\"at M\"unchen},
  year = 2008,
  month = {April},
  address = {Germany}
}
@article{davenport-10:multivalued,
          volume = {6167 },
           month = {July},
          author = {James Davenport},
            note = {Invited talk at Artificial Intelligence and Symbolic Computation 2010, part of the Conferences in Intelligent Mathematics 2010, 4-10 July 2010. Paris, France.},
           title = {The Challenges of Multivalued "Functions"},
       publisher = {Springer-Verlag},
         journal = {Lecture Notes in Computer Science},
           pages = {1--12},
            year = {2010},
             url = {http://opus.bath.ac.uk/18792/},
             doi = {10.1007/978-3-642-14128-7\_1}
}

@Book{Geddes-92:comp-alg,
  author =       {Keith O. Geddes and Stephen R. Czapor and George Labahn},
  title =        {Algorithms for Computer Algebra},
  publisher =    {Kluwer Academic Publishers},
  year =         {1992},
  ISBN =         {0-7923-9259-0}
}
@ARTICLE{Chaieb-Nipkow:2008,
  author = {Amine Chaieb and Tobias Nipkow},
  title = {{Proof Synthesis and Reflection for Linear Arithmetic}},
  journal = {Journal of Automated Reasoning},
  year = 2008,
  month = {April},
  pdf = {http://www4.in.tum.de/~chaieb/pubs/pdf/linear.pdf}
}
@Misc{Isabelle:ReflectionEx,
 note = {http://isabelle.in.tum.de/dist/library/HOL/HOL-ex/ReflectionEx.html}
%  url = {http://isabelle.in.tum.de/dist/library/HOL/HOL-ex/ReflectionEx.html}
}
@Misc{Isabelle:Polynomial,
 note = {http://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Polynomial.html}
}
@Misc{Isabelle:Groups,
 note = {http://isabelle.in.tum.de/dist/library/HOL/Groups.html}
}
@Misc{Isabelle:Rings,
 note = {http://isabelle.in.tum.de/dist/library/HOL/Rings.html}
}
@Misc{Isabelle:GCD,
 note = {http://isabelle.in.tum.de/dist/library/HOL/GCD.html}
}
@article{Nipkow-Prehofer-JFP95,
 author={Tobias Nipkow and Christian Prehofer},
 title={Type Reconstruction for Type Classes},
 journal={Journal of Functional Programming},
 volume=5,number=2, year=1995,pages={201--224}
}
@InProceedings{haftm-wenzel:constr-type-class:07,
  author =       {Florian Haftmann and Makarius Wenzel},
  title =        {Constructive Type Classes in Isabelle},
  booktitle = {Types for Proofs and Programs},
  year =         {2007},
  editor =       {T. Altenkirch and C. McBride},
  number =       {4502},
  series =       {LNCS},
  organization = {TYPES 2006},
  publisher = {Springer}
}
@Manual{isa:classes,
  title =        {Haskell-style type classes with {I}sabelle/{I}sar},
  author =       {Florian Haftmann},
  year =         {2013},
  note =         {Contained in the Isabelle distribution},
  url =          {http://isabelle.in.tum.de/dist/Isabelle2013/doc/classes.pdf}
}
@Manual{isa:locales,
  title =        {Tutorial to Locales and Locale Interpretation},
  author =       {Clemens Ballarin},
  year =         {2010},
  note =         {Contained in the Isabelle distribution},
  url =          {http://isabelle.in.tum.de/dist/Isabelle2013/doc/locales.pdf}
}

@inproceedings{Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement,
  author =      {Florian Haftmann and Alexander Krauss and Ond\v{r}ej Kun\v{c}ar and Tobias Nipkow},
  title =       {Data Refinement in {Isabelle/HOL}},
  booktitle =   {Interactive Theorem Proving (ITP 2013)},
  pages =       {100-115},
  year =        2013,
  publisher =   Springer,
  series =      {Lecture Notes in Computer Science},
  volume =      {7998},
  editor =      {S. Blazy and C. Paulin-Mohring and D. Pichardie}
}
@inproceedings{kaliszyk-sac11,
  author = {Cezary Kaliszyk and
               Christian Urban},
  title = {Quotients revisited for {I}sabelle/{HOL}},
  booktitle = {Proc. of the 26th ACM Symposium on Applied Computing (SAC'11)},
  url = {http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-sac11.pdf},
  year = {2011},
  pages = {1639-1644},
  publisher = {ACM},
  editor = {William C. Chu and W. Eric Wong and Mathew J. Palakal and Chih-Cheng Hung}
}
@INPROCEEDINGS{Homeier05adesign,
    author = {Peter V. Homeier},
    title = {A Design Structure for Higher Order Quotients},
    booktitle = {In Proc. of the 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), volume 3603 of LNCS},
    year = {2005},
    pages = {130--146}
}