KA-add.bib

   1 @InCollection{KA-closedSr,
   2   author =       "D. Kozen",
   3   title =        "On {Kleene} algebras and closed semirings",
   4   booktitle =    "Proceedings of the 15th International Symposium on
   5                  Mathematical Foundations of Computer Science, MFCS'90
   6                  (Bansk{\'a} Bystrica, Czechoslovakia, August 27-31,
   7                  1990)",
   8   pages =        "26--47",
   9   year =         "1990",
  10   volume =       "452",
  11   series =       "LNCS",
  12   editor =       "B. Rovan",
  13   publisher =    "Springer-Verlag",
  14   address =      "Berlin-Heidelberg-New York-London-Paris-Tokyo-Hong
  15                  Kong",
  16   URL =          "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=452&spage=26",
  17   acknowledgement = "LEABib --- Lehrstuhl f{\"u}r Effiziente Algorithmen
  18                  der Technischen Universit{\"a}t M{\"u}nchen.
  19                  http://wwwmayr.informatik.tu-muenchen.de/leabib",
  20   cdate =        "1970-01-01",
  21   mdate =        "1970-01-01",
  22 }
  23
  24 @Misc{oai:CiteSeerPSU:104845,
  25   title =        "Typed {Kleene} Algebra",
  26   author =       "Dexter Kozen",
  27   year =         "1998",
  28   month =        mar # "~17",
  29   abstract =     "In previous work we have found it necessary to argue
  30                  that certain theorems of Kleene algebra hold even when
  31                  the symbols are interpreted as nonsquare matrices. In
  32                  this note we define and investigate typed Kleene
  33                  algebra, a typed version of Kleene algebra in which
  34                  objects have types s ! t. Although nonsquare matrices
  35                  are the principal motivation, there are many other
  36                  useful interpretations: traces, binary relations,
  37                  Kleene algebra with tests. We give a set of typing
  38                  rules and show that every expression has a unique most
  39                  general typing (mgt). Then we prove the following
  40                  metatheorem that incorporates the abovementioned
  41                  results for nonsquare matrices as special cases. Call
  42                  an expression 1-free if it contains only the Kleene
  43                  algebra operators (binary) +, (unary) + , 0, and Delta,
  44                  but no occurrence of 1 or . Then every universal 1-free
  45                  formula that is a theorem of Kleene algebra is also a
  46                  theorem of typed Kleene algebra under its most general
  47                  typing. The metatheorem is false without the...",
  48   citeseer-references = "oai:CiteSeerPSU:111064; oai:CiteSeerPSU:111064;
  49                  oai:CiteSeerPSU:62200; oai:CiteSeerPSU:188632",
  50   annote =       "Author: Dexter Kozen (Affiliation: Department of
  51                  Computer Science, Cornell University; Address: Ithaca,
  52                  New York 14853-7501, USA; ); The Pennsylvania State
  53                  University CiteSeer Archives",
  54   language =     "en",
  55   oai =          "oai:CiteSeerPSU:104845",
  56   rights =       "unrestricted",
  57   subject =      "Dexter Kozen Typed Kleene Algebra",
  58   URL =          "http://citeseer.ist.psu.edu/104845.html;
  59                  http://www.cs.cornell.edu/kozen/papers/typed.ps",
  60 }
  61
  62 @Misc{oai:CiteSeerPSU:211884,
  63   title =        "On {Hoare} Logic, {Kleene} Algebra, and Types",
  64   author =       "Dexter Kozen",
  65   year =         "1999",
  66   month =        jul # "~30",
  67   abstract =     "We show that propositional Hoare logic is subsumed by
  68                  the type calculus of typed Kleene algebra augmented
  69                  with subtypes and typecasting. Assertions are
  70                  interpreted as typecast operators. Thus Hoare-style
  71                  reasoning with partial correctness assertions reduces
  72                  to typechecking in this system. 1 Introduction In
  73                  previous work [18, 19], we have shown that Kleene
  74                  algebra with tests (KAT) subsumes propositional Hoare
  75                  logic (PHL). Thus the specialized syntax and deductive
  76                  apparatus of Hoare logic are inessential and can be
  77                  replaced by simple equational reasoning. We have also
  78                  shown that KAT provides a complete deductive system for
  79                  Hoare-style inference rules involving partial
  80                  correctness assertions and that PHL is PSPACE-complete.
  81                  In other recent work [17], we have introduced a simple
  82                  and natural type system for Kleene algebra (KA) in
  83                  which objects have types s ! t. The use of types was
  84                  motivated by the desire to handle nonsquare matrices,
  85                  although there are other useful interpretations. In
  86                  t...",
  87   citeseer-references = "oai:CiteSeerPSU:85616; oai:CiteSeerPSU:111064;
  88                  oai:CiteSeerPSU:111064; oai:CiteSeerPSU:100980;
  89                  oai:CiteSeerPSU:100980; oai:CiteSeerPSU:62200",
  90   annote =       "Author: Dexter Kozen (Affiliation: Department of
  91                  Computer Science, Cornell University; Address: Ithaca,
  92                  New York 14853-7501, USA; ); The Pennsylvania State
  93                  University CiteSeer Archives",
  94   language =     "en",
  95   oai =          "oai:CiteSeerPSU:211884",
  96   rights =       "unrestricted",
  97   subject =      "Dexter Kozen On Hoare Logic, Kleene Algebra, and
  98                  Types",
  99   URL =          "http://citeseer.ist.psu.edu/211884.html;
 100                  http://www.cs.cornell.edu/kozen/papers/typedHoare.ps",
 101 }
 102
 103 @InProceedings{KA-commutative-Parikh,
 104   author =       "M. Hopkins and D. Kozen",
 105   title =        "Parikh's Theorem in Commutative {Kleene} Algebra",
 106   pages =        "394--401",
 107   booktitle =    "14th Symposium on Logic in Computer Science
 108                  ({LICS}'99)",
 109   ISBN =         "0-7695-0158-3",
 110   month =        jul,
 111   publisher =    "IEEE",
 112   address =      "Washington - Brussels - Tokyo",
 113   year =         "1999",
 114 }
 115
 116 @Article{KA-Myhill,
 117   author =       "Dexter Kozen",
 118   title =        "{Myhill-Nerode} Relations on Automatic Systems and the
 119                  Completeness of {Kleene} Algebra",
 120   journal =      "Lecture Notes in Computer Science",
 121   volume =       "2010",
 122   pages =        "27--??",
 123   year =         "2001",
 124   CODEN =        "LNCSD9",
 125   ISSN =         "0302-9743",
 126   bibdate =      "Sat Feb 2 13:03:28 MST 2002",
 127   URL =          "http://link.springer-ny.com/link/service/series/0558/bibs/2010/20100027.htm;
 128                  http://link.springer-ny.com/link/service/series/0558/papers/2010/20100027.pdf",
 129   acknowledgement = ack-nhfb,
 130 }
 131
 132 @Misc{oai:CiteSeerPSU:261988,
 133   title =        "Certification of Compiler Optimizations using {Kleene}
 134                  Algebra with Tests",
 135   author =       "Dexter Kozen and Maria-cristina Patron",
 136   year =         "1999",
 137   month =        dec # "~30",
 138   abstract =     "We use Kleene algebra with tests to verify a wide
 139                  assortment of common compiler optimizations, including
 140                  dead code elimination, common subexpression
 141                  elimination, copy propagation, loop hoisting, induction
 142                  variable elimination, instruction scheduling, algebraic
 143                  simplification, loop unrolling, elimination of
 144                  redundant instructions, array bounds check elimination,
 145                  and introduction of sentinels. In each of these cases,
 146                  we give a formal equational proof of the correctness of
 147                  the optimizing transformation. 1 Introduction Kleene
 148                  algebra (KA) is the algebra of regular expressions. It
 149                  was first introduced by Kleene in 1956 [9] and further
 150                  developed in the 1971 monograph of Conway [6]. It has
 151                  reappeared in many contexts in mathematics and computer
 152                  science [23, 10, 22, 16, 17, 1, 8]. In [12], an
 153                  extension of KA called Kleene algebra with tests (KAT)
 154                  was introduced. This system combines programs and
 155                  assertions in a simple, purely equational system. In
 156                  [14] it was shown that KAT strictly subsumes...",
 157   citeseer-references = "oai:CiteSeerPSU:1688; oai:CiteSeerPSU:85616;
 158                  oai:CiteSeerPSU:111064; oai:CiteSeerPSU:118905;
 159                  oai:CiteSeerPSU:100980; oai:CiteSeerPSU:62200;
 160                  oai:CiteSeerPSU:50371; oai:CiteSeerPSU:17400;
 161                  oai:CiteSeerPSU:188632",
 162   annote =       "Author: Dexter Kozen (Affiliation: Cornell University;
 163                  Address: Ithaca, New York 14853-7501; ); Author:
 164                  Maria-cristina Patron (Affiliation: Cornell University;
 165                  Address: Ithaca, New York 14853-7501; ); The
 166                  Pennsylvania State University CiteSeer Archives",
 167   language =     "en",
 168   oai =          "oai:CiteSeerPSU:261988",
 169   rights =       "unrestricted",
 170   subject =      "Dexter Kozen,Maria-cristina Patron Certification of
 171                  Compiler Optimizations using Kleene Algebra with
 172                  Tests",
 173   URL =          "http://citeseer.ist.psu.edu/261988.html;
 174                  http://www.cs.cornell.edu/kozen/papers/opti.ps",
 175 }
 176
 177 @Misc{KAT-coalgebraic,
 178   title =        "A Coalgebraic Approach to {Kleene} Algebra with Tests",
 179   note =         "Comment: 21 pages, 1 figure; preliminary version
 180                  appeared in Proc. Workshop on Coalgebraic Methods in
 181                  Computer Science (CMCS'03)",
 182   author =       "Hubie Chen and Riccardo Pucella",
 183   year =         "2004",
 184   month =        may # "~26",
 185   abstract =     "Kleene algebra with tests is an extension of Kleene
 186                  algebra, the algebra of regular expressions, which can
 187                  be used to reason about programs. We develop a
 188                  coalgebraic theory of Kleene algebra with tests, along
 189                  the lines of the coalgebraic theory of regular
 190                  expressions based on deterministic automata. Since the
 191                  known automata-theoretic presentation of Kleene algebra
 192                  with tests does not lend itself to a coalgebraic
 193                  theory, we define a new interpretation of Kleene
 194                  algebra with tests expressions and a corresponding
 195                  automata-theoretic presentation. One outcome of the
 196                  theory is a coinductive proof principle, that can be
 197                  used to establish equivalence of our Kleene algebra
 198                  with tests expressions.",
 199   identifier =   "Theoretical Computer Science, 327 (1-2), 23-44
 200                  (2004)",
 201   oai =          "oai:arXiv.org:cs/0405097",
 202   subject =      "Logic in Computer Science; Programming Languages;
 203                  F.3.1; I.1.1; I.1.3",
 204   URL =          "http://arxiv.org/abs/cs/0405097",
 205 }
 206
 207 @Proceedings{KA-appls,
 208   title =        {Applications of {Kleene} algebra},
 209   year =         {2001},
 210   editor =       {R Backhouse and D Kozen and B Moller},
 211   note =         {ÎÉÞÅÇÏ ÏÓÏÂÅÎÎÏ ÐÏÌÅÚÎÏÇÏ},
 212 }
 213
 214 @Article{dynamic-model,
 215   author =       "Dexter Kozen",
 216   title =        "Some Results in Dynamic Model Theory",
 217   journal =      "Lecture Notes in Computer Science",
 218   volume =       "2386",
 219   pages =        "21--??",
 220   year =         "2002",
 221   CODEN =        "LNCSD9",
 222   ISSN =         "0302-9743",
 223   bibdate =      "Tue Sep 10 19:10:03 MDT 2002",
 224   URL =          "http://link.springer-ny.com/link/service/series/0558/bibs/2386/23860021.htm;
 225                  http://link.springer-ny.com/link/service/series/0558/papers/2386/23860021.pdf",
 226   acknowledgement = ack-nhfb,
 227 }
 228
 229 @techreport{KAT-schematology,
 230  author = {Allegra Angus and Dexter Kozen},
 231  title = {{Kleene} Algebra with Tests and Program Schematology},
 232  year = {2001},
 233  source = {http://www.ncstrl.org:8900/ncstrl/servlet/search?formname=detail\&id=oai%3Ancstrlh%3Acornellcs%3ACORNELLCS%3ATR2001-1844},
 234  publisher = {Cornell University},
 235   institution =  {Cornell University},
 236  address = {Ithaca, NY, USA},
 237  }
 238
 239 @inproceedings{DBLP:conf/lpar/Hardin04,
 240   author    = {Christopher Hardin},
 241   title     = {How the Location of * Influences Complexity in {Kleene} Algebra
 242                with Tests.},
 243   booktitle = {LPAR},
 244   year      = {2004},
 245   pages     = {224-239},
 246   ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3452{\&}spage=224},
 247   crossref  = {DBLP:conf/lpar/2004},
 248   bibsource = {DBLP, http://dblp.uni-trier.de}
 249 }
 250
 251 @proceedings{DBLP:conf/lpar/2004,
 252   editor    = {Franz Baader and
 253                Andrei Voronkov},
 254   title     = {Logic for Programming, Artificial Intelligence, and Reasoning,
 255                11th International Conference, LPAR 2004, Montevideo, Uruguay,
 256                March 14-18, 2005, Proceedings},
 257   booktitle = {LPAR},
 258   publisher = {Springer},
 259   series    = {Lecture Notes in Computer Science},
 260   volume    = {3452},
 261   year      = {2005},
 262   isbn      = {3-540-25236-3},
 263   bibsource = {DBLP, http://dblp.uni-trier.de}
 264 }
 265
 266 @InProceedings{Kozen-induction-continuity,
 267   author =       "D. Kozen",
 268   title =        "On induction vs. *-continuity",
 269   booktitle =    "Proc. Workshop on Logics of Programs 1981",
 270   series =       "Lecture Notes in Computer Science",
 271   volume =       "131",
 272   publisher =    "Spring-Verlag",
 273   editor =       "D. Kozen",
 274   year =         "1981",
 275   pages =        "167--176",
 276   note =         {\toRead},
 277 }