Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/BirdKMP/document/   (Sammlung formaler Beweise Version 2026-5©)  Datei vom 29.4.2026 mit Größe 13 kB image not shown  

Quelle  root.bib

  Sprache: Latech
 

@STRING{LNCS="LNCS"}
@STRING{scp="Science of Computer Programming"}

@article{BirdGibbonsJones:1989,
  author    = {Bird, R. S. and
               Gibbons, J. and
               Jones, G.},
  title     = {Formal Derivation of a Pattern Matching Algorithm},
  journal   = {Science of Computer Programming},
  volume    = 12,
  number    = 2,
  pages     = {93--104},
  year      = 1989,
  doi       = {10.1016/0167-6423(89)90036-1},
}

@book{Bird:PearlsofFAD:2010,
  title = "Pearls of Functional Algorithm Design",
  author = "R. S. Bird",
  year = 2010,
  isbn = 9780521513388,
  publisher = "CUP",
}

@incollection{Bird:1987,
  title = "An Introduction to the Theory of Lists",
  author = "R. S. Bird",
  year = 1987,
  booktitle = "Logic of Programming and Calculi of Discrete Design",
  editor = "M. Broy",
  note = "NATO ASI Series~F Volume~36. Also available as Technical Monograph PRG-56, from the Programming Research Group, Oxford University",
  pages = "3--42",
  publisher = "Springer-Verlag",
}

@inproceedings{Bird:2005,
  author    = {R. S. Bird},
  title     = {Polymorphic string matching},
  booktitle = {Haskell'2005},
  pages     = {110--115},
  publisher = {{ACM}},
  year      = 2005,
  doi       = {10.1145/1088348.1088359},
}

@article{TakeichiAkama:1990,
 author = {Takeichi, M. and Akama, Y.},
 title = {Deriving a Functional {Knuth-Morris-Pratt} Algorithm by Transformation},
 journal = {Journal of Information Processing},
 issue_date = 1990,
 volume = 13,
 number = 4,
 month = apr,
 year = 1991,
 pages = {522--528},
 numpages = 7,
 publisher = {Information Processing Society of Japan},
 address = {Tokyo, Japan, Japan},
}

@article{Bird:2012,
  author    = {R. S. Bird},
  title     = {On building cyclic and shared structures in {Haskell}},
  journal   = {Formal Aspects of Computing},
  volume    = 24,
  number    = {4-6},
  pages     = {609--621},
  year      = 2012,
  doi       = {10.1007/s00165-012-0243-6},
}

@inproceedings{Pettorossi:1987,
  author    = {A. Pettorossi},
  title     = {Program Development Using Lambda Abstraction},
  booktitle = {FSTTCS'1987},
  series    = LNCS,
  volume    = {287},
  pages     = {420--434},
  year      = 1987,
  doi       = {10.1007/3-540-18625-5_65},
}

@article{Bird:1977,
  author    = {R. S. Bird},
  title     = {Improving Programs by the Introduction of Recursion},
  journal   = {Communications of the {ACM}},
  volume    = 20,
  number    = 11,
  pages     = {856--863},
  year      = 1977,
  doi       = {10.1145/359863.359889},
}

@inproceedings{DanielssonHJG:2006,
  author    = {Danielsson, N. A.  and
               Hughes, J. and
               Jansson, J. and
               Gibbons, J.},
  title     = {Fast and loose reasoning is morally correct},
  booktitle = {POPL 2006},
  publisher = {{ACM}},
  pages     = {206--217},
  year      = 2006,
  doi       = {10.1145/1111037.1111056},
}

@article{Pettorossi:1996,
  author    = {Pettorossi, A. and
               Proietti, M.},
  title     = {Rules and Strategies for Transforming Functional and Logic Programs},
  journal   = {{ACM} Computing Surveys},
  volume    = {28},
  number    = {2},
  pages     = {360--414},
  year      = {1996},
  doi       = {10.1145/234528.234529},
}

@article{AgerDanvyRohde:2006,
  author    = {M. S. Ager and
               O. Danvy and
               H. K. Rohde},
  title     = {Fast partial evaluation of pattern matching in strings},
  journal   = toplas,
  volume    = 28,
  number    = 4,
  pages     = {696--714},
  year      = 2006,
  doi       = {10.1145/1146812},
}

@article{Scott:1976,
  author    = {D. S. Scott},
  title     = {Data Types as Lattices},
  journal   = {{SIAM} Journal of Computing},
  volume    = 5,
  number    = 3,
  pages     = {522--587},
  year      = 1976,
  doi       = {10.1137/0205037},
}

@book{Stoy:1977,
 author = {J. E. Stoy},
 title = "Denotational Semantics: The {S}cott-{S}trachey Approach to Programming Language Theory",
 year = {1977},
 publisher = {MIT Press},
}

@article{MannaNesVuillemin:1973,
  author    = {Manna, Z. and
               Ness, S. and
               Vuillemin, J.},
  title     = {Inductive Methods for Proving Properties of Programs},
  journal   = cacm,
  volume    = 16,
  number    = 8,
  pages     = {491--502},
  year      = 1973,
  doi       = {10.1145/355609.362336},
}

@inproceedings{barbed-wire:1991,
        abstract = {We develop a calculus for lazy functional programming based on recursion operators associated with data type definitions. For these operators we derive various algebraic laws that are useful in deriving and manipulating programs. We shall show that all example functions in Bird and Wadler's "Introduction to Functional Programming" can  expressed using these operators.},
        author = {E. Meijer and M. Fokkinga and R. Paterson},
        booktitle = "FPCA'1991",
        pages = {124--144},
        posted-at = {2008-08-18 18:44:21},
        priority = 2,
        publisher = {Springer-Verlag},
        title = {Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire},
        year = 1991
}

@article{Gammie:2011,
  author =       {P. Gammie},
  title =        {Short Note: Strict unwraps make worker/wrapper fusion totally correct},
  journal =      {Journal of Functional Programming},
  year =         2011,
  volume =       21,
  pages =        {209--213}
}

@article{GillHutton:2009,
  author = {A. Gill and G. Hutton},
  title = {The worker/wrapper transformation},
  journal = "Journal of Functional Programming",
  publisher = {CUP},
  volume = 19,
  number = 2,
  pages = {227--251},
  month = {March},
  year = 2009
}

@book{Hutton:2016,
  author = "G. Hutton",
  title = "Programming in {Haskell}",
  publisher = "CUP",
  month = sep,
  edition = "Second",
  year = 2016
}

@inproceedings{Matthews:1999,
  author    = {J. Matthews},
  title     = {Recursive Function Definition over Coinductive Types},
  booktitle = {TPHOLs'99},
  pages     = {73--90},
  year      = 1999,
  doi       = {10.1007/3-540-48256-3\_6},
}

@book{CrochemoreRytter:2002,
  author =    {M. Crochemore and W. Rytter},
  title =        {Jewels of Stringology},
  publisher =    {World Scientific},
  year =         2002,
  isbn = {981-02-4782-6}
}

@inproceedings{BlanchetteEtAl:2017,
  author    = {Blanchette, J. C. and
               A. Bouzy and
               A. Lochbihler and
               A. Popescu and
               D. Traytel},
  title     = {Friends with Benefits - Implementing Corecursion in Foundational Proof
               Assistants},
  booktitle = {ESOP'2017},
  publisher = {Springer},
  series    = LNCS,
  volume    = 10201,
  pages     = {111--140},
  year      = 2017,
  doi       = {10.1007/978-3-662-54434-1\_5},
}

% Worked with Irving on Stable Marriage
@book{Gusfield:1997,
  author    = {D. Gusfield},
  title     = {Algorithms on Strings, Trees, and Sequences - Computer Science and
               Computational Biology},
  publisher = {CUP},
  year      = 1997,
  isbn      = {0-521-58519-8},
}

@article{HinzeJeuring:2001,
  author    = {R. Hinze and
               J. Jeuring},
  title     = {Weaving a web},
  journal   = {Journal of Functional Programming},
  volume    = 11,
  number    = 6,
  pages     = {681--689},
  year      = 2001,
  doi       = {10.1017/S0956796801004129},
}

@article{JeanninEtAl:2017,
  author    = {J.{-}B. Jeannin and
               D. Kozen and
               A. Silva},
  title     = {CoCaml: Functional Programming with Regular Coinductive Types},
  journal   = {Fundamenta Informaticae},
  volume    = 150,
  number    = {3-4},
  pages     = {347--377},
  year      = 2017,
  doi       = {10.3233/FI-2017-1473},
}

@article{Courcelle:1983,
  author    = {B. Courcelle},
  title     = {Fundamental Properties of Infinite Trees},
  journal   = TCS,
  volume    = 25,
  pages     = {95--169},
  year      = 1983,
  doi       = {10.1016/0304-3975(83)90059-2},
}

@InCollection{Colmerauer:1982,
  author =       "A. Colmerauer",
  title =        "{Prolog} and infinite trees",
  booktitle =    "Logic Programming",
  publisher =    "Academic Press",
  year =         "1982",
  editor =       "K. L. Clark and S. -\AA. Tarnlund",
  pages =        "107--114",
}

@article{GiannesiniCohen:1984,
  author    = {F. Giannesini and
               J. Cohen},
  title     = {Parser Generation and Grammar Manipulation Using {Prolog}'s Infinite
               Trees},
  journal   = {Journal of Logic Programming},
  volume    = 1,
  number    = 3,
  pages     = {253--265},
  year      = 1984,
  doi       = {10.1016/0743-1066(84)90013-X},
}

@inproceedings{DanvyThiemannZerny:2013,
  author    = {O. Danvy and
               P. Thiemann and
               I. Zerny},
  title     = {Circularity and Lambda Abstraction: From {Bird} to {Pettorossi} and back},
  publisher = {{ACM}},
  booktitle = {IFL'2013},
  pages     = 85,
  year      = 2013,
  doi       = {10.1145/2620678.2620687},
}

@inproceedings{Danielsson:2010,
  author    = {N. A. Danielsson},
  title     = {Total parser combinators},
  publisher = {{ACM}},
  booktitle = {ICFP'2010},
  pages     = {285--296},
  year      = 2010,
  doi       = {10.1145/1863543.1863585},
}

@article{HOLCF:1999,
  author = {O. M\"uller and T. Nipkow and von Oheimb, D. and O. Slotosch},
  title = {{HOLCF = HOL + LCF}},
  journal="Journal of Functional Programming",volume=9,pages={191--223},
  year=1999
}

@article{BurstallDarlington:1977,
 author = {R. M. Burstall and J. Darlington},
 title = {A Transformation System for Developing Recursive Programs},
 journal = jacm,
 volume = 24,
 number = 1,
 year = 1977,
 pages = {44--67},
 doi = {10.1145/321992.321996},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{HOLCF-Prelude-AFP:2017,
  author    = {J. Breitner and
               B. Huffman and
               N. Mitchell and
               C. Sternagel},
  title     = {{HOLCF-Prelude}},
  journal   = {Archive of Formal Proofs},
  year      = 2017,
  url       = {https://www.isa-afp.org/entries/HOLCF-Prelude.shtml},
}

@article{KnuthMorrisPratt:1977,
  author    = {D. E. Knuth and
               Morris Jr., J. H. and
               V. R. Pratt},
  title     = {Fast Pattern Matching in Strings},
  journal   = {{SIAM} Journal on Computing},
  volume    = 6,
  number    = 2,
  pages     = {323--350},
  year      = 1977,
  doi       = {10.1137/0206024},
}

@inproceedings{LochbihlerMaximova:2015,
  author    = {A. Lochbihler and
               A. Maximova},
  title     = {Stream Fusion for {Isabelle}'s Code Generator - Rough Diamond},
  booktitle = {ITP'2015},
  series    = lncs,
  volume    = 9236,
  publisher = {Springer},
  pages     = {270--277},
  year      = 2015,
  doi       = {10.1007/978-3-319-22102-1\_18},
}

@article{Huffman:2009,
  author  = {B. Huffman},
  title   = {Stream Fusion},
  journal = {Archive of Formal Proofs},
  month   = apr,
  year    = 2009,
  url     = "http://isa-afp.org/entries/Stream-Fusion.html",
}

@inproceedings{TurbakWells:2001,
  author    = {F. A. Turbak and
               J. B. Wells},
  title     = {Cycle Therapy: {A} Prescription for Fold and Unfold on Regular Trees},
  booktitle = {PPDP'2001},
  publisher = {{ACM}},
  pages     = {137--149},
  year      = 2001,
  doi       = {10.1145/773184.773200},
}

@article{Sijtsma:1989,
  author    = {Ben A. Sijtsma},
  title     = {On the Productivity of Recursive List Definitions},
  journal   = toplas,
  volume    = 11,
  number    = 4,
  pages     = {633--649},
  year      = 1989,
  doi       = {10.1145/69558.69563},
}

@article{vanderWoude:1989,
  author    = {van der Woude, J.},
  title     = {Playing with Patterns, Searching for Strings},
  journal   = scp,
  volume    = 12,
  number    = 3,
  pages     = {177--190},
  year      = 1989,
  doi       = {10.1016/0167-6423(89)90001-4},
}

@phdthesis{Tullsen:PhDThesis,
 author = {M. Tullsen},
 title = {{PATH}, a Program Transformation System for {H}askell},
 year = {2002},
 isbn = {0-493-60483-9},
 order_no = {AAI3046238},
 school = {Yale University},
 address = {New Haven, CT, USA},
 url = "http://www.cs.yale.edu/publications/techreports/tr1229.pdf"
}

@misc{Pottier:2012,
  author = "F. Pottier",
  title = "Reconstructing the {Knuth-Morris-Pratt} algorithm",
  year = 2012,
  url = "http://gallium.inria.fr/blog/kmp/"
}

@book{Paulson:1987,
  author    = {L. C. Paulson},
  title     = {Logic and computation - interactive proof with {Cambridge LCF}},
  series    = {Cambridge Tracts in Theoretical Computer Science},
  volume    = 2,
  publisher = {CUP},
  year      = 1987,
  isbn      = {978-0-521-34632-0},
}

@inproceedings{Huffman:2009a,
  author    = {B. Huffman},
  title     = {A Purely Definitional Universal Domain},
  booktitle = "{TPHOL}s",
  series    = lncs,
  volume    = 5674,
  year      = 2009,
  pages     = {260-275},
  doi       = "10.1007/978-3-642-03359-9_19",
}

@inproceedings{Altenkirch:2001,
  author    = {T. Altenkirch},
  title     = {Representations of First Order Function Types as Terminal Coalgebras},
  booktitle = {{TLCA} 2001},
  series    = lncs,
  volume    = 2044,
  pages     = {8--21},
  publisher = {Springer},
  year      = 2001,
  doi       = {10.1007/3-540-45413-6_5},
}

@book{SterlingShapiro:1994,
  author    = {L. Sterling and E. Shapiro},
  title     = {The Art of Prolog - Advanced Programming Techniques},
  publisher = {{MIT} Press},
  year      = 1994,
  edition   = "2nd"
}

Messung V0.5 in Prozent
C=89 H=96 G=92

¤ Dauer der Verarbeitung: 0.6 Sekunden  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.