Research & Teaching Experience ffl Research Assistant 1997-present (2009)
Researched type systems and optimization techniques for run-time code generation (RTCG). Built an optimizing and certifying compiler supporting RTCG. Evaluated the compiler's performance with...
Applications of Metric Coinduction (2009)
Kozen, Dexter, Ruozzi, Nicholas
Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One can prove a coinduction step showing that some...
The lexicographic flow problem is a flow problem in which the edges are assigned priorities, and we wish to find a flow that is lexicographically maximum with respect to the priority assignment. The...
This paper studies the problem of simulating a coin of arbitrary real bias q with a coin of arbitrary real bias p with minimum loss of entropy. We establish a lower bound that is strictly greater...
2 KAT-ML: An Interactive Theorem Proverfor Kleene Algebra with Tests (2008)
Kamal Aboul-hosn, Dexter Kozen
Abstract. KAT-ML is an interactive theorem prover for Kleene algebra withtests ( KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. We...
Halting and Equivalence of Schemes over Recursive Theories (2008)
Let Σ be a fixed first-order signature. In this note we consider the following decision problems. (i) Given a recursive ground theory T over Σ, a program scheme p over Σ, and input values...
Automating Proofs in Category Theory (2008)
Dexter Kozen, Christoph Kreitz
Abstract. We introduce a semi-automated proof system for basic category-theoretic reasoning. It is based on a first-order sequent calculus that captures the basic properties of categories, functors...
Myhill-Nerode relations on automatic systems and the completeness of Kleene algebra (2008)
Abstract. It is well known that finite square matrices over a Kleene algebra again form a Kleene algebra. This is also true for infinite matrices under suitable restrictions. One can use this fact to...
speci cation techniques � F.3.2 [Logics and Meanings of Programs]: Semantics of (2008)
We show that Kleene algebra with tests (KAT) subsumes propositional Hoare logic (PHL). Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by simple...
Nonlocal Flow of Control and Kleene Algebra with Tests (2008)
Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA), or the algebra of regular expressions, with Boolean algebra. It can model basic...
Nonlocal Flow of Control and Kleene Algebra with Tests (2008)
Kleene algebra with tests (KAT) is an equational system for program verification that combines Kleene algebra (KA), or the algebra of regular expressions, with Boolean algebra. It can model basic...
Local Variable Scoping and Kleene Algebra with Tests (2008)
Kamal Aboul-hosn, Dexter Kozen
Abstract. Most previous work on the semantics of programs with local state involves complex storage modeling with pointers and memory cells, complicated categorical constructions, or reasoning in the...
We investigate a family of inference problems on Markov models, where many sample paths are drawn from a Markov chain and partial information is revealed to an observer who attempts to reconstruct...
Separability in Domain Semirings (2008)
Abstract. First, we show with two examples that in test semirings with an incomplete test algebra a domain operation may or may not exist. Second, we show that two notions of separability in test...
Automating Proofs in Category Theory (2008)
Dexter Kozen, Christoph Kreitz, Eva Richter
Abstract. We introduce a semi-automated proof system for basic category-theoretic reasoning. It is based on a first-order sequent calculus that captures the basic properties of categories, functors...
It is shown that over any countable rst-order structure, IND programs with dictionaries accept
Separability in Domain Semirings (2008)
Dexter Kozen, Bernhard Möller, Copyright Dexter, Kozen Bernhard Möller, Dexter Kozen, ...
Abstract. First, we show with two examples that in test semirings with an incomplete test algebra a domain operation may or may not exist. Second, we show that two notions of separability in test...
speci cation techniques � F.3.2 [Logics and Meanings of Programs]: Semantics of (2008)
Programs|assertions � invariants � logics of programs � mechanical veri cation � pre- and postconditions�
Substructural logic and partial correctness (2008)
We formulate a noncommutative sequent calculus for partial correctness that subsumes propositional Hoare Logic. Partial correctness assertions are represented by intuitionistic linear implication. We...
On the Coalgebraic Theory of Kleene Algebra with Tests (2008)
We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of Rutten (1998) for Kleene algebra (KA) and Chen and Pucella (2003) for a limited version of KAT, resolving two...
On the Coalgebraic Theory of Kleene Algebra with Tests (2008)
We develop a coalgebraic theory of Kleene algebra with tests (KAT) along the lines of Rutten (1998) for Kleene algebra (KA) and Chen and Pucella (2003) for a limited version of KAT, resolving two...
In August, Dexter Kozen, Joseph Newton
Its purpose is to inform you of appointments, 1
Dexter Kozen, Michael I. Schwartzbach, Jens Palsberg
Subtyping in the presence of recursive types for the λ-calculus was studied by Amadio and Cardelli in 1991 [1]. In that paper they showed that the problem of deciding whether one recursive type is a...
We investigate a family of inference problems on Markov models, where many sample paths are drawn from a Markov chain and partial information is revealed to an observer who attempts to reconstruct...
Language-Based Security for Malicious Mobile Code (2008)
Fred B. Schneider, Dexter Kozen, Greg Morrisett, Andrew C. Myers
The need for secure computing first became apparent in the early 1970’s, when the high cost of hardware forced users to share standalone computers by time-multiplexing the processor. Concurrent...
Relational Semantics for Higher-Order (2008)
Functional Programs Kamal, Kamal Aboul-hosn, Dexter Kozen
Much work has been done on the semantics of programs with local state. Most of this work involves complex storage modeling with pointers and memory cells, complicated categorical constructions, and...
Local Variable Scoping and (2008)
Kleene Algebra With, Kamal Aboul-hosn, Dexter Kozen
Much work has been done on the semantics of programs with local state. The goal of most of the work in reasoning about state is to design a semantics that is fully abstract, where semantic...
The Boehm-Jacopini Theorem is False, Propositionally (2008)
Kozen, Dexter, Tseng, Wei-Lung (Dustin)
The Boehm-Jacopini theorem (Boehm and Jacopini, 1966) is a classical result of program schematology. It states that any deterministic flowchart program is equivalent to a while program. The theorem...
The Boehm-Jacopini Theorem is False, Propositionally (2008)
Kozen, Dexter, Tseng, Wei-Lung (Dustin)
The Boehm-Jacopini theorem (Boehm and Jacopini, 1966) is a classical result of program schematology. It states that any deterministic flowchart program is equivalent to a while program. The theorem...
Also in Proc. POPL'93, pages 419--428. Efficient Recursive Subtyping (2007)
Dexter Kozen, Jens Palsberg, Michael I. Schwartzbach
Subtyping in the presence of recursive types for the-calculus was studied by Amadio and Cardelli in 1991 [1]. In that paper they showed that the problem of deciding whether one recursive type is a...
David Harel, Dexter Kozen, Rohit Parikh
A process logic (PL) is defined that subsumes Pratt's process logic, Parikh's SOAPL, Nishimura's process logic, and Pnueli's Temporal Logic in expressiveness. The language of PL...
This paper addresses the problem of sending an encoded video stream over a channel of limited bandwidth. When there is insufficient bandwidth available, some data must be dropped. For many video...
Coinductive Proof Principles for Stochastic Processes (2007)
We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique....
Indefinite Summation and the Kronecker Delta (2007)
Indefinite summation, together with a generalized version of the Kronecker delta, provide a calculus for reasoning about various polynomial functions that arise in combinatorics, such as the Tutte,...
Indefinite Summation and the Kronecker Delta (2007)
Indefinite summation, together with a generalized version of the Kronecker delta, provide a calculus for reasoning about various polynomial functions that arise in combinatorics, such as the Tutte,...
Call a connected undirected graph (d,c)-colorable if there is a vertex coloring using at most c colors such that no two vertices of distance d or less have the same color. It is well known that...
Call a connected undirected graph (d,c)-colorable if there is a vertex coloring using at most c colors such that no two vertices of distance d or less have the same color. It is well known that...
Collective Inference on Markov Models for Modeling Bird Migration (2007)
Sheldon, Daniel, Elmohamed, M. A. Saleh, Kozen, Dexter
We investigate a family of inference problems on Markov models, where many sample paths are drawn from a Markov chain and partial information is revealed to an observer who attempts to reconstruct...
Collective Inference on Markov Models for Modeling Bird Migration (2007)
Sheldon, Daniel, Elmohamed, M. A. Saleh, Kozen, Dexter
We investigate a family of inference problems on Markov models, where many sample paths are drawn from a Markov chain and partial information is revealed to an observer who attempts to reconstruct...
Applications of Metric Coinduction (2007)
Kozen, Dexter, Ruozzi, Nicholas
Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One proves a coinduction step showing that some...
Applications of Metric Coinduction (2007)
Kozen, Dexter, Ruozzi, Nicholas
Metric coinduction is a form of coinduction that can be used to establish properties of objects constructed as a limit of finite approximations. One proves a coinduction step showing that some...
Call a connected undirected graph (d, c)-colorable if there is a vertex coloring using at most c colors such that no two vertices of distance d or less have the same color. It is well known that (1,...
Call a connected undirected graph (d, c)-colorable if there is a vertex coloring using at most c colors such that no two vertices of distance d or less have the same color. It is well known that (1,...
Relational semantics for higher-order programs (2006)
Kamal Aboul-hosn, Dexter Kozen
Abstract. Most previous work on the semantics of higher-order programs with local state involves complex storage modeling with pointers and memory cells, complicated categorical constructions, or...
Relational semantics for higher-order programs (2006)
Kamal Aboul-hosn, Dexter Kozen
Abstract. Most previous work on the semantics of higher-order programs with local state involves complex storage modeling with pointers and memory cells, complicated categorical constructions, or...
Coinductive proof principles for stochastic processes (2006)
Vol. 3 (4:8) 2007, pp. 1–14
D.: Local variable scoping and Kleene algebra with tests. In: RelMiCS (2006)
Kamal Aboul-hosn, Dexter Kozen
Abstract. We explore the power of relational semantics and equational reasoning in the style of Kleene algebra for analyzing programs with mutable, statically scoped local variables. We provide (i) a...
Relational Semantics of Local Variable Scoping (2005)
Aboul-Hosn, Kamal, Kozen, Dexter
Most previous work on the equivalence of programs in the presence of local state has involved intricate memory modeling and the notion of contextual (observable) equivalence. We show how relational...
Relational Semantics of Local Variable Scoping (2005)
Aboul-Hosn, Kamal, Kozen, Dexter
Most previous work on the equivalence of programs in the presence of local state has involved intricate memory modeling and the notion of contextual (observable) equivalence. We show how relational...
Coinductive Proof Principles for Stochastic Processes (2005)
We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique....
Coinductive Proof Principles for Stochastic Processes (2005)
We give an explicit coinduction principle for recursively-defined stochastic processes. The principle applies to any closed property, not just equality, and works even when solutions are not unique....
Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management (2005)
Kozen, Dexter, Ramanarayanan, Ganesh
There are many real-life examples of formal systems that support constructions or proofs, but that do not provide direct support for remembering them so that they can be recalled and reused in the...
Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management (2005)
Kozen, Dexter, Ramanarayanan, Ganesh
There are many real-life examples of formal systems that support constructions or proofs, but that do not provide direct support for remembering them so that they can be recalled and reused in the...
Publication/citation: A prooftheoretic approach to mathematical knowledge management (2005)
Dexter Kozen, Ganesh Ramanarayanan
There are many real-life examples of formal systems that support constructions or proofs, but that do not provide direct support for remembering them so that they can be recalled and reused in the...
Relational Semantics of Local Variable Scoping (2005)
Most previous work on the equivalence of programs in the presence of local state has involved intricate memory modeling and the notion of contextual (observable) equivalence. We show how relational...
Supporting workflow in a course management system (2005)
Chavdar Botev, Hubert Chao, Theodore Chao, Yim Cheng, Raymond Doyle, Sergey Grankin, ...
CMS is a secure and scalable web-based course management system developed by the Cornell University Computer Science Department. The system was designed to simplify, streamline, and automate many...
Second-Order Abstract Interpretation via Kleene Algebra (2004)
Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In this paper...
Kleene Algebra and Bytecode Verification (2004)
Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In a recent...
Second-Order Abstract Interpretation via Kleene Algebra (2004)
Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In this paper...
Kleene Algebra and Bytecode Verification (2004)
Most standard approaches to the static analysis of programs, such as the popular worklist method, are first-order methods that inductively annotate program points with abstract values. In a recent...
Toward the Automation of Category Theory (2004)
We introduce a sequent system for basic category-theoretic reasoning suitable for computer implementation. We illustrate its use by giving a complete formal proof that the functor categories...
Toward the Automation of Category Theory (2004)
We introduce a sequent system for basic category-theoretic reasoning suitable for computer implementation. We illustrate its use by giving a complete formal proof that the functor categories...
Natural Transformations as Rewrite Rules and Monad Composition (2004)
Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a...
Natural Transformations as Rewrite Rules and Monad Composition (2004)
Eklund et al. (2002) present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a...
Separability in Domain Semirings (2004)
Kozen, Dexter, Möller, Bernhard
First, we show with two examples that in test semirings with an incomplete test algebra a domain operation may or may not exist. Second, we show that two notions of separability in test semirings...
The FACS FACTS Team Newsletter Editor Paul Boca [ (2004)
Editorial Team, Jonathan Bowen, Judith Carlton, John Cooke, Kevin Lano, Mike Stannett, ...
FACS FACTS [ISSN: 0950-1231] is the newsletter of the BCS Specialist
Natural Transformations as Rewrite Rules and Monad Composition (2004)
Eklund et al. [6] present a graphical technique aimed at simplifying the verification of various category-theoretic constructions, notably the composition of monads. In this note we take a different...
Some results in dynamic model theory (2004)
First-order structures over a xed signature give rise to a family of trace-basedandrelational Kleene algebras with tests de ned in terms of Tarskian frames. A Tarskian frame is a Kripke frame whose...
Toward the automation of category theory (2004)
We introduce a sequent system for basic category-theoretic reasoning suitable for computer implementation. We illustrate its use by giving a complete formal proof that the functor categories Fun[C ×...
Kleene Algebra with Tests and the Static Analysis of Programs (2003)
We propose a general framework for the static analysis of programs based on Kleene algebra with tests (KAT). We show how KAT can be used to statically verify compliance with safety policies specified...
Kleene Algebra with Tests and the Static Analysis of Programs (2003)
We propose a general framework for the static analysis of programs based on Kleene algebra with tests (KAT). We show how KAT can be used to statically verify compliance with safety policies specified...
On the Representation of Kleene Algebras with Tests (2003)
We investigate conditions under which a given Kleene algebra with tests is isomorphic to an algebra of binary relations. Two simple separation properties are identified that, along with...
On the Representation of Kleene Algebras with Tests (2003)
We investigate conditions under which a given Kleene algebra with tests is isomorphic to an algebra of binary relations. Two simple separation properties are identified that, along with...
KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests (2003)
Aboul-Hosn, Kamal, Kozen, Dexter
KAT-ML is an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. We describe...
KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests (2003)
Aboul-Hosn, Kamal, Kozen, Dexter
KAT-ML is an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. We describe...
On the Complexity of the Horn Theory of REL (2003)
We show that the universal Horn theory of relational Kleene algebras is Pi-1-1-complete.
On the Complexity of the Horn Theory of REL (2003)
We show that the universal Horn theory of relational Kleene algebras is Pi-1-1-complete.
Language-Based Security for Malicious Mobile Code (2003)
Schneider, Fred B., Kozen, Dexter, Morrisett, Greg, Myers, Andrew
This report summarizes progress over the past year in developing language-based technologies for defending software systems against attacks from mobile code and system extensions.
KAT-ML: An interactive theorem prover for Kleene Algebra with Tests (2003)
Kamal Aboul-hosn, Dexter Kozen
Abstract. We describe an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds...
We show that the universal Horn theory of relational Kleene algebras is Π 1 1-complete. 1
Kleene algebras with tests and the static analysis of programs (2003)
We propose a general framework for the static analysis of programs based on Kleene algebra with tests (KAT). We show how KAT can be used to statically verify compliance with safety policies specified...
KAT-ML: An interactive theorem prover for Kleene Algebra with Tests (2003)
Kamal Aboul-hosn, Dexter Kozen
ABSTRACT. We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that...
KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests (2003)
Kamal Aboul-hosn, Dexter Kozen
We describe an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in the...
KAT-ML: An Interactive Theorem Prover for Kleene Algebra with Tests (2003)
Kamal Aboul-hosn, Dexter Kozen
We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system is designed to reflect the natural style of reasoning with KAT that one finds in...
Some Results in Dynamic Model Theory (2002)
First-order structures over a fixed signature S give rise to a family of trace-based and relational Kleene algebras with tests defined in terms of Tarskian frames. A Tarskian frame is a Kripke frame...
Some Results in Dynamic Model Theory (2002)
First-order structures over a fixed signature S give rise to a family of trace-based and relational Kleene algebras with tests defined in terms of Tarskian frames. A Tarskian frame is a Kripke frame...
Halting and Equivalence of Schemes over Recursive Theories (2002)
Let S be a fixed first-order signature. In this note we consider the following decision problems. (i) Given a recursive ground theory T over S, a program scheme p over S, and input values specified...
Halting and Equivalence of Schemes over Recursive Theories (2002)
Let S be a fixed first-order signature. In this note we consider the following decision problems. (i) Given a recursive ground theory T over S, a program scheme p over S, and input values specified...
Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests (2002)
In a recent paper of Mateev et al. (2001), a new technique for program analysis called fractal symbolic analysis was introduced and applied to verify the correctness of a series of source-level...
Equational Verification of Cache Blocking in LU Decomposition using Kleene Algebra with Tests (2002)
In a recent paper of Mateev et al. (2001), a new technique for program analysis called fractal symbolic analysis was introduced and applied to verify the correctness of a series of source-level...
On the Elimination of Hypotheses in Kleene Algebra with Tests (2002)
The validity problem for certain universal Horn formulas of Kleene algebra with tests (KAT) can be efficiently reduced to the equational theory. This reduction is known as elimination of hypotheses....
On the Elimination of Hypotheses in Kleene Algebra with Tests (2002)
The validity problem for certain universal Horn formulas of Kleene algebra with tests (KAT) can be efficiently reduced to the equational theory. This reduction is known as elimination of hypotheses....
Malicious Code Detection for Open Firmware (2002)
Adelstein, Frank, Stillerman, Matt, Kozen, Dexter
Malicious boot firmware is a largely unrecognized but significant security risk to our global information infrastructure. Since boot firmware executes before the operating system is loaded, it can...
Malicious Code Detection for Open Firmware (2002)
Adelstein, Frank, Stillerman, Matt, Kozen, Dexter
Malicious boot firmware is a largely unrecognized but significant security risk to our global information infrastructure. Since boot firmware executes before the operating system is loaded, it can...
Computational Inductive Definability (2002)
It is shown that over any countable first-order structure, IND programs with dictionaries accept exactly the Pi-1-1 relations. This extends a result of Harel and Kozen (1984) relating IND and Pi-1-1...
Computational Inductive Definability (2002)
It is shown that over any countable first-order structure, IND programs with dictionaries accept exactly the Pi-1-1 relations. This extends a result of Harel and Kozen (1984) relating IND and Pi-1-1...
On Two Letters versus Three (2002)
If A is a context-free language over a two-letter alphabet, then the set of all words obtained by sorting words in A and the set of all permutations of words in A are context-free. This is false over...
On Two Letters versus Three (2002)
If A is a context-free language over a two-letter alphabet, then the set of all words obtained by sorting words in A and the set of all permutations of words in A are context-free. This is false over...
Eager class initialization for Java (2002)
Abstract. We describe a static analysis method on Java bytecode to determine class initialization dependencies. This method can be used for eager class loading and initialization. It catches many...
On Two Letters versus Three (2002)
If A is a context-free language over a two-letter alphabet, then the set of all words obtained by sorting words in A and the set of all permutations of words in A are context-free. This is false over...
Equational verification of cache blocking in lu decomposition using kleene algebra with tests (2002)
In a recent paper of Mateev et al. (2001), a new technique for program analysis called fractal symbolic analysis was introduced and applied to verify the correctness of a series of source-level...
Eager Class Initialization for Java (2001)
Kozen, Dexter, Stillerman, Matt
We describe a static analysis method on Java bytecode to determine class initialization dependencies. This method can be used for eager class loading and initialization. It catches many...
Eager Class Initialization for Java (2001)
Kozen, Dexter, Stillerman, Matt
We describe a static analysis method on Java bytecode to determine class initialization dependencies. This method can be used for eager class loading and initialization. It catches many...
Kleene Algebra with Tests and Program Schematology (2001)
The theory of flowchart schemes has a rich history going back to Ianov (1960); see Manna (1974) for an elementary exposition. A central question in the theory of program schemes is scheme...
Kleene Algebra with Tests and Program Schematology (2001)
The theory of flowchart schemes has a rich history going back to Ianov (1960); see Manna (1974) for an elementary exposition. A central question in the theory of program schemes is scheme...
Automata on Guarded Strings and Applications (2001)
Guarded strings are like ordinary strings over a finite alphabet P, except that atoms of the free Boolean algebra on a set of atomic tests B alternate with the symbols of P. The regular sets of...
Automata on Guarded Strings and Applications (2001)
Guarded strings are like ordinary strings over a finite alphabet P, except that atoms of the free Boolean algebra on a set of atomic tests B alternate with the symbols of P. The regular sets of...
Intuitionistic Linear Logic and Partial Correctness (2001)
We formulate a Gentzen-style sequent calculus for partial correctness that subsumes propositional Hoare Logic. The system is a noncommutative Intuitionistic Linear Logic. We prove soundness and...
Intuitionistic Linear Logic and Partial Correctness (2001)
We formulate a Gentzen-style sequent calculus for partial correctness that subsumes propositional Hoare Logic. The system is a noncommutative Intuitionistic Linear Logic. We prove soundness and...
Kleene algebra with tests and program schematology (2001)
The theory of flowchart schemes has a rich history going back to Ianov [6]; see Manna [22] for an elementary exposition. A central question in the theory of program schemes is scheme equivalence....
Automata on guarded strings and applications (2001)
Guarded strings are like ordinary strings over a finite alphabet P, except that atoms of the free Boolean algebra on a set of atomic tests B alternate with the symbols of P. The regular sets of...
On the Completeness of Propositional Hoare Logic (2001)
. We investigate the completeness of Hoare logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a...
Myhill-Nerode Relations on Automatic Systems and the Completeness ofKleene Algebra (2000)
It is well known that finite square matrices over a Kleene algebra again form a Kleene algebra. This is also true for infinite matrices under suitable restrictions. One can use this fact to solve...
Myhill-Nerode Relations on Automatic Systems and the Completeness ofKleene Algebra (2000)
It is well known that finite square matrices over a Kleene algebra again form a Kleene algebra. This is also true for infinite matrices under suitable restrictions. One can use this fact to solve...
Certi cation of compiler optimizations using Kleene algebra with tests, in (2000)
Dexter Kozen, Maria-cristina Patron
Abstract. We use Kleene algebra with tests to verify a wide assortment ofcommon compiler optimizations, including dead code elimination, common subexpression elimination, copy propagation, loop...
On the completeness of propositional Hoare logic (2000)
Abstract. We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook’s proof are characterized propositionally. We give a...
Certification of Compiler Optimizations using Kleene Algebra with Tests (1999)
Patron, Maria-Cristina, Kozen, Dexter
We use Kleene algebra with tests to verify a wide assortment of common compiler optimizations, including dead code elimination, common subexpression elimination, copy propagation, loop hoisting,...
Certification of Compiler Optimizations using Kleene Algebra with Tests (1999)
Patron, Maria-Cristina, Kozen, Dexter
We use Kleene algebra with tests to verify a wide assortment of common compiler optimizations, including dead code elimination, common subexpression elimination, copy propagation, loop hoisting,...
On the Completeness of Propositional Hoare Logic (1999)
We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness...
On the Completeness of Propositional Hoare Logic (1999)
We investigate the completeness of Hoare Logic on the propositional level. In particular, the expressiveness requirements of Cook's proof are characterized propositionally. We give a completeness...
On Hoare Logic, Kleene Algebra, and Types (1999)
We show that propositional Hoare logic is subsumed by the type calculus of typed Kleene algebra augmented with subtypes and typecasting. Assertions are interpreted as typecast operators. Thus...
On Hoare Logic, Kleene Algebra, and Types (1999)
We show that propositional Hoare logic is subsumed by the type calculus of typed Kleene algebra augmented with subtypes and typecasting. Assertions are interpreted as typecast operators. Thus...
Language-Based Security (1999)
Security of mobile code is a major issue in today's global computing environment. When you download a program from an untrusted source, how can you be sure it will not do something undesirable? In...
Language-Based Security (1999)
Security of mobile code is a major issue in today's global computing environment. When you download a program from an untrusted source, how can you be sure it will not do something undesirable? In...
Parikh's Theorem in Commutative Kleene Algebra (1999)
Parikh's Theorem says that the commutative image of every context free language is the commutative image of some regular set. Pilling has shown that this theorem is essentially a statement about...
Parikh's Theorem in Commutative Kleene Algebra (1999)
Parikh's Theorem says that the commutative image of every context free language is the commutative image of some regular set. Pilling has shown that this theorem is essentially a statement about...
On Hoare logic, Kleene algebra, and types (1999)
We show that propositional Hoare logic is subsumed by the type calculus of typed Kleene algebra augmented with subtypes and typecasting. Assertions are interpreted as typecast operators. Thus...
Certification of Compiler Optimizations using Kleene Algebra with Tests (1999)
Maria-cristina Patron, Dexter Kozen
We use Kleene algebra with tests to verify a wide assortment of common compiler optimizations, including dead code elimination, common subexpression elimination, copy propagation, loop hoisting,...
Language-Based Security (1999)
. Security of mobile code is a major issue in today's global computing environment. When you download a program from an untrusted source, how can you be sure it will not do something...
On Hoare Logic, Kleene Algebra, and Types (1999)
We show that propositional Hoare logic is subsumed by the type calculus of typed Kleene algebra augmented with subtypes and typecasting. Assertions are interpreted as typecast operators. Thus...
Language-based security (1999)
Abstract. Security of mobile code is a major issue in today's global computing environment. When you download a program from an untrusted source, how can you be sure it will not do something...
On Hoare Logic and Kleene Algebra with Tests (1998)
We show that Kleene algebra with tests subsumes propositional Hoare logic. Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by ordinary...
On Hoare Logic and Kleene Algebra with Tests (1998)
We show that Kleene algebra with tests subsumes propositional Hoare logic. Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by ordinary...
Language-Based Security for Malicious Mobile Code (1998)
Schneider, Fred B., Kozen, Dexter, Morrisett, Greg, Myers, Andrew
This report summarizes progress over the past year in developing language-based technologies for defending software systems against attacks from mobile code and system extensions. The approach...
Language-Based Security for Malicious Mobile Code (1998)
Schneider, Fred B., Kozen, Dexter, Morrisett, Greg, Myers, Andrew
Report summarizes progress over the past year in developing language-based technologies for defending software systems against attacks from mobile code and system extensions.
In previous work we have found it necessary to argue that certain theorems of Kleene algebra hold even when the symbols are interpreted as nonsquare matrices. In this note we define and investigate...
In previous work we have found it necessary to argue that certain theorems of Kleene algebra hold even when the symbols are interpreted as nonsquare matrices. In this note we define and investigate...
Efficient Code Certification (1998)
We introduce a simple and efficient approach to the certification of compiled code. We ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack...
Efficient Code Certification (1998)
We introduce a simple and efficient approach to the certification of compiled code. We ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack...
E cient code certi cation (1998)
We introduce a simple and e cient approach to the certi cation of compiled code. We ensure a basic but nontrivial level of code safety, including control ow safety, memory safety, and stack safety....
Efficient Code Certification (1998)
We introduce a simple and efficient approach to the certification of compiled code. We ensure a basic but nontrivial level of code safety, including control flow safety, memory safety, and stack...
On Hoare Logic and Kleene Algebra with Tests (1998)
We show that Kleene algebra with tests subsumes propositional Hoare logic. Thus the specialized syntax and deductive apparatus of Hoare logic are inessential and can be replaced by ordinary...
In previous work we have found it necessary to argue that certain theorems of Kleene algebra hold even when the symbols are interpreted as nonsquare matrices. In this note we define and investigate...
A Theory of Interleavers (1997)
Andrews, Kenneth, Heegard, Chris, Kozen, Dexter
An interleaver is a hardware device commonly used in conjunction with error correcting codes to counteract the effect of burst errors. Interleavers are in widespread use and much is known about them...
A Theory of Interleavers (1997)
Andrews, Kenneth, Heegard, Chris, Kozen, Dexter
An interleaver is a hardware device commonly used in conjunction with error correcting codes to counteract the effect of burst errors. Interleavers are in widespread use and much is known about them...
On the Complexity of Reasoning in Kleene Algebra (1997)
We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra equational assumptions $E$; that is, the complexity of deciding the validity of...
On the Complexity of Reasoning in Kleene Algebra (1997)
We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra equational assumptions $E$; that is, the complexity of deciding the validity of...
Kleene algebra with tests (1997)
Abstract. We investigate conditions under which a given Kleene algebra with tests is isomorphic to an algebra of binary relations. Two simple separation properties are identified that, along with...
A Theory of Interleavers (1997)
Kenneth Andrews, Chris Heegard, Dexter Kozen
An interleaver is a hardware device commonly used in conjunction with error correcting codes to counteract the effect of burst errors. Interleavers are in widespread use and much is known about them...
Computing the Newtonian Graph (1997)
Introduction Following Smale (1985), we define the Newtonian vector field of a polynomial f 2 C [z] by N f (z) = \Gammaf (z)=f 0 (z). The name is derived from Newton's method for root...
On the Complexity of Reasoning in Kleene Algebra (1997)
We study the complexity of reasoning in Kleene algebra and *-continuous Kleene algebra in the presence of extra equational assumptions E; that is, the complexity of deciding the validity of universal...
On the complexity of reasoning in Kleene algebra (1997)
We study the complexity of reasoning in Kleene algebra and-continuous Kleene algebra in the presence of extra equational assumptions E; that is, the complexity of deciding the validity of universal...
The Complexity of Kleene Algebra with Tests (1996)
Cohen, Ernie, Kozen, Dexter, Smith, Frederick
Kleene algebras with tests provide a natural framework for equational specification and verification. Kleene algebras with tests and related systems have been used successfully in basic safety...
The Complexity of Kleene Algebra with Tests (1996)
Cohen, Ernie, Kozen, Dexter, Smith, Frederick
Kleene algebras with tests provide a natural framework for equational specification and verification. Kleene algebras with tests and related systems have been used successfully in basic safety...
Kleene Algebra with Tests: Completeness and Decidability (1996)
Kozen, Dexter, Smith, Frederick
Kleene algebras with tests provide a rigorous framework for equational specification and verification. They have been used successfully in basic safety analysis, source-to-source program...
Kleene Algebra with Tests: Completeness and Decidability (1996)
Kozen, Dexter, Smith, Frederick
Kleene algebras with tests provide a rigorous framework for equational specification and verification. They have been used successfully in basic safety analysis, source-to-source program...
Some Notes on Rational Spaces (1996)
Set constraints are inclusions between expressions denoting set of ground terms over a finitely ranked alphabet $\Sigma$. Rational spaces are topological spaces obtained as spaces of runs of...
Some Notes on Rational Spaces (1996)
Set constraints are inclusions between expressions denoting set of ground terms over a finitely ranked alphabet $\Sigma$. Rational spaces are topological spaces obtained as spaces of runs of...
Kleene algebra with tests and commutativity conditions (1996)
We give an equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one...
Kleene algebra with tests and commutativity conditions (1996)
We give an equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one...
Some notes on rational spaces (1996)
Abstract. Set constraints are inclusions between expressions denoting sets of ground terms over a finite ranked alphabet #. Rational spaces are topological spaces obtained as spaces of runs of...
Tarskian set constraints (1996)
Robert Givan, Dexter Kozen, David Mcallester, Carl Witty
Abstract: We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the...
The Complexity of Kleene Algebra with Tests (1996)
Ernie Cohen, Dexter Kozen, Frederick Smith
Kleene algebras with tests provide a natural framework for equational specification and verification. Kleene algebras with tests and related systems have been used successfully in basic safety...
Kleene Algebra with Tests: Completeness and Decidability (1996)
. Kleene algebras with tests provide a rigorous framework for equational specification and verification. They have been used successfully in basic safety analysis, source-to-source program...
Tarskian Set Constraints (1996)
Robert Givan, Robert Givan, David Mcallester, David Mcallester, Carl Witty, Carl Witty, ...
We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning...
Tarskian Set Constraints (1996)
Robert Givan, Dexter Kozen, David Mcallester, Carl Witty
: We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning...
Tarskian Set Constraints (1996)
David Mcallester Att, David A. Mcallester, Robert Givan, Carl Witty, Dexter Kozen
We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning...
A Complete Gentzen-Style Axiomatization for Set Constraints (1996)
. Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we...
Kleene Algebra with Tests: Completeness and Decidability (1996)
. Kleene algebras with tests provide a rigorous framework for equational specification and verification. They have been used successfully in basic safety analysis, source-to-source program...
Tarskian Set Constraints (1996)
David A. McAllester, Robert Givan, Carl Witty, D. Kozen, Dexter Kozen
We investigate set constraints over set expressions with Tarskian functional and relational operations. Unlike the Herbrand constructor symbols used in recent set constraint formalisms, the meaning...
On Regularity-Preserving Functions (1995)
We give a characterization of regularity-preserving functions.
On Regularity-Preserving Functions (1995)
We give a characterization of regularity-preserving functions.
Efficient Algorithms for Optimal Video Transmission (1995)
Kozen, Dexter, Minsky, Yaron, Smith, Brian
This paper addresses the problem of sending an encoded video stream over a channel of limited bandwidth. When there is insufficient bandwidth available, some data must be dropped. For many video...
A Complete Gentzen-style Axiomatization for Set Constraints (1995)
Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we provide...
Efficient Algorithms for Optimal Video Transmission (1995)
Kozen, Dexter, Minsky, Yaron, Smith, Brian
This paper addresses the problem of sending an encoded video stream over a channel of limited bandwidth. When there is insufficient bandwidth available, some data must be dropped. For many video...
A Complete Gentzen-style Axiomatization for Set Constraints (1995)
Set constraints are inclusion relations between expressions denoting sets of ground terms over a ranked alphabet. They are the main ingredient in set-based program analysis. In this paper we provide...
Rational Spaces and Set Constraints (1995)
Set constraints are inclusions between expressions denoting sets of ground terms. They have been used extensively in program analysis and type inference. In this paper we investigate the topological...
Rational Spaces and Set Constraints (1995)
Set constraints are inclusions between expressions denoting sets of ground terms. They have been used extensively in program analysis and type inference. In this paper we investigate the topological...
Decidability of systems of set constraints with negative constraints (1995)
Alexander Aiken, Alexander Aiken, Dexter Kozen, Dexter Kozen
is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent publications in the BRICS Report Series. Copies...
Efficient Algorithms for Optimal Video Transmission (1995)
This paper addresses the problem of sending an encoded video stream over a channel of limited bandwidth. When there is insufficient bandwidth available, some data must be dropped. For many video...
Decidability of Systems of Set Constraints with Negative Constraints (1995)
Alexander Aiken, Dexter Kozen, Ed Wimmers
Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general...
On Regularity-Preserving Functions (1995)
Boolean transition matrix of an automaton for A. This is the square Boolean matrix \Delta indexed by states of the automaton with 1 in position uv iff the automaton contains a transition u a \Gamma!...
Decidability of Systems of Set Constraints with Negative Constraints (1995)
Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general...
Rational Spaces and Set Constraints (1995)
this paper we investigate the topological structure of the spaces of solutions to systems of set constraints. We identify a family of topological spaces called rational spaces, which formalize the...
Set Constraints and Logic Programming (1995)
this paper we describe a constraint logic programming language clp(sc) over set constraints in the style of Jaffar and Lassez [17]. The language subsumes ordinary logic programs over an Herbrand...
Efficient Recursive Subtyping (1995)
Dexter Kozen, Jens Palsberg, Michael I. Schwartzbach
Subtyping in the presence of recursive types for the -calculus was studied by Amadio and Cardelli in 1991 [1]. In that paper they showed that the problem of deciding whether one recursive type is a...
Nils Klarlund, Dexter Kozen, Pankaj Agarwal, Andrew Goldberg, Ketan Mulmuley, Eric Allender, ...
Rabin conditions are a general class of properties of infinite sequences that encompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper, we introduce a...
Decidability of systems of set constraints with negative constraints (1995)
Dexter Kozen, Dexter Kozen, Alexander Aiken, Alexander Aiken
Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy. See back inner page for a list of recent...
[ii] Chicago Journal of Theoretical Computer Science 1995-3Rabin Measures (1995)
Pankaj Agarwal, Andrew Goldberg, Ketan Mulmuley, Eric Allender, Georg Gottlob, Gil Neiger, ...
Published one article at a time in LATEX source form on the Internet. Pagination
Logical Aspects of Set Constraints (1994)
Set constraints are inclusion relations between sets of ground terms over a ranked alphabet. They have been used extensively in program analysis and type inference. Here we present an equational...
Logical Aspects of Set Constraints (1994)
Set constraints are inclusion relations between sets of ground terms over a ranked alphabet. They have been used extensively in program analysis and type inference. Here we present an equational...
Efficient Average-Case Algorithms for the Modular Group (1994)
The modular group occupies a central position in many branches of mathematical sciences. In this paper we give average polynomial-time algorithms for the unbounded and bounded membership problems for...
Efficient Resolution of Singularities of Plane Curves (1994)
We give a new algorithm for resolving singularities of plane curves. The algorithm is polynomial time in the bit complexity model, does not require factorization, and works over the rationals or...
Efficient Average-Case Algorithms for the Modular Group (1994)
The modular group occupies a central position in many branches of mathematical sciences. In this paper we give average polynomial-time algorithms for the unbounded and bounded membership problems for...
Efficient Resolution of Singularities of Plane Curves (1994)
We give a new algorithm for resolving singularities of plane curves. The algorithm is polynomial time in the bit complexity model, does not require factorization, and works over the rationals or...
Set Constaints and Logic Programming (1994)
Set constraints are inclusion relations between expressions denoting sets of ground terms over a randed alphabet. They are the main ingredient in set-based program analysis[3,4,12,13,17,20,21,22,26]....
Set Constaints and Logic Programming (1994)
Set constraints are inclusion relations between expressions denoting sets of ground terms over a randed alphabet. They are the main ingredient in set-based program analysis[3,4,12,13,17,20,21,22,26]....
Decomposition of Algebraic Functions (1994)
Kozen, Dexter, Landau, Susan, Zippel, Richard
Functional decomposition--whether a function $f(x)$ can be written as a composition of functions $g(h(x))$ in a nontrivial way--is an important primitive in symbolic computation systems. The problem...
Decomposition of Algebraic Functions (1994)
Kozen, Dexter, Landau, Susan, Zippel, Richard
Functional decomposition--whether a function $f(x)$ can be written as a composition of functions $g(h(x))$ in a nontrivial way--is an important primitive in symbolic computation systems. The problem...
Efficient Average-Case Algorithms for the Modular Group (1994)
Jin-yi Cai, Wolfgang H. Fuchs, Dexter Kozen, Zicheng Liu
The modular group occupies a central position in many branches of mathematical sciences. In this paper we give average polynomial-time algorithms for the unbounded and bounded membership problems for...
Efficient inference of partial types (1994)
Dexter Kozen, Jens Palsberg, Michael I. Schwartzbach
Partial types for the-calculus were introduced by Thatte in 1988 [8] as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. In that...
Efficient Resolution of Singularities of Plane Curves (1994)
. We give a new algorithm for resolving singularities of plane curves. The algorithm is polynomial time in the bit complexity model, does not require factorization, and works over Q or finite fields....
A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events (1994)
We give a finitary axiomatization of the algebra of regular events involving only equations and equational implications. Unlike Salomaa 's axiomatizations, the axiomatization given here is sound...
Efficient Inference of Partial Types (1994)
Dexter Kozen, Jens Palsberg, Michael I. Schwartzbach
Partial types for the -calculus were introduced by Thatte in 1988 [8] as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. In that...
Optimal Bounds for the Change-Making Problem (1994)
The change-making problem is the problem of representing a given value with the fewest coins possible. We investigate the problem of determining whether the greedy algorithm produces an optimal...
Decomposition of Algebraic Functions (1994)
Dexter Kozen, Susan Landau, Richard Zippel
. Functional decomposition---whether a function f(x) can be written as a composition of functions g(h(x)) in a nontrivial way---is an important primitive in symbolic computation systems. The problem...
Efficient Average-Case Algorithms for the Modular Group (1994)
Jin-yi Cai, Wolfgang H. Fuchs, Dexter Kozen, Zicheng Liu
The modular group occupies a central position in many branches of mathematical sciences. In this paper we give average polynomial-time algorithms for the unbounded and bounded membership problems for...
Efficient inference of partial types (1994)
Dexter Kozen, Michael I. Schwartzbach, Jens Palsberg
Partial types for the λ-calculus were introduced by Thatte in 1988 [3] as a means of typing objects that are not typable with simple types,such as heterogeneous lists and persistent data. In that...
Efficient inference of partial types (1994)
Dexter Kozen, Jens Palsberg, Michael I. Schwartzbach
Partial types for the λ-calculus were introduced by Thatte in 1988 [8] as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. In that...
Computing the Newtonian Graph (Extended abstract) (1993)
Kozen, Dexter, Stefansson, Kjartan
A polynomial $f\in \complex[z]$ defines a vector field $N_f(z) = -f(z)/f'(z)$ on $\complex$. Certain degenerate curves of flow in $N_f$ give the edges of the Newtonian graph, as defined by...
Computing the Newtonian Graph (Extended abstract) (1993)
Kozen, Dexter, Stefansson, Kjartan
A polynomial $f\in \complex[z]$ defines a vector field $N_f(z) = -f(z)/f'(z)$ on $\complex$. Certain degenerate curves of flow in $N_f$ give the edges of the Newtonian graph, as defined by...
Decidability of Systems of Set Constraints with Negative Constraints (1993)
Aiken, Alexander, Kozen, Dexter, Wimmers, Ed
Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general...
Decidability of Systems of Set Constraints with Negative Constraints (1993)
Aiken, Alexander, Kozen, Dexter, Wimmers, Ed
Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. Recently, several algorithms for solving general...
The Complexity of Set Constraints (1993)
Aiken, Alexander, Kozen, Dexter, Vardi, Moshe, Wimmers, Ed
Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. We present several results on the computational...
The Complexity of Set Constraints (1993)
Aiken, Alexander, Kozen, Dexter, Vardi, Moshe, Wimmers, Ed
Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. We present several results on the computational...
Efficient Recursive Subtyping (1993)
Dexter Kozen, Jens Palsberg, Michael I. Schwartzbach
Subtyping in the presence of recursive types for the -calculus was studied by Amadio and Cardelli in 1991 [1]. In that paper they showed that the problem of deciding whether one recursive type is a...
The Complexity of Set Constraints (1993)
Alexander Aiken, Dexter Kozen, Moshe Vardi, Ed Wimmers
. Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. We present several results on the computational...
Logical Aspects of Set Constraints (1993)
. Set constraints are inclusion relations between sets of ground terms over a ranked alphabet. They have been used extensively in program analysis and type inference. Here we present an equational...
The Complexity of Set Constraints (1993)
Alexander Aiken, Dexter Kozen, Moshe Vardi, Ed Wimmers
. Set constraints are relations between sets of terms. They have been used extensively in various applications in program analysis and type inference. We present several results on the computational...
Efficient Recursive Subtyping (1993)
Dexter Kozen, Jens Palsberg, Michael I. Schwartzbach
Subtyping in the presence of recursive types for the -calculus was studied by Amadio and Cardelli in 1991 [1]. In that paper they showed that the problem of deciding whether one recursive type is a...
Action algebras have been proposed by Pratt [22] as an alternative to Kleene algebras [8, 9]. Their chief advantage over Kleene algebras is that they form a finitely-based equational variety, so the...
On the Myhill-Nerode Theorem for Trees (1992)
Science Department, Cornell University, Ithaca, New York 14853, USA mention of the equivalence of the tree analogs of (i) and (ii) seems to be by Brainerd [2, 3] and Eilenberg and Wright [4],...
Efficient Inference of Partial Types (1992)
Jens Palsberg, Michael I. Schwartzbach, Dexter Kozen, Dexter Kozen
Partial types for the -calculus were introduced by Thatte in 1988 [8] as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. In that...
Partial Automata and Finitely Generated Congruences: An Extension of Nerode's Theorem (1992)
Let T \Sigma be the set of ground terms over a finite ranked alphabet \Sigma. We define partial automata on T \Sigma and prove that the finitely generated congruences on T \Sigma are in one-to-one...
Rabin Measures and Their Applications to Fairness and Automata Theory (1991)
Rabin conditions are general class of properties of infinite sequences that emcompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper we show how to...
Rabin Measures and Their Applications to Fairness and Automata Theory (1991)
Rabin conditions are general class of properties of infinite sequences that emcompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper we show how to...
A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events (1990)
We give a finite axiomatization of the algebra of regular events involving only universal Horn formulas. Unlike Salomaa's axiomatizations, ours is sound for all interpretations over Kleene algebras.
On Kleene Algebras and Closed Semirings (1990)
Kleene algebras are an important class of algebraic structures that arise in diverse areas of computer science: program logic and semantics, relational algebra, automata theory, and the design and...
A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events (1990)
We give a finite axiomatization of the algebra of regular events involving only universal Horn formulas. Unlike Salomaa's axiomatizations, ours is sound for all interpretations over Kleene algebras.
On Kleene Algebras and Closed Semirings (1990)
Kleene algebras are an important class of algebraic structures that arise in diverse areas of computer science: program logic and semantics, relational algebra, automata theory, and the design and...
Parallel Resultant Computation (1990)
Ierardi, Doug J., Kozen, Dexter
A resultant is a purely algebraic criterion for determining when a finite collection of polynomials have a common zero. It has been shown to be a useful tool in the design of efficient parallel and...
Parallel Resultant Computation (1990)
Ierardi, Doug J., Kozen, Dexter
A resultant is a purely algebraic criterion for determining when a finite collection of polynomials have a common zero. It has been shown to be a useful tool in the design of efficient parallel and...
On Kleene Algebras and Closed Semirings (1990)
Kleene algebras are an important class of algebraic structures that arise in diverse areas of computer science: program logic and semantics, relational algebra, automata theory, and the design and...
On Kleene algebras and closed semirings (1990)
Kleene algebras are an important class of algebraic structures that arise in diverse areas of computer science: program logic and semantics, relational algebra, automata theory, and the design and...
Definability with Bounded Number of Bound Variables (1989)
A theory satisfies the k-variable property if every first-order formula is equivalent to a formula with at most k bound variables (possibly reused). Gabbay has shown that a model of temporal logic...
Definability with Bounded Number of Bound Variables (1989)
A theory satisfies the k-variable property if every first-order formula is equivalent to a formula with at most k bound variables (possibly reused). Gabbay has shown that a model of temporal logic...
A finite model theorem for the propositional µ-calculus (1988)
We prove a finite model theorem and infinitary completeness result for the propositional µ-calculus. The construction establishes a link between finite model theorems for propositional program...
Functional Decomposition of Polynomials (1987)
Von Zur Gathen, Joachim, Kozen, Dexter, Landau, Susan
ABSTRACT NOT AVAILABLE
Functional Decomposition of Polynomials (1987)
Von Zur Gathen, Joachim, Kozen, Dexter, Landau, Susan
ABSTRACT NOT AVAILABLE
On Teaching Left-Handed Children to Write (1987)
It is argued that the handwriting method commonly taught to left-handed children is incorrect and harmful. The disadvantages of this method are noted, and a new method alleviating these disadvantages...
On Teaching Left-Handed Children to Write (1987)
It is argued that the handwriting method commonly taught to left-handed children is incorrect and harmful. The disadvantages of this method are noted, and a new method alleviating these disadvantages...
ALEX - an Alexical Programming Language (1987)
Kozen, Dexter, Teitelbaum, Tim, Chen, Wilfred Z., Field, John H., Pugh, William W., Vander Zanden, Bradley T.
ALEX is an experimental language for high-level parallel programming. It is a testbed for exploring various non-traditional ways of expressing algorithmic ideas, making extensive use of...
ALEX - an Alexical Programming Language (1987)
Kozen, Dexter, Teitelbaum, Tim, Chen, Wilfred Z., Field, John H., Pugh, William W., Vander Zanden, Bradley T.
ALEX is an experimental language for high-level parallel programming. It is a testbed for exploring various non-traditional ways of expressing algorithmic ideas, making extensive use of...
Definability with Bounded Number of Bound Variables (1987)
A theory satisfies the $k$-variable-property if every first-order formula is equivalent to a formula with at most $k$ bound variables (possibly reused). Gabbay has shown that a fixed time structure...
Definability with Bounded Number of Bound Variables (1987)
A theory satisfies the $k$-variable-property if every first-order formula is equivalent to a formula with at most $k$ bound variables (possibly reused). Gabbay has shown that a fixed time structure...
NC Algorithms for Comparability Graphs, Interval Graphs, and Unique Perfect Matchings (1986)
Kozen, Dexter, Vazirani, Umesh V., Vazirani, Vijay V.
Laszlo Lovasz recently posed the following problem: "Is there an NC algorithm for testing if a given graph has a unique perfect matching?" We present such an algorithm for bipartite graphs. We also...
NC Algorithms for Comparability Graphs, Interval Graphs, and Unique Perfect Matchings (1986)
Kozen, Dexter, Vazirani, Umesh V., Vazirani, Vijay V.
Laszlo Lovasz recently posed the following problem: "Is there an NC algorithm for testing if a given graph has a unique perfect matching?" We present such an algorithm for bipartite graphs. We also...
Polynomial Decomposition Algorithms (1986)
In a recent paper [BZ], Barton and Zippel examine the question of when a polynomial $f(x)$ over a field of characteristic 0 has a nontrivial decomposition $f(x)=g(h(x))$. They give two...
Polynomial Decomposition Algorithms (1986)
In a recent paper [BZ], Barton and Zippel examine the question of when a polynomial $f(x)$ over a field of characteristic 0 has a nontrivial decomposition $f(x)=g(h(x))$. They give two...
A zero-one law for logic with a fixed-point operator (1985)
Blass, Andreas, Gurevich, Yuri, Kozen, Dexter
The logic obtained by adding the least-fixed-point operator to first-order logic was proposed as a query language by Aho and Ullman (in "Proc. 6th ACM Sympos. on Principles of Programming Languages,"...
David Harel, Dexter Kozen, Jerzy Tiuryn
Dynamic Logic (DL) is a formal system for reasoning about programs. Traditionally, this has meant formalizing correctness specifications and proving rigorously that those specifications are met by a...
Conway, and Gerry Salton, on the occasion of Juris Hartmanis’s Turing Award celebration. (1978)
Juris Hartmanis, Juris Hartmanis, David Gries, John Hopcroft, Juris Hartmanis, Bob Constable, ...
Degrees granted 25 20 15 10 5 PhD’s Granted
First Order Predicate Logic Without Negation is NP-Complete (1977)
Techniques developed in the study of the complexity of finitely presented algebras are used to show that the problem of deciding validity of positive sentences in the language of first order...
First Order Predicate Logic Without Negation is NP-Complete (1977)
Techniques developed in the study of the complexity of finitely presented algebras are used to show that the problem of deciding validity of positive sentences in the language of first order...
Finitely Presented Algebras and the Polynomial Time Hiercharchy (1977)
Let $S_{n}(V_{n})=\{less than \Gamma, Q_{1}v_{1}\cdots Q_{k}v_{k} s \equiv j greater than | \Gamma$ is a finite presentation of $\cal A, Q_{1} \cdots Q_{k}$ is a string of quantifiers with $n$...
Finitely Presented Algebras and the Polynomial Time Hiercharchy (1977)
Let $S_{n}(V_{n})=\{less than \Gamma, Q_{1}v_{1}\cdots Q_{k}v_{k} s \equiv j greater than | \Gamma$ is a finite presentation of $\cal A, Q_{1} \cdots Q_{k}$ is a string of quantifiers with $n$...
Complexity of Finitely Presented Algebras (1976)
An algebra $\cal A$ is finitely presented if there is a finite set G of generator symbols, a finite set O of operator symbols, and a finite set $\Gamma$ of defining relations $x \equiv y$ where $x$...
Complexity of Finitely Presented Algebras (1976)
An algebra $\cal A$ is finitely presented if there is a finite set G of generator symbols, a finite set O of operator symbols, and a finite set $\Gamma$ of defining relations $x \equiv y$ where $x$...
On Parallelism in Turing Machines (1976)
A model of parallel computation based on a generalization of nondeterminism in Turing machines is introduced. Complexity classes //T(n)-TIME, //L(n)-SPACE, //LOGSPACE, //PTIME, etc. are defined for...
On Parallelism in Turing Machines (1976)
A model of parallel computation based on a generalization of nondeterminism in Turing machines is introduced. Complexity classes //T(n)-TIME, //L(n)-SPACE, //LOGSPACE, //PTIME, etc. are defined for...
Polynomial Decomposition Algorithms
We examine the question of when a polynomial f over a commutative ring has a nontrivial functional decomposition f = g ffi h. Previous algorithms [2, 3, 1] are exponential-time in the worst case,...