Publications Available Online
Dexter Kozen

• Kleene Algebra & Logic
• Programming Languages & Program Analysis
• Computational Algebra
• Automata & Formal Languages
• Algorithms & Complexity
• Coding Theory
• Security
• Other

[By year] [Show abstracts] [Home]

Kleene Algebra & Logic

• Dexter Kozen. Nonlocal flow of control and Kleene algebra with tests. In Proc. 23rd IEEE Symp. Logic in Computer Science (LICS'08), pages 105-117, June 2008.
  [full text] [abstract] [bibtex] [top]

• Dexter Kozen. On the coalgebraic theory of Kleene algebra with tests. Technical Report http://hdl.handle.net/1813/10173, Computing and Information Science, Cornell University, March 2008.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen and Wei-Lung (Dustin) Tseng. The Böhm-Jacopini theorem is false, propositionally. In P. Audebaud and C. Paulin-Mohring, editors, Proc. 9th Int. Conf. Mathematics of Program Construction (MPC'08), volume 5133 of Lect. Notes in Comput. Sci., pages 177-192. Springer, July 2008.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Kamal Aboul-Hosn and Dexter Kozen. Local variable scoping and Kleene algebra with tests. J. Log. Algebr. Program., 2007. DOI: 10.1016/j.jlap.2007.10.007.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Coinductive proof principles for stochastic processes. Logical Methods in Computer Science, 3(4:8), 2007. DOI: 10.2168/LMCS-3 (4:8) 2007.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen and Marc Timme. Indefinite summation and the Kronecker delta. Technical Report http://hdl.handle.net/1813/8352, Computing and Information Science, Cornell University, October 2007.
  [full text] [abstract] [bibtex] [top]

• Dexter Kozen and Nicholas Ruozzi. Applications of metric coinduction. In T. Mossakowski et al., editor, Proc. 2nd Conf. Algebra and Coalgebra in Computer Science (CALCO 2007), volume 4624 of Lecture Notes in Computer Science, pages 327-341. Springer, August 2007.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. On the representation of Kleene algebras with tests. In R. Královic and P. Urzyczyn, editors, Proc. Conf. Mathematical Foundations of Computer Science (MFCS'06), volume 4162 of Lecture Notes in Computer Science, pages 73-83. Springer, August 2006.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Kamal Aboul-Hosn and Dexter Kozen. Relational semantics for higher-order programs. In Tarmo Uustalu, editor, Proc. 8th Int. Conf. Mathematics of Program Construction (MPC'06), volume 4014 of Lecture Notes in Computer Science, pages 29-48. Springer, July 2006.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen, Christoph Kreitz, and Eva Richter. Automating proofs in category theory. In: Proc. 3rd Int. Joint Conf. Automated Reasoning (IJCAR'06), number 4130 in Lecture Notes in AI, pages 392-407. Springer, August 2006.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Kamal Aboul-Hosn and Dexter Kozen. KAT-ML: An interactive theorem prover for Kleene algebra with tests. Journal of Applied Non-Classical Logics, 16(1-2):9-33, 2006.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen and Ganesh Ramanarayanan. Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management. Technical Report TR2005-1985, Computer Science Department, Cornell University, March 2005.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen and Bernhard Möller. Separability in Domain Semirings. Technical Report 2004-16, Universität Augsburg, Institut für Informatik, December 2004.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Toward the Automation of Category Theory. Technical Report TR2004-1964, Computer Science Department, Cornell University, September 2004.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Natural transformations as rewrite rules and monad composition. Technical Report TR2004-1942, Computer Science Department, Cornell University, July 2004.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Some Results in Dynamic Model Theory. Science of Computer Programming 51:1-2, May 2004, 3-22. Special issue, Mathematics of Program Construction (MPC 2002). Ed. E. Boiten and B. Moller.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Computational Inductive Definability. Annals of Pure and Applied Logic 126:1-3, April 2004, 139-148. Special issue: Provinces of logic determined. Essays in the memory of Alfred Tarski. Ed. Z. Adamowicz, S. Artemov, D. Niwinski, E. Orlowska, A. Romanowska, J. Wolenski.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Chris Hardin and Dexter Kozen. On the Complexity of the Horn Theory of REL. Technical Report TR2003-1896, Computer Science Department, Cornell University, May 2003.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen and Jerzy Tiuryn. Substructural Logic and Partial Correctness. Trans. Computational Logic, 4(3), July 2003, 355-378. (Subsumes Dexter Kozen and Jerzy Tiuryn. Intuitionistic Linear Logic and Partial Correctness. In Proc. 16th IEEE Symp. Logic in Comput. Sci. (LICS'01), June 2001, 259-268.)
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. On Hoare Logic, Kleene Algebra, and Types. In P. Gärdenfors, J. Wolenski, and K. Kijania-Placek, editors, In the Scope of Logic, Methodology, and Philosophy of Science: Volume 1 of the 11th Int. Congress Logic, Methodology and Philosophy of Science, Cracow, August 1999, volume 315 of Studies in Epistemology, Logic, Methodology, and Philosophy of Science, pages 119-133. Kluwer, 2002.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. On the Complexity of Reasoning in Kleene Algebra. Information and Computation 179, 152-162, 2002.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Halting and Equivalence of Schemes over Recursive Theories. Technical Report TR2002-1881, Computer Science Department, Cornell University, October 2002.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Chris Hardin and Dexter Kozen. On the Elimination of Hypotheses in Kleene Algebra with Tests. Technical Report TR2002-1879, Computer Science Department, Cornell University, October 2002.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Adam Barth and Dexter Kozen. Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests. Technical Report TR2002-1865, Computer Science Department, Cornell University, June 2002.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Allegra Angus and Dexter Kozen. Kleene Algebra with Tests and Program Schematology. Technical Report TR2001-1844, Computer Science Department, Cornell University, July 2001.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen and Jerzy Tiuryn. On the completeness of propositional Hoare logic. Information Sciences, 139 (2001), 187-195.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Myhill-Nerode relations on automatic systems and the completeness of Kleene algebra. In: Afonso Ferreira and Horst Reichel, eds., Proc. 18th Symp. Theoretical Aspects of Computer Science (STACS'01), Dresden, Germany, February 2001. Springer-Verlag, Lecture Notes in Computer Science 2010, 27-38.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Ernie Cohen and Dexter Kozen. A Note on the Complexity of Propositional Hoare Logic. Trans. Computational Logic 1:1 (July 2000), 171-174.
  [full text (.pdf)] [abstract] [bibtex] [top]

• David Harel, Dexter Kozen and Jerzy Tiuryn. Dynamic Logic. MIT Press, 2000. ISBN 0-262-08289-6. 459 pages.
  [table of contents (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen and Maria-Cristina Patron. Certification of compiler optimizations using Kleene algebra with tests. In J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L.~M. Pereira, Y. Sagiv, and P.~J. Stuckey, eds, Proc. 1st Int. Conf. Computational Logic (CL2000), volume 1861 of Lecture Notes in Artificial Intelligence, Springer-Verlag, London, July 2000, 568-582.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. On Hoare logic and Kleene algebra with tests. Proc. IEEE Conf. Logic in Computer Science (LICS'99), IEEE, July 1999, 167-172. Trans. Computational Logic 1:1 (July 2000), 60-76.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Mark Hopkins and Dexter Kozen. Parikh's theorem in commutative Kleene algebra. Proc. 14th Conf. Logic in Computer Science (LICS'99), IEEE, July 1999, 394-401.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. Typed Kleene algebra. Technical Report TR98-1669, Computer Science Department, Cornell University, March 1998.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. Kleene algebra with tests. Transactions on Programming Languages and Systems, May 1997, 427-443.
  [full text (.ps)] [abstract] [bibtex] [top]

• Ernie Cohen, Dexter Kozen, and Frederick Smith. The complexity of Kleene algebra with tests. Technical Report TR96-1598, Computer Science Department, Cornell University, July 1996.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen and Frederick Smith. Kleene algebra with tests: completeness and decidability. Proc. 10th Int. Workshop on Computer Science Logic (CSL'96), ed. D. van Dalen and M. Bezem, Utrecht, The Netherlands, Springer-Verlag Lecture Notes in Computer Science volume 1258, September 1996, 244-259.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Infor. and Comput., 110:366-390, May 1994.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. On action algebras. In J. van Eijck and A. Visser, editors, Logic and Information Flow, pages 78-88. MIT Press, 1994.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. On Kleene algebras and closed semirings. In Rovan, editor, Proc. Math. Found. Comput. Sci., volume 452 of Lect. Notes in Comput. Sci., pages 26-47. Springer, 1990.
  [full text (.ps)] [abstract] [bibtex] [top]

• Neil Immerman and Dexter Kozen. Definability with bounded number of bound variables. Infor. and Comp. 83:2 (November 1989), 121-139.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. A finite model theorem for the propositional mu-calculus. Studia Logica 47(3):233-241, 1988.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Krzysztof Apt and Dexter Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22:307-309, 1986.
  [full text (.pdf)] [abstract] [bibtex] [top]

Programming Languages & Program Analysis

• Lucja Kot and Dexter Kozen. Kleene Algebra and Bytecode Verification. Proc. 1st Workshop Bytecode Semantics, Verification, Analysis, and Transformation (Bytecode'05), ed. Fausto Spoto, Edinburgh, April 2005, 201-215.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Lucja Kot and Dexter Kozen. Second-Order Abstract Interpretation via Kleene Algebra. Technical Report TR2004-1971, Computer Science Department, Cornell University, December 2004.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Kleene Algebra with Tests and the Static Analysis of Programs. Technical Report TR2003-1915, Computer Science Department, Cornell University, November 2003.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Robert Givan, David McAllester, Carl Witty and Dexter Kozen. Tarskian Set Constraints. Information and Computation, 174(2):105-131, May 2002.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen and Matt Stillerman. Eager Class Initialization for Java. In W. Damm and E.R. Olderog, editors, Proc. 7th Int. Symp. Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), volume 2469 of Lecture Notes in Computer Science, pages 71-80. IFIP, Springer-Verlag, Sept. 2002.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Set Constraints and Logic Programming. Information and Computation 142:1 (April 1998), 2-25.
  [full text (.ps)] [abstract] [bibtex] [top]

• Allan Cheng and Dexter Kozen. Some notes on rational spaces. Technical Report TR96-1576, Computer Science Department, Cornell University, March 1996.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. Rational Spaces and Set Constraints. Theoretical Computer Science 167 (1996), 73-94.
  [full text (.ps)] [abstract] [bibtex] [top]

• Allan Cheng and Dexter Kozen. A complete Gentzen-style axiomatization for set constraints. In F. Meyer auf der Heide and B. Monien, editors, Proc. 23rd International Colloquium, ICALP '96, volume 1099 of Lect. Notes in Comput. Sci., pages 134-145. Eur. Assoc. for Theoretical Comput. Sci., Springer, July 1996.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient recursive subtyping. Mathematical Structures in Computer Science 5 (1995), 1-13.
  [full text (.ps)] [abstract] [bibtex] [top]

• Alexander Aiken, Dexter Kozen, and Edward Wimmers. Decidability of systems of set constraints with negative constraints. Infor. and Comput. 122:1, October 1995, 30-44.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen, Jens Palsberg, and Michael I. Schwartzbach. Efficient inference of partial types. J. Comput. Syst. Sci. 49:2 (October 1994), 306-324.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. Logical aspects of set constraints. In Proc. 1993 Conf. Computer Science Logic (CSL'93). Eur. Assoc. Comput. Sci. Logic, Swansea, UK, September 1993. Ed. E. B"orger, Y. Gurevich, and K. Meinke, Springer-Verlag Lect. Notes in Comput. Sci. 832, 175-188.
  [full text (.ps)] [abstract] [bibtex] [top]

• Alexander Aiken, Dexter Kozen, Moshe Vardi, and Edward Wimmers. The complexity of set constraints. In Proc. 1993 Conf. Computer Science Logic (CSL'93). Eur. Assoc. Comput. Sci. Logic, Ed. E. B"orger, Y. Gurevich, and K. Meinke, Swansea, UK, September 1993, Springer-Verlag Lect. Notes in Comput. Sci. 832, 1-17.
  [full text (.ps)] [abstract] [bibtex] [top]

Computational Algebra

• Dexter Kozen and Kjartan Stefansson. Computing the Newtonian graph. J. Symbolic Computation 24 (1997), 125-136.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen, Susan Landau, and Richard Zippel. Decomposition of algebraic functions. J. Symbolic Computation, 22:3 (Sept. 1996), 235-246.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. Efficient resolution of singularities of plane curves. In P.S. Thiagarajan, editor, Proc. 14th Conf. Foundations of Software Technology and Theoretical Computer Science, Springer-Verlag Lect. Notes in Comput. Sci. 880, 1-11, December 1994.
  [full text (.ps)] [abstract] [bibtex] [top]

• Jin-Yi Cai, Wolfgang Fuchs, Dexter Kozen, and Zicheng Liu. Efficient Average-Case Algorithms for the Modular Group. In Proc. 35th IEEE Symp. Foundations of Computer Science, November 1994, 143-152.
  [full text (.ps)] [abstract] [bibtex] [top]

• Doug Ierardi and Dexter Kozen. Parallel resultant computation. In J. Reif, editor, Synthesis of Parallel Algorithms, pages 679-720. Morgan Kaufmann, 1993.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen and Susan Landau. Polynomial decomposition algorithms. J. Symbolic Computation 7 (1989), 445-456.
  [full text (.ps)] [abstract] [bibtex] [top]

• Michael Ben-Or, Ephraim Feig, Dexter Kozen, and Prasoon Tiwari. A fast parallel algorithm for determining all roots of a polynomial with real roots. SIAM J. Computing 17:6, 1081-1092, 1988.
  [full text] [abstract] [bibtex] [top]

Automata & Formal Languages

• Dexter Kozen. Theory of Computation. Springer, 2006.
  [table of contents (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Automata on Guarded Strings and Applications. Matématica Contemporânea 24 (2003), 117-139.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. On Two Letters versus Three. Technical Report 2002-1860, Computer Science Department, Cornell University, February 2002.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Automata and Computability. Springer, 1997. ISBN 0-387-94907-0. 400 pages. (table of contents and a few sample chapters)
  [table of contents (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. On regularity-preserving functions. Bull. Europ. Assoc. Theor. Comput. Sci. 58, February, 1996, 131-138.
  [full text (.ps)] [abstract] [bibtex] [top]

• Nils Klarlund and Dexter Kozen. Rabin measures. Chicago Journal of Theoretical Computer Science, 1995(3), September 1995.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Partial automata and finitely generated congruences: an extension of Nerode's theorem. In J. N. Crossley, J. B. Remmel, R. A. Shore, and M. E. Sweedler, editors, Logical Methods: in Honor of Anil Nerode's Sixtieth Birthday, pages 490-511. Birkhäuser, 1993.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. On the Myhill-Nerode theorem for trees. Bull. Europ. Assoc. Theor. Comput. Sci., 47:170-173, June 1992.
  [full text (.ps)] [abstract] [bibtex] [top]

Algorithms & Complexity

• Dexter Kozen. Lexicographic flow. Manuscript, July 2008.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen and Alexa Sharp. On distance coloring. Technical Report TR2007-2084, Computing and Information Science, Cornell University, June 2007.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Daniel Sheldon, M. A. Saleh Elmohamed, and Dexter Kozen. Collective inference on Markov models for modeling bird migration. In J. Platt, D. Koller, Y. Singer, and S. Roweis, editors, Advances in Neural Information Processing Systems (NIPS'07), volume 20, December 2007.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen, Yaron Minsky, and Brian Smith. Efficient algorithms for optimal video transmission. In: Proc. IEEE Data Compression Conference (DCC'98), ed. James A. Storer and Martin Cohn, Snowbird, Utah, March 1998, 229-238.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen and Shmuel Zaks. Optimal bounds for the change-making problem. Theor. Comput. Sci., 123:377-388, 1994.
  [full text (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen. The Design and Analysis of Algorithms. Springer-Verlag, 1991. ISBN 0-387-97687-6. 322 pages.
  [table of contents (.ps)] [abstract] [bibtex] [top]

• Dexter Kozen, Umesh Vazirani, and Vijay Vazirani. NC algorithms for comparability graphs, interval graphs, and unique perfect matching.
  [full text (.ps)] [abstract] [bibtex] [top]

Coding Theory

• Kenneth Andrews, Chris Heegard, and Dexter Kozen. A theory of interleavers. Technical report TR97-1634, Computer Science Department, Cornell University, June 1997.
  [full text (.ps)] [abstract] [bibtex] [top]

Security

• Fred B. Schneider, Dexter Kozen, Greg Morrisett, and Andrew C. Myers. Language-based security for malicious mobile code. In Department of Defense Sponsored Information Security Research: New Methods for Protecting Against Cyber Threats, pages 477-494. Wiley, 2007.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Frank Adelstein, Dexter Kozen and Matt Stillerman. Malicious Code Detection for Open Firmware. In Proc. 18th Computer Security Applications Conf. (ACSAC'02), Las Vegas, December 2002, pages 403-412.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Language-Based Security. In M. Kutylowski, L. Pacholski, and T. Wierzbicki, editors, Proc. Conf. Mathematical Foundations of Computer Science (MFCS'99), volume 1672 of Lecture Notes in Computer Science, pages 284--298. Springer-Verlag, September 1999.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. Efficient Code Certification. Technical report TR98-1661, Computer Science Department, Cornell University, January 1998.
  [full text (.pdf)] [abstract] [bibtex] [top]

Other

• Chavdar Botev, Hubert Chao, Theodore Chao, Yim Cheng, Raymond Doyle, Sergey Grankin, Jon Guarino, Saikat Guha, Pei-Chen Lee, Dan Perry, Christopher Re, Ilya Rifkin, Tingyan Yuan, Dora Abdullah, Kathy Carpenter, David Gries, Dexter Kozen, Andrew Myers, David Schwartz, and Jayavel Shanmugasundaram. Supporting Workflow in a Course Management System. In W. Dann et al., editor, Proc. Technical Symposium on Computer Science Education (SIGCSE 2005). ACM SIGCSE, February 2005, pages 262-266.
  [full text (.pdf)] [abstract] [bibtex] [top]

• Dexter Kozen. On teaching left-handed children to write. Technical Report TR87-844, Computer Science Department, Cornell University, June 1987.
  [full text] [abstract] [bibtex] [top]