Dexter Kozen

Orcid: 0000-0002-8007-4725

Affiliations:
  • Cornell University, Computer Science Department


According to our database1, Dexter Kozen authored at least 155 papers between 1976 and 2024.

Collaborative distances:
  • Dijkstra number2 of three.
  • Erdős number3 of two.

Awards

ACM Fellow

ACM Fellow 2003, "For contributions to theoretical computer science.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
A cyclic proof system for Guarded Kleene Algebra with Tests (full version).
CoRR, 2024

A Cyclic Proof System for Guarded Kleene Algebra with Tests.
Proceedings of the Automated Reasoning - 12th International Joint Conference, 2024

Multisets and Distributions.
Proceedings of the Logics and Type Systems in Theory and Practice, 2024

2023
Formal Abstractions for Packet Scheduling.
Proc. ACM Program. Lang., October, 2023

Joint Distributions in Probabilistic Semantics.
Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, 2023

Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity.
Proceedings of the 50th International Colloquium on Automata, Languages, and Programming, 2023

Abstract Huffman Coding and PIFO Tree Embeddings.
Proceedings of the Data Compression Conference, 2023

2022
2022 Alonzo Church Award Announcement.
ACM SIGLOG News, October, 2022

Reminiscences of Juris.
SIGACT News, 2022

Coalgebraic tools for randomness-conserving protocols.
J. Log. Algebraic Methods Program., 2022

Formalizing Moessner's theorem and generalizations in Nuprl.
J. Log. Algebraic Methods Program., 2022

Concurrent NetKAT - Modeling and analyzing stateful, concurrent networks.
Proceedings of the Programming Languages and Systems, 2022

2021
Universal Semantics for the Stochastic λ-Calculus.
Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

Guarded Kleene Algebra with Tests: Coequations, Coinduction, and Completeness.
Proceedings of the 48th International Colloquium on Automata, Languages, and Programming, 2021

2020
Left-handed completeness.
Theor. Comput. Sci., 2020

Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time.
Proc. ACM Program. Lang., 2020

Semantics of higher-order probabilistic programs with conditioning.
Proc. ACM Program. Lang., 2020

Universal Semantics for the Stochastic Lambda-Calculus.
CoRR, 2020

Minimisation in Logical Form.
CoRR, 2020

2019
Natural Transformations as Rewrite Rules and Monad Composition.
Log. Methods Comput. Sci., 2019

On Free ω-Continuous and Regular Ordered Algebras.
Log. Methods Comput. Sci., 2019

Scalable verification of probabilistic networks.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

2018
Boolean-Valued Semantics for the Stochastic λ-Calculus.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

The Ackermann Award 2018.
Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, 2018

2017
Practical coinduction.
Math. Struct. Comput. Sci., 2017

Well-founded coalgebras, revisited.
Math. Struct. Comput. Sci., 2017

Completeness and incompleteness in nominal Kleene algebra.
J. Log. Algebraic Methods Program., 2017

CoCaml: Functional Programming with Regular Coinductive Types.
Fundam. Informaticae, 2017

Infinitary Axiomatization of the Equational Theory of Context-Free Languages.
Fundam. Informaticae, 2017

Deciding Probabilistic Program Equivalence in NetKAT.
CoRR, 2017

Cantor meets scott: semantic foundations for probabilistic networks.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Unrestricted stone duality for Markov processes.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Nominal Automata with Name Binding.
Proceedings of the Foundations of Software Science and Computation Structures, 2017

2016
Cantor meets Scott: Domain-Theoretic Foundations for Probabilistic Network Programming.
CoRR, 2016

Kolmogorov Extension, Martingale Convergence, and Compositionality of Processes.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Probabilistic NetKAT.
Proceedings of the Programming Languages and Systems, 2016

2015
A Coalgebraic Decision Procedure for NetKAT.
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Nominal Kleene Coalgebra.
Proceedings of the Automata, Languages, and Programming - 42nd International Colloquium, 2015

The Ackermann Award 2015.
Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

2014
A Metrized Duality Theorem for Markov Processes.
Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, 2014

NetkAT: semantic foundations for networks.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Kleene Algebra with Equations.
Proceedings of the Automata, Languages, and Programming - 41st International Colloquium, 2014

Citations for the test-of-time award from 1994.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

KAT + B!
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

Optimal Coin Flipping.
Proceedings of the Horizons of the Mind. A Tribute to Prakash Panangaden, 2014

NetKAT - A Formal System for the Verification of Networks.
Proceedings of the Programming Languages and Systems - 12th Asian Symposium, 2014

2013
On Moessner's Theorem.
Am. Math. Mon., 2013

Reflection in the Chomsky Hierarchy.
J. Autom. Lang. Comb., 2013

Preface.
Proceedings of the Twenty-ninth Conference on the Mathematical Foundations of Programming Semantics, 2013

Strong Completeness for Markovian Logics.
Proceedings of the Mathematical Foundations of Computer Science 2013, 2013

Stone Duality for Markov Processes.
Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, 2013

Language Constructs for Non-Well-Founded Computation.
Proceedings of the Programming Languages and Systems, 2013

Kleene Algebra with Products and Iteration Theories.
Proceedings of the Computer Science Logic 2013 (CSL 2013), 2013

2012
Computing with Capsules.
J. Autom. Lang. Comb., 2012

Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics, 2012

Capsules and Separation.
Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

2011
Realization of Coinductive Types.
Proceedings of the Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, 2011

2010
Church-Rosser Made Easy.
Fundam. Informaticae, 2010

Halting and Equivalence of Program Schemes in Models of Arbitrary Theories.
Proceedings of the Fields of Logic and Computation, 2010

2009
Applications of Metric Coinduction
Log. Methods Comput. Sci., 2009

Learning prediction suffix trees with Winnow.
Proceedings of the 26th Annual International Conference on Machine Learning, 2009

2008
Local variable scoping and Kleene algebra with tests.
J. Log. Algebraic Methods Program., 2008

The Böhm-Jacopini Theorem Is False, Propositionally.
Proceedings of the Mathematics of Program Construction, 9th International Conference, 2008

Nonlocal Flow of Control and Kleene Algebra with Tests.
Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, 2008

2007
Preface.
Sci. Comput. Program., 2007

Coinductive Proof Principles for Stochastic Processes.
Log. Methods Comput. Sci., 2007

Collective Inference on Markov Models for Modeling Bird Migration.
Proceedings of the Advances in Neural Information Processing Systems 20, 2007

2006
Theory of Computation.
Texts in Computer Science, Springer, ISBN: 978-1-84628-477-9, 2006

Logic, Language, Information and Computation.
Theor. Comput. Sci., 2006

KAT-ML: an interactive theorem prover for Kleene algebra with tests.
J. Appl. Non Class. Logics, 2006

Relational Semantics for Higher-Order Programs.
Proceedings of the Mathematics of Program Construction, 8th International Conference, 2006

On the Representation of Kleene Algebras with Tests.
Proceedings of the Mathematical Foundations of Computer Science 2006, 2006

Automating Proofs in Category Theory.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005
Kleene Algebra and Bytecode Verification.
Proceedings of the First Workshop on Bytecode Semantics, 2005


2004
Some results in dynamic model theory.
Sci. Comput. Program., 2004

Computational inductive definability.
Ann. Pure Appl. Log., 2004

2003
Substructural logic and partial correctness.
ACM Trans. Comput. Log., 2003

Efficient Code Certification for Open Firmware.
Proceedings of the 3rd DARPA Information Survivability Conference and Exposition (DISCEX-III 2003), 2003

2002
On the Complexity of Reasoning in Kleene Algebra.
Inf. Comput., 2002

Tarskian Set Constraints.
Inf. Comput., 2002

Eager Class Initialization for Java.
Proceedings of the Formal Techniques in Real-Time and Fault-Tolerant Systems, 2002

On two letters versus three.
Proceedings of the Fixed Points in Computer Science, 2002

Malicious Code Detection for Open Firmware.
Proceedings of the 18th Annual Computer Security Applications Conference (ACSAC 2002), 2002

2001
Dynamic logic.
SIGACT News, 2001

On the completeness of propositional Hoare logic.
Inf. Sci., 2001

Myhill-Nerode Relations on Automatic Systems and the Completeness of Kleene Algebra.
Proceedings of the STACS 2001, 2001

Intuitionistic Linear Logic and Partial Correctness.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

2000
On Hoare logic and Kleene algebra with tests.
ACM Trans. Comput. Log., 2000

A note on the complexity of propositional Hoare logic.
ACM Trans. Comput. Log., 2000

Certification of Compiler Optimizations Using Kleene Algebra with Tests.
Proceedings of the Computational Logic, 2000

1999
Language-Based Security.
Proceedings of the Mathematical Foundations of Computer Science 1999, 1999

Parikh's Theorem in Commutative Kleene Algebra.
Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

1998
Set Constraints and Logic Programming.
Inf. Comput., 1998

Efficient Algorithms for Optimal Video Transmission.
Proceedings of the Data Compression Conference, 1998

1997
Kleene Algebra with Tests.
ACM Trans. Program. Lang. Syst., 1997

Computing the Newtonian Graph.
J. Symb. Comput., 1997

Automata and computability.
Undergraduate texts in computer science, Springer, ISBN: 978-0-387-94907-9, 1997

1996
Rational Spaces and Set Constraints.
Theor. Comput. Sci., 1996

Decomposition of Algebraic Functions.
J. Symb. Comput., 1996

On Regularity-Preserving Functions.
Bull. EATCS, 1996

Kleene Algebra with Tests and Commutativity Conditions.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1996

A Complete Gentzen-Style Axiomatization for Set Constraints.
Proceedings of the Automata, Languages and Programming, 23rd International Colloquium, 1996

Kleene Algebra with Tests: Completeness and Decidability.
Proceedings of the Computer Science Logic, 10th International Workshop, 1996

1995
Decidability of Systems of Set Constraints with Negative Constraints
Inf. Comput., October, 1995

Efficient Recursive Subtyping.
Math. Struct. Comput. Sci., 1995

Rabin Measures.
Chic. J. Theor. Comput. Sci., 1995

1994
A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events
Inf. Comput., May, 1994

Optimal Bounds for the Change-Making Problem.
Theor. Comput. Sci., 1994

Efficient Inference of Partial Types.
J. Comput. Syst. Sci., 1994

Efficient Average-Case Algorithms for the Modular Group
Electron. Colloquium Comput. Complex., 1994

Efficient Resolution of Singularities of Plane Curves.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1994

1993
Logical Aspects of Set Constraints.
Proceedings of the Computer Science Logic, 7th Workshop, 1993

The Complexity of Set Constraints.
Proceedings of the Computer Science Logic, 7th Workshop, 1993

1992
On the Myhill-Nerode theorem theorem for trees.
Bull. EATCS, 1992

Design and Analysis of Algorithms.
Texts and Monographs in Computer Science, Springer, ISBN: 978-1-4612-4400-4, 1992

1991
Rabin Measures and Their Applications to Fairness and Automata Theory
Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

1990
On Kleene Algebras and Closed Semirings.
Proceedings of the Mathematical Foundations of Computer Science 1990, 1990

Logics of Programs.
Proceedings of the Handbook of Theoretical Computer Science, 1990

1989
Definability with Bounded Number of Bound Variables
Inf. Comput., November, 1989

Polynomial Decomposition Algorithms.
J. Symb. Comput., 1989

1988
A Fast Parallel Algorithm for Determining all Roots of a Polynomial with Real Roots.
SIAM J. Comput., 1988

A finite model theorem for the propositional μ-calculus.
Stud Logica, 1988

1987
Functional Decomposition of Polynomials
Proceedings of the 28th Annual Symposium on Foundations of Computer Science, 1987

1986
Fast parallel orthogonalization.
SIGACT News, 1986

The Complexity of Elementary Algebra and Geometry.
J. Comput. Syst. Sci., 1986

Limits for Automatic Verification of Finite-State Concurrent Systems.
Inf. Process. Lett., 1986

1985
A Probabilistic PDL.
J. Comput. Syst. Sci., 1985

A Zero-One Law for Logic with a Fixed-Point Operator
Inf. Control., 1985

NC Algorithms for Comparability Graphs, Interval Gaphs, and Testing for Unique Perfect Matching.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1985

Algebraic Cell Decomposition in NC (Preliminary Version)
Proceedings of the 26th Annual Symposium on Foundations of Computer Science, 1985

1984
A Programming Language for the Inductive Sets, and Applications
Inf. Control., 1984

Pebblings, Edgings, and Equational Logic
Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30, 1984

The Complexity of Elementary Algebra and Geometry (Preliminary Abstract)
Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30, 1984

Generalized Fair Termination.
Proceedings of the Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages, 1984

1983
Results on the Propositional mu-Calculus.
Theor. Comput. Sci., 1983

A Decision Procedure for the Propositional µ-Calculus.
Proceedings of the Logics of Programs, 1983

1982
Process Logic: Expressiveness, Decidability, Completeness.
J. Comput. Syst. Sci., 1982

Results on the Propositional µ-Calculus.
Proceedings of the Automata, 1982

1981
An Elementary Proof of the Completness of PDL.
Theor. Comput. Sci., 1981

Semantics of Probabilistic Programs.
J. Comput. Syst. Sci., 1981

Alternation.
J. ACM, 1981

Communication: Positive First-Order Logic is NP-Complete.
IBM J. Res. Dev., 1981

On Induction vs. *-Continuity.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, 1981

1980
Indexings of Subrecursive Classes.
Theor. Comput. Sci., 1980

Complexity of Boolean Algebras.
Theor. Comput. Sci., 1980

A Representation Theorem for Models of *-Free PDL.
Proceedings of the Automata, 1980

1979
On the Duality of Dynamic Algebras and Kripke Models.
Proceedings of the Logics of Programs, Workshop, ETH Zürich, May-July 1979, 1979

Automata and planar graphs.
Proceedings of the Fundamentals of Computation Theory, 1979

1978
A clique problem equivalent to graph isomorphism.
SIGACT News, 1978

Indexing of Subrecursive Classes
Proceedings of the 10th Annual ACM Symposium on Theory of Computing, 1978

On the Power of the Compass (or, Why Mazes Are Easier to Search than Graphs)
Proceedings of the 19th Annual Symposium on Foundations of Computer Science, 1978

1977
Complexity of Finitely Presented Algebras
Proceedings of the 9th Annual ACM Symposium on Theory of Computing, 1977

Lower Bounds for Natural Proof Systems
Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October, 1977

1976
On Parallelism in Turing Machines
Proceedings of the 17th Annual Symposium on Foundations of Computer Science, 1976


  Loading...