Three of my recent papers are now available on-line at
1) Clause-logical aspects of the Smyth powerdomain (with Bill Rounds)
In this paper we study the logical aspects of the Smyth powerdomain via
clausal theories. The clause-theoretic view leads to an unexpectedly
simple, operational, representation of the Smyth powerdomain. At the
heart of this representation is a hyperresolution rule, whose
completeness hinges upon a combinatorial lemma for the book-keeping of
intermediate clauses. These results are motivated by the need to
develop least fixed-point semantics for disjunctive logic programming.
We show that, indeed, the clause-theoretic representation of the Smyth
powerdomain provides a clean and correct fixed-point semantics for
disjunctive logic programs. Correctness is established by proving that
clauses in the fixed-point theory induced by a logic program coincide
with those that are logical consequences of the program.
The next two are not related to types; they are on automata theory
which some of you might be interested.
2) Automata, Boolean Matrices, and Ultimate Periodicity
This paper presents a Boolean-matrix based method to automata theory,
with an application to the study of regularity-preserving functions. A
new characterization of such functions is derived in terms of their
ultimate periodicity with respect to powers of Boolean matrices. This
characterization reveals the intrinsic algebraic nature of regularity
preserving functions. It facilitates a concise proof of known, as well
as previously unknown properties of regularity-preserving functions,
leading to the solution of the ``subtraction problem'' left open by
3) Periodic Functions for Finite Semigroups
This paper introduces the concept of ultimately periodic functions for
finite semigroups. Ultimately periodic functions are shown to be the
same as regularity-preserving functions in automata theory. This
characterization reveals the algebraic nature of regularity-preserving
functions. It makes it possible to prove properties of ultimately
periodic functions through automata-theoretic methods; some of the
properties do not seem to have direct proofs in semigroup theory.
Comments are welcome.