\section{Introduction}
The areas of Qualitative Reasoning about physical systems
\cite{QP-readings}, reasoning about action and state change
\cite{nmr-readings}, reactive, real-time computing
\cite{ieee-rt-issue} and concurrent programming languages
\cite{ccs,csp-book} are areas of inquiry that are fundamentally
about the same subject matter --- the representation, design and
analysis of continuous and discrete dynamical systems.  

Surprisingly, no robust, common analyses of this subject matter
have hitherto emerged, though these areas have independently been
the beneficiaries of vigorous investigation in the past
decade(s).  The area of reactive, real-time computing has put
forth the elegant idea of synchronous programming --- languages
for specifying and implementing reactive systems that interact
``instantaneously'' with their environment. The well-developed
languages in this family, such as \Esterel{}, \Lustre{} and
\Signal{}, enjoy remarkable mathematical, computational and
expressiveness properties.  The analysis of concurrency --- and,
in general, the programme of research into the foundations of
computing at the heart of theoretical computer science --- has
put forth several models for indeterminate, concurrent,
communicating systems. And it has developed a methodology for
research based on developing an ``algebra'' of processes, on
identifying primitive processes and combinators that are
definable in these models and that together (through ``full
abstraction'' results) characterize these models. 

The area of non-monotonic reasoning has identified the importance
of {\em defeasible} reasoning --- the possibly erroneous
``jumping to conclusions'' that is the inevitable consequence of
the lack of omniscience about a dynamic environment
characteristic of all finitary computational systems.  (And it
has highlighted the paucity of resources at our disposal in
attacking these fundamental problems of of {\em efficient}
reasoning in the face of (state) change. The more powerful
theories of non-monotonic inference remain hamstrung by
artificial model theories or impossibly hard computational
problems.) The area of Qualitative Physics has highlighted the
importance and centrality of explicit, compositional,
declarative, models for simulation, monitoring, diagnosis,
control and design of such dynamical systems.

The natural meeting ground for these hitherto non-confluent areas
of inquiry is logic --- the logic of time and change.  Our thrust
to this heartland is through the synthesis of (concurrent)
constraint programming (CCP) --- itself at the heart of the dual
logicism and proceduralism of computational logic --- with
synchronous programming. From the viewpoint of programming
language design, we do not claim that there is something profound
about the choice of CCP as our starting point.  Indeed we believe
that the theory of timed computation we develop is robust enough
to be applicable to other asynchronous models of computation.
However, we have found the notion of an underlying constraint
system to be a robust crutch to support our intuitions about the
design of powerful computational systems.

CCP is based on the simple idea of a collection of (possibly
distributed) agents communicating by imposing and checking pieces
of partial information --- constraints --- on shared variables.
Agents are not synchronized, the constraints posted accumulate
monotonically --- perhaps after arbitrary unbounded delay --- in
a (possibly mythical) shared store. The computational view is
thus asynchronous, monotonic and untimed; the logical view is in
terms of deduction in intuitionistic logic.

The fundamental move in the Timed Concurrent Constraint
Programming (\tcc{}) framework is to augment the ability of
constraint programming to detect ``positive information'' (``some
event is happening'', some constraint is derivable) with the
ability to detect {\em negative information} --- ``some event did
not happen'', some constraint was {\em not} derivable on
quiescence.  Such detection is at the heart of the notion of
time-outs that are crucial to reactive, real-time computation and
of the notion of ``closed world'' assumptions that are crucial to
reasoning with incomplete information and in the face of change.
It also causes the underlying logical view of computation to be
in terms of deduction in (fixed-point extensions of)
intuitionistic (linear-time) {\em temporal} logic.

In addition, \tcc{} incorporates a simple idea with its roots in
the work in Qualitative Reasoning on model-based simulation of
physical systems: the current and future can have no causal
impact on the past. Thus, once negative information is detected,
it is too late to change the state of affairs that led to the
event not happening; all that can be done is to set up for action
now and in the future.  This idea is instrumental in
circumventing the ``temporal paradoxes'' \cite{esterel} that
arise from the confusion between causality and temporality that
has hitherto seemed to be an integral part of the synchronous
approach to computing.  And it is at the heart of our
identification of a powerful form of ``safe'' default reasoning
that avoids the complicated mathematical and computational
properties of more general forms of non-monotonic reasoning.

This paper explores the expressive power of the \tcc{} paradigm.
The origin of the work in the integration of synchronous and
constraint programming is described.  The basic conceptual and
mathematical framework --- developed in the spirit of the
model-based approach characteristic of theoretical computer
science --- is reviewed.  We show that a range of constructs for
expressing timeouts, preemption and other complicated patterns
of temporal activity are expressible in the basic model and
language-framework.  Indeed, we present a single construct on
processes, definable in the language, that can simulate the
effect of other preemption constructs.  

We present \tgentzen{}, a concrete \tcc{} language instantiated
over the ``generic'' constraint system \Gentzen{} that underlies
``unification-free'' computation in (classical, intuitionistic,
linear) logic. Recall that the constraint system \herbrand{}
\cite{my-book} originates in the use of ``delayed instantiation''
of existentially quantified variables on the ``right hand side''
of a sequent system: in the query $\vdash \exists X.(p(X) \wedge
q(X))$ one may think of $p$ and $q$ as processes that dynamically
impose constraints on $X$. The task of the \herbrand{} constraint
system is to express and resolve equalities over uninterpreted
terms, through variations of the Herbrand-Martelli-Montanari
(first-order) unification algorithm.  In contrast, the constraint
system we name \Gentzen{} is concerned with solving the core
(incremental) inference problem that arises in computing with
formulas on the {\em left} hand side of sequents (e.g., $p(X),
\forall Y. p(Y) \rightarrow q(Y) \vdash a$). In brief, the ``tokens''
of the constraint system here are arbitrary (positive) atomic
formulas (possibly with ``eigen-variables''), and the inference
relation is that forced by the non-logical structural rules
(identity, cut, permutation, etc.). Thus the computational
problem is essentially a database lookup problem, in the face of
(1)~arbitrary tree-structured data, (2)~a monotonically
increasing database, (3)~universally quantified queries.
Somewhat surprisingly, this constraint system has already been
used heavily in implemented work in Qualitative Reasoning --- it
underlies the ``active database'' viewpoint for organizing
problem-solving systems developed by Sussman and his colleagues
in the 70's; see \cite{forbus-dekleer} for a recent expository
development.

Subsequently, we present solutions to several representative
reactive and synchronous programming problems in \tgentzen; also
we discuss how some common default inferencing techniques can be
represented. In a paper of this form, it is possible
only to select and treat a few representative examples.

No paper on programming techniques can be complete without
providing the reader with the ability to test and develop new
programs. We discuss and include a full working interpreter for
\tgentzen{}, written in \prolog{}, that can be used for running
these programs. It is short, under a hundred lines long, but
fully functional. 

\paragraph{Acknowledgements}
We gratefully acknowledge extended discussions on various aspects
of this work with Danny Bobrow, Jerry Burch, Adam Farquhar,
Markus Fromherz, Lalita Jategaonkar, John Lamping, Tim Lindholm,
Olivier Raiman, Mark Shirley, Brian Smith and Brian Williams.