Arrow Research search

Author name cluster

Dexter Kozen

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

37 papers
2 author rows

Possible papers

37

CSL Conference 2025 Conference Paper

Classical Linear Logic in Perfect Banach Lattices

  • Pedro H. Azevedo de Amorim
  • Leon Witzman
  • Dexter Kozen

In recent years, researchers have proposed various models of linear logic with strong connections to measure theory, with probabilistic coherence spaces (PCoh) being one of the most prominent. One of the main limitations of the PCoh model is that it cannot interpret continuous measures. To overcome this obstacle, Ehrhard has extended PCoh to a category of positive cones and linear Scott-continuous functions and shown that it is a model of intuitionistic linear logic. In this work we show that the category PBanLat₁ of perfect Banach lattices and positive linear functions of norm at most 1 can serve the same purpose, with some added benefits. We show that PBanLat₁ is a model of classical linear logic (without exponential) and that PCoh embeds fully and faithfully in PBanLat₁ while preserving the monoidal and *-autonomous structures. Finally, we show how PBanLat₁ can be used to give semantics to a higher-order probabilistic programming language.

Details

Highlights Conference 2022 Conference Abstract

25 Years of KAT

  • Dexter Kozen

Kleene algegra with tests (KAT) is a system for equational reasoning about imperative programs. The system is based on Kleene algebra, the algebra of regular expressions. In this talk I will trace the origins of the system and survey past and recent results on expressiveness, decision complexity, and deductive completeness, along with various applications, including correctness of compiler optimizations and verification of packet switching networks.

Details

CSL Conference 2018 Conference Paper

The Ackermann Award 2018

  • Dexter Kozen
  • Thomas Schwentick

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2018 edition of the award.

Details

CSL Conference 2015 Conference Paper

The Ackermann Award 2015

  • Anuj Dawar
  • Dexter Kozen
  • Simona Ronchi Della Rocca

The eleventh Ackermann Award is presented at CSL'15 in Berlin, Germany. This year, again, the EACSL Ackermann Award is generously sponsored by the Kurt Gödel Society. Besides providing financial support for the Ackermann Award, the Kurt Gödel Society has also committed to inviting the recipients of the Award for a special lecture to be given to the Society in Vienna.

Details

CSL Conference 2013 Conference Paper

Kleene Algebra with Products and Iteration Theories

  • Dexter Kozen
  • Konstantinos Mamouras

We develop a typed equational system that subsumes both iteration theories and typed Kleene algebra in a common framework. Our approach is based on cartesian categories endowed with commutative strong monads to handle nondeterminism.

Details

MFCS Conference 2013 Conference Paper

Strong Completeness for Markovian Logics

  • Dexter Kozen
  • Radu Mardare
  • Prakash Panangaden

Abstract In this paper we present Hilbert-style axiomatizations for three logics for reasoning about continuous-space Markov processes (MPs): (i) a logic for MPs defined for probability distributions on measurable state spaces, (ii) a logic for MPs defined for sub-probability distributions and (iii) a logic defined for arbitrary distributions. These logics are not compact so one needs infinitary rules in order to obtain strong completeness results. We propose a new infinitary rule that replaces the so-called Countable Additivity Rule (CAR) currently used in the literature to address the problem of proving strong completeness for these and similar logics. Unlike the CAR, our rule has a countable set of instances; consequently it allows us to apply the Rasiowa-Sikorski lemma for establishing strong completeness. Our proof method is novel and it can be used for other logics as well.

Details

NeurIPS Conference 2007 Conference Paper

Collective Inference on Markov Models for Modeling Bird Migration

  • M. a. Elmohamed
  • Dexter Kozen
  • Daniel Sheldon

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 the sample paths. We present algo- rithms and hardness results for several variants of this problem which arise by re- vealing different information to the observer and imposing different requirements for the reconstruction of sample paths. Our algorithms are analogous to the clas- sical Viterbi algorithm for Hidden Markov Models, which finds the single most probable sample path given a sequence of observations. Our work is motivated by an important application in ecology: inferring bird migration paths from a large database of observations.

PDF Details

MFCS Conference 2006 Invited Paper

On the Representation of Kleene Algebras with Tests

  • Dexter Kozen

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 star-continuity, are sufficient for nonstandard relational representation. An algebraic condition is identified that is necessary and sufficient for the construction to produce a standard representation.

Details

MFCS Conference 1999 Conference Paper

Language-Based Security

  • Dexter Kozen

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 undesirable? In this paper I will discuss a particular approach to this problem called language-based security. In this approach, security information is derived from a program written in a high-level language during the compilation process and is included in the compiled object. This extra security information can take the form of a formal proof, a type annotation, or some other form of certificate or annotation. It can be downloaded along with the object code and automatically verified before running the code locally, giving some assurance against certain types of failure or unauthorized activity. The verifier must be trusted, but the compiler, code, and certificate need not be. Java bytecode verification is an example of this approach. I will give an overview of some recent work in this area, including a particular effort in which we are trying to make the production of certificates and the verification as efficient and invisible as possible.

Details

CSL Conference 1997 Conference Paper

Kleene Algebra with Tests: Completeness and Decidability

  • Dexter Kozen
  • Frederick Smith

Abstract 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 transformation, and concurrency control. We prove the completeness of the equational theory of Kleene algebra with tests and-continuous Kleene algebra with tests over language-theoretic and relational models. We also show decidability. Cohen's reduction of Kleene algebra with hypotheses of the form r =0 to Kleene algebra without hypotheses is simplified and extended to handle Kleene algebras with tests.

Details

FOCS Conference 1994 Conference Paper

Efficient Average-Case Algorithms for the Modular Group

  • Jin-Yi Cai
  • Wolfgang H. J. Fuchs
  • Dexter Kozen
  • Zicheng Liu 0001

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 finitely generated subgroups of the modular group. The latter result affirms a conjecture of Y. Gurevich (1990). >

Details

CSL Conference 1994 Conference Paper

Logical Aspects of Set Constraints

  • Dexter Kozen

Abstract 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 axiomatization of the algebra of set constraints. Models of these axioms are called termset algebras. They are related to the Boolean algebras with operators of Jónsson and Tarski. We also define a family of combinatorial models called topological term automata, which are essentially the term automata studied by Kozen, Palsberg, and Schwartzbach endowed with a topology such that all relevant operations are continuous. These models are similar to Kripke frames for modal or dynamic logic. We establish a Stone duality between termset algebras and topological term automata, and use this to derive a completeness theorem for a related multidimensional modal logic. Finally, we prove a small model property by filtration, and argue that this result contains the essence of several algorithms appearing in the literature on set constraints.

Details

CSL Conference 1994 Conference Paper

The Complexity of Set Constraints

  • Alexander Aiken
  • Dexter Kozen
  • Moshe Y. Vardi
  • Edward L. Wimmers

Abstract 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 complexity of solving systems of set constraints. The systems we study form a natural complexity hierarchy depending on the form of the constraint language.

Details

FOCS Conference 1992 Conference Paper

Efficient Inference of Partial Types

  • Dexter Kozen
  • Jens Palsberg
  • Michael I. Schwartzbach

Partial types for the lambda -calculus were introduced by Thatte (1988) as a means of typing objects that are not typable with simple types, such as heterogeneous lists and persistent data. He showed that type inference for partial types was semidecidable. Decidability remained open until O'Keefe and Wand gave an exponential time algorithm for type inference. The authors give an O(n/sup 3/) algorithm. The algorithm constructs a certain finite automaton that represents a canonical solution to a given set of type constraints. Moreover, the construction works equally well for recursive types. >

Details

MFCS Conference 1990 Invited Paper

On Kleene Algebras and Closed Semirings

  • Dexter Kozen

Abstract 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 analysis of algorithms. The literature contains at several inequivalent definitions of Kleene algebras and related algebraic structures [2, 13, 14, 5, 6, 1, 9, 7]. In this paper we establish some new relationships among these structures. Our main results are: •There is a Kleene algebra in the sense of [6] that is not *-continuous. •The categories of *-continuous Kleene algebras [5, 6], closed semirings [1, 9] and S-algebras [2] are strongly related by adjunctions. •The axioms of Kleene algebra in the sense of [6] are not complete for the universal Horn theory of the regular events. This refutes a conjecture of Conway [2, p. 103]. •Right-handed Kleene algebras are not necessarily left-handed Kleene algebras. This verifies a weaker version of a conjecture of Pratt [14].

Details

FOCS Conference 1985 Conference Paper

Algebraic Cell Decomposition in NC (Preliminary Version)

  • Dexter Kozen
  • Chee-Keng Yap

We give an algorithm to construct a cell decomposition of Rd, including adjacency information, defined by any given set of rational polynomials in d variables. The algorithm runs in single exponential parallel time, and in NC for fixed d. The algorithm extends a recent algorithm of Ben-Or, Kozen, and Reif for deciding the theory of real closed fields.

Details

FOCS Conference 1980 Conference Paper

Process Logic: Expressiveness, Decidability, Completeness

  • David Harel
  • Dexter Kozen
  • Rohit Parikh

We define a process logic PL that subsumes Pratt's process logic, Parikh's SOAPL, Nishimura's process logic, and Pnueli's Temporal Logic in expressiveness. The language of PL is an extension of the language of Propositional Dynamic Logic (PDL). We give a deductive system for PL which includes the Segerberg axioms for PDL and prove that it is complete. We also show that PL is decidable.

Details

FOCS Conference 1979 Conference Paper

Semantics of Probabilistic Programs

  • Dexter Kozen

Two complementary but equivalent semantic interpretations of a high level probabilistic programming language are given. One of these interprets programs as partial measurable functions on a measurable space. The other interprets programs as continuous linear operators on a Banach space of measures. It is shown how the ordered domains of Scott and others are embedded naturally into these spaces. Two general results about probabilistic programs are proved.

Details

FOCS Conference 1977 Conference Paper

Lower Bounds for Natural Proof Systems

  • Dexter Kozen

Two decidable logical theories are presented, one complete for deterministic polynomial time, one complete for polynomial space. Both have natural proof systems. A lower space bound of n/log(n) is shown for the proof system for the PTIME complete theory and a lower length bound of 2cn/log(n) is shown for the proof system for the PSPACE complete theory.

Details

FOCS Conference 1976 Conference Paper

On Parallelism in Turing Machines

  • Dexter Kozen

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 these machines in a way analogous to T(n)-TIME, L(n)-SPACE, LOGSPACE, PTIME, etc. for deterministic machines. It is shown that, given appropriate honesty conditions, L(n)-SPACE ⊆ //L(n)2-TIME T(n)-TIME ⊆ //log T(n)-SPACE //L(n)-SPACE ⊆ exp L(n)-TIME //T(n)-TIME ⊆ T(n)2-SPACE thus · · //EXPTIME = EXPSPACE //PSPACE = EXPTIME //PTIME = PSPACE //LOGSPACE = PTIME? = LOGSPACE That is, the deterministic hierarchy LOGSPACE ⊆ PTIME ⊆ PSPACE ⊆ EXPTIME ⊆. .. shifts by exactly one level when parallelism is introduced. We give a natural characterization of the polynomial time hierarchy of Stockmeyer and Meyer in terms of parallel machines. Analogous space hierarchies are defined and explored, and a generalization of Saviten's result NONDET-L(n)-SPACE ⊆ L(n)2-SPACE is given. Parallel finite automata are defined, and it is shown that, although they accept only regular sets, in general 22k states are necessary and sufficient to simulate a k-state parallel finite automaton deterministically.

Details