Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Uday S. Reddy
Current activities I have completed a 4-year
term as the Head of Department in August 2008. I am looking forward
to renewing my research and teaching. Please do tell me about all
your latest exciting work!
Research Areas:
Functional programming, logic programming, object-oriented programming,
especially, programming with state.
Type systems, semantics and reasoning methods.
Constructive logic and type theory,
especially, linear logic.
Automated deduction, program transformation and synthesis.
Separation Logic is a recent development in programming logic which
has been applied by Peter O'Hearn to concurrency based on critical
sections as well as semaphores. In this paper, we go one step further
and apply it to fine-grained concurrency. We note that O'Hearn's
formulation of Concurrent Separation Logic is by and large applicable
to fine-grained concurrent programs with only minor adaptations.
However, proving substantial properties of such programs involves the
employment of sophisticated ``permissions'' frameworks so that different
processes can have different levels of access and exchange such
access. We illustrate these techniques by showing the correctness
proof of a concurrent garbage collector originally studied by Dijkstra
et al.
[ps file | pdf file]
Parametric limits (Brian P. Dunphy and Uday S. Reddy, to appear in
LICS 2004)
We develop a categorical model of polymorphic lambda calculi using a
notion called parametric limits, which extend the notion of limits in
categories to reflexive graphs of categories. We show that a number
of parametric models of polymorphism can be captured in this way. We
also axiomatize the structure of reflexive graphs needed for modelling
parametric polymorphism based on ideas of fibrations, and show that it
leads to proofs of representation results such as the initial algebra and
final coalgebra properties one expects in polymorphic lambda calculi.
[ps file]
Programming with the Mathematical and the Physical (Inaugural
lecture, May 6, 2003)
Slides from my Inaugural
Lecture. Reviews my work on the semantics of programming languages,
and discusses the dichotomy between mathematical and physical entities
that is faced in this work.
Correctness of data representations involving heap data structures
(with H. Yang, to appear in Science of Computer Programming)
While the semantics of local variables in programming languages is by
now well-understood, the semantics of pointer-addressed heap variables
is still an outstanding issue. In particular, the commonly assumed
relational reasoning principles for data representations have not been
validated in a semantic model of heap variables. In this paper, we
define a parametricity semantics for a Pascal-like language with
pointers and heap variables which gives such reasoning principles. It
is found that the correspondences between data representations are not
simply relations between states, but more intricate correspondences
that also need to keep track of visible locations whose pointers can
be stored and leaked.
[ps file |
earlier version in ESOP 2003]
Brian Dunphy's PhD Thesis
Parametricity as a notion of uniformity in reflexive graphs,
Department of Mathematics, University of Illinois, 2002.
[ ps file]
Hongseok Yang's PhD Thesis
Local reasoning for stateful programs, Department of Computer Science,
University of Illinois, 2001.
[ ps file]
On the Semantics of Refinement Calculi (with H. Yang, FOSSACS 2000)
Refinement calculi for imperative programs provide an integrated
framework for programs and specifications and allow one to develop
programs from specifications in a systematic fashion. The semantics
of these calculi has traditionally been defined in terms of predicate
transformers and poses several challenges in defining a state
transformer semantics in the denotational style. We define a novel
semantics in terms of sets of state transformers and prove it to be
isomorphic to multiplicative predicate transformers. This semantics
disagrees with the traditional semantics in some places and the
consequences of the disagreement are analyzed.
[ps file |
pdf file]
Parametric Sheaves for modelling store locality (with H.Yang)
In this paper, we bring together two important ideas in the semantics of
Algol-like imperative programming languages. One is that program phrases
act on fixed sets of storage locations. The second is that
the information of local variables is hidden from client programs.
This involves combining sheaf theory and parametricity
to produce new classes of sheaves. We define the semantics
of an Algol-like language using such sheaves and discuss the
reasoning principles validated by the semantics.
[ps file |
pdf file]
Objects and classes in Algol-like languages
(Information and Computation, 2002)
Many object-oriented languages used in practice descend from Algol.
With this motivation, we study the theoretical issues underlying such
languages via the theory of Algol-like languages. It is shown that
the basic framework of this theory extends cleanly and elegantly to
the concepts of objects and classes. An important idea that comes to
light is that classes are abstract data types, whose theory
corresponds to that of existential types. Equational and Hoare-like
reasoning methods, and relational parametricity provide powerful
formal tools for reasoning about Algol-like object-oriented programs.
[ps
file | pdf file]
]
Type Reconstruction for SCI, Part 2
(H. Huang and H. Yang, ICCL 98)
Syntactic Control of Interference (SCI) [Rey78] has long been studied
as a basis for interference-free programming, with cleaner reasoning
properties and semantics than traditional imperative languages. This
paper makes SCI-based languages more practical by introducing a revised
version of Huang and Reddy's type reconstruction system [HR96] with two
significant improvements. First, we eliminate the need for explicit
coercion operators in terms. Although this can lead to more complex
principal typings, we introduce some minor restrictions on the
inference system to keep the typings manageable. Second, we consider
adding let-bound polymorphism. Such a modification appears to be
nontrivial. We propose a new approach which addresses issues of both
polymorphism and interference control.
SCI can be adapted to a wide variety of languages, and
our techniques should be applicable to any such language with SCI-based
interference control.
[
ps file]
Imperative Lambda Calculus revisited
(Aug 97, with H. Yang)
Imperative Lambda Calculus is a type system designed to combine
functional and imperative programming features in an orthogonal
fashion without compromising the algebraic properties of functions.
It has been noted that the original system is too restrictive and
lacks the subject reduction property. We define a revised type system
that solves these problems using ideas from Reynolds's Syntactic
Control of Interference. We also extend it to handle Hindley-Milner
style polymorphism and devise type reconstruction algorithms. A
sophisticated constraint language is designed to formulate principal
types for terms.
[dvi file |
ps file]
When parametricity implies naturality
(Notes, July 97)
The issue of whether parametricity and naturality should be assumed
separately or whether parametricity automatically implies naturality
crops up in the parametricity semantics for
Algol (O'Hearn and Tennent, 1995; O'Hearn and Reynolds, 1997).
Intuitively, parametricity and naturality are trying to capture the
same idea of ``uniformity.'' So, it is not immediately clear why one
needs two theories of uniformity or whether one should find some
other theory that subsumes both parametricity and naturality.
The results here are meant to shed some light on the issue. We
use the framework of reflexive graphs from
(O'Hearn and Tennent, 1995) and add suitable conditions which
entail that parametricity implies naturality. Further, we show that
the semantics of Algol can be given in such a framework.
[dvi file |
ps file]
Semantics:
The language Idealized Algol+ is proposed as a foundation for
Algol-like object-oriented languages[Red98].
Objects with state form the foundation for a new semantics for
higher-order imperative programs without a global state
[Red96].
It has been proved fully abstract up to second order
[OR95]. An early semantic model for inheritance
in a global state framework is in [KR94] which
subsumes the conference version [Red88].
Type systems:
A type system allows the integration of functional and imperative
programming features without compromise
[SRI91]. A revised type system with better
properties appears in [SRI97].
See also
Vipin
Swarup's thesis.
Reynolds's Syntactic Control of Interference (SCI) has similar goals
and also aims to control unwanted interference through a type system.
We are
able to do type inference for SCI in
[HR96]. Here is the home page of
SCI and Linear Logic workshop.
Linear logic:
"Acceptors as values" explores functional programming applications for
Girard's linear logic
[Red91].
"Linear logic model of state"
[Red93a]
is the inspiration behind the new object-based semantics.
Object-oriented programming:
An attempt at a sane definition of core C++ is
here.
Illinois Concert C++
is a simple and powerful extension of C++ for
high-performance parallel computing
[CRPD96].
Logic Programming:
Typed Prolog is an implementation of Hindley-Milner typing for Prolog
[LR91].
An application of linear logic ideas to directional typing of concurrent
logic programs is found here
[Red93].
Directional typing of Prolog programs gives a handle on their
termination issues
[BLR92].
All this and much more in
T.K.Lakshman's thesis.
Program transformation/synthesis:
An overview of the Focus project, an experimental system for the
application of term-rewriting and automated deduction techniques for program
transformation, is in
[Red91a].
The theoretical underpinnings of these techniques is found in
[DR93].
Automated Deduction:
"Term-rewriting induction" is an induction method for rewrite systems
which justifies the erstwhile "inductionless" induction
[Red90].
But, induction on term orderings does better
[BRH94].
Term rewriting ideas and completion techniques are applied to
resolution theorem proving in
[BR92].
"Proof nets" help clean up the completeness issues
[BR96].
All this and more in
Francois Bronsard's thesis.
Linear Continuation Passing,
J. Berdine, P. W. O'Hearn, U. S. Reddy, H. Thielecke,
Higher Order and Symbolic Computation, 15(2/3):181--208,
September 2002.
Higher-order aspects of logic programming,
in R.Dyckhoff (ed), Extensions of Logic Programming,
LNAI Vol. 798, Springer-Verlag, 1994.
(Also) Extended Abstract in P.Van Hentenryck (ed),
Logic Programming: Eleventh International Conf., MIT Press,
1994. pp. 402-418.
Reduction techniques for first-order reasoning,
F.Bronsard and U.S.Reddy,
in M.Rusinowitch and J.L.Remy (eds), Conditional Term
rewriting systems, LNCS Vol. 656, Springer-Verlag, 1992, pp.
242-256.
A logical view of assignments,
V.Swarup and U.S.Reddy,
in J.P.Myers and M.J.O'Donnell (eds),
Constructivity in Computer Science, LNCS Vol. 613,
Springer-Verlag, 1992.
Assignments for applicative languages,
V.Swarup, U.S.Reddy and E.Ireland,
in R.J.M.Hughes (ed), FPCA 91,
LNCS Vol. 523, Springer-Verlag, 1991, pp. 192-214.