Prof. Uday S. Reddy
School of Computer Science,
University of Birmingham.
Appointments See my
Diary
as well as
School diary.
Email me with suggested times at u.s.reddy at the School email address
(cs.bham.ac.uk), +44 121 414 2740.
Current activities I have completed a 4year
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!
Other affiliations:
Formerly at the
Department of Computer Science,
University of Illinois.
I had been a visiting professor at
Queen Mary, University of
London, and spent a sabbatical leave at
Imperial College and
University of Glasgow.
Research Areas:
Functional programming, logic programming, objectoriented 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.
Research
Discussions

Teaching

Recent papers/manuscripts
The Essence of Reynolds
(with Stephen Brookes and
Peter O'Hearn,
POPL 2014.)
John Reynolds (19352013) was a pioneer of programming languages
research. In this paper we pay tribute to the man, his ideas,
and his influence.[PDF 
Presentation at POPL]
Logical Relations and Parametricity: A Reynolds Programme for Category
Theory and Programming Languages
(with
Claudio Hermida and
Edmund Robinson.
Dedicated to the memory of John C. Reynolds, 19352013,
WACT 2013.)
In his seminal paper on “Types, Abstraction and Parametric Polymorphism,”
John Reynolds called for homomorphisms to be generalized from functions to
relations. He reasoned that such a generalization would allow typebased
“abstraction” (representation independence, information hiding, naturality
or parametricity) to be captured in a mathematical theory, while accounting
for higherorder types. However, after 30 years of research, we do not yet
know fully how to do such a generalization. In this article, we explain the
problems in doing so, summarize the work carried out so far, and call for a
renewed attempt at addressing the problem.
[ENTCS

preprint PDF]
AutomataTheoretic Semantics of Idealized Algol with Passive Expressions
(MFPS 2013)
Passive expressions in Algollike languages represent computations that read
the state but do not modify it. The need for such readonly computations
arises in programming logics as well as in concurrent programming. It is
also a central facet in Reynolds's Syntactic Control of Interference.
Despite its importance and essentially basic character, capturing the notion
of passivity in semantic models has proved to be difficult. In this paper,
we provide a new model of passive expressions using an automatatheoretic
framework recently proposed by the author. The central idea is that the
store of a program is viewed as an abstract form of an automaton, with a
representation of its states as well as state transitions. The framework
allows us to combine the strengths of conventional statebased models and
the more recent eventbased models to synthesize new "automatabased"
models. Once this basic framework is set up, relational parametricity does
the job of identifying passive computations.
[PDF 
Slides from MFPS Reynolds
memorial session 
Slides with
transitions
]
An AutomataTheoretic Model of Idealized Algol (with Brian Dunphy,
ICALP 2012, July 2012)
In this paper, we present a new model of classbased Algollike programming
languages inspired by automatatheoretic concepts. The model may be seen as
a variant of the "objectbased" model previously proposed by Reddy, where
objects are described by their observable behaviour in terms of events. At
the same time, it also reflects the intuitions behind statebased models
studied by Reynolds, Oles, Tennent and O'Hearn where the effect of commands
is described by state transformations. The idea is to view stores as
automata, capturing not only their states but also the allowed state
transformations. In this fashion, we are able to combine both the
statebased and eventbased views of objects. We illustrate the efficacy of
the model by proving several test equivalences and discuss its connections
to the previous models.
[Extended abstract 
Full paper
]
Syntactic Control of Interference for Separation Logic (with John
C. Reynolds, POPL 2012, Jan 2012)
Separation Logic has witnessed tremendous success in recent years in
reasoning about programs that deal with heap storage. Its success owes to
the fundamental principle that one should keep separate areas of the heap
storage separate in program reasoning. However, the way Separation Logic
deals with program variables continues to be based on traditional Hoare
Logic without taking any benefit of the separation principle. This has led
to unwieldy proof rules suffering from lack of clarity as well as questions
surrounding their soundness. In this paper, we extend the separation idea
to the treatment of variables in Separation Logic, especially Concurrent
Separation Logic, using the system of Syntactic Control of Interference
proposed by Reynolds in 1978. We extend Reynolds's original system with
permission algebras, making it more powerful and able to deal with the
issues of concurrent programs. The result is a streamined presentation of
Concurrent Separation Logic, whose rules are memorable and soundness
obvious. We also include a discussion of how the new rules impact the
semantics and devise static analysis techniques to infer the required
permissions automatically.
[pdf file 
Slides from POPL 
Reddy's slides 
Reynolds' slides]
An AutomataTheoretic Model of Objects (with Brian P. Dunphy,
Foundations of Objectoriented Languages, October 2011)
In this paper, we present a new model of classbased Algollike programming
languages inspired by automatatheoretic concepts. The model may be seen as
a variant of the "objectbased" model previously proposed by the author,
where objects are described by their observable behaviour in terms of
events. At the same time, it also reflects the intuitions behind
statebased models studied by Reynolds, Oles, Tennent and O'Hearn where the
effect of commands is described by state transformations. The idea is to
view stores as automata, capturing not only their states but also the
allowed state transformations. In this fashion, we are able to combine both the
statebased and eventbased views of objects. We illustrate the efficacy of
the model by proving several test equivalences and discuss its connections
to the previous models.
[pdf
file 
talk at Domains X 
talk at FOOL 2011]
Syntactic Control of Interference for Separation Logic
(Preliminary Report, April 2011)
Reynolds formulated a system of rules called Syntactic Control of
Interference in 1978 to capture the conventions of good programming
practice in controlling variable aliasing and to facilitate reasoning
about programs. We apply these principles to the formulation of
Concurrent Separation Logic, which has been fraught with numerous side
conditions in its proof rules, making it noncompositional and hard to
use in practice. Our system of Syntactic Control of Interference is
Reynolds's system extended with a permissions algebra, making it
powerful enough to deal with the issues of Concurrent Separation
Logic. Alternative solutions from Brookes and Parkinson et al. are
compared and our solution is placed in context. We also examine how
the reformulated proof rules impact the denotational semantics of the
programming language.
[pdf file 
slides]
John Reynolds has formulated a static analysis algorithm for this
system of rules, presented in his
MFPS 2011 talk. A
joint paper combining both the rules and the algorithm is under
preparation.
Semantics of Parametric Polymorphism in Imperative Programming
Languages (with Brian P. Dunphy, October 2010)
Programming languages such as CLU, Ada and Modula3 have included
facilities for parametric polymorphism and, more recently, C++ and
Java have also added similar facilities. In this paper, we examine
the issues of defining denotational semantics for imperative
programming languages with polymorphism. We use the framework of
reflexive graphs of categories previously developed for a general
axiomatization of relational parametricity constraints implicit in
polymorphic functions. We specialize it to the context of imperative
programming languages, which in turn involve parametricity constraints
implicit in local variables. The two levels of parametricity inherent
in such languages can be captured in a pleasing way in "higherorder"
reflexive graphs.
[pdf file]
Finegrained concurrency with Separation Logic (Kalpesh Kapoor,
Kamal Lodaya and Uday
Reddy, Journal of Philosophical Logic, Oct. 2011)
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 finegrained concurrency. We note that O'Hearn's
formulation of Concurrent Separation Logic is by and large applicable
to finegrained 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.
[pdf file]
Parametric limits (Brian P. Dunphy and Uday S. Reddy,
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]
 pdf file]
Correctness of data representations involving heap data structures
(with H. Yang, Science of Computer Programming, 2004)
While the semantics of local variables in programming languages is by
now wellunderstood, the semantics of pointeraddressed 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 Pascallike 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.
[pdf file 
earlier version in ESOP 2003]
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.
Brian Dunphy's PhD Thesis, 2002
Parametricity as a notion of uniformity in reflexive graphs,
Department of Mathematics, University of Illinois, 2002.
[ PS file 
PDF file]
Hongseok Yang's PhD Thesis, 2001
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
Algollike 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 Algollike language using such sheaves and discuss the
reasoning principles validated by the semantics.
[ps file 
pdf file]
Objects and classes in Algollike languages
(Information and Computation, 2002)
Many objectoriented languages used in practice descend from Algol.
With this motivation, we study the theoretical issues underlying such
languages via the theory of Algollike 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 Hoarelike
reasoning methods, and relational parametricity provide powerful
formal tools for reasoning about Algollike objectoriented programs.
[ps
file  pdf file]
]
This paper is an expanded version of a FOOL 98 paper:
[pdf file 
dvi file and a
ps figure]
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 interferencefree programming, with cleaner reasoning
properties and semantics than traditional imperative languages. This
paper makes SCIbased 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 letbound 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 SCIbased
interference control.
[
pdf 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 HindleyMilner
style polymorphism and devise type reconstruction algorithms. A
sophisticated constraint language is designed to formulate principal
types for terms.
[dvi file 
pdf file]
Parametricity and Naturality in the Semantics of Algollike Languages
(Unpublished manuscript, December 1998)
We examine the relationship between two notions of uniformity for
polymorphic functions, viz., relational parametricity and naturality.
While naturality applies only to firstorder function types,
parametricity is more general. We axiomatize parametricity at a
categorical level so that it subsumes naturality, and provide examples
of this situation. Both parametricity and naturality are key
components in giving denotational semantics to Algollike languages.
The known models for these languages do not have strong enough
parametricity properties to subsume naturality. We give new models
where such subsumption takes place. The parametricity properties of
the new models automatically incorporate solutions for some of the
thorny issues in semantics such as passivity and irreversible state
change.
[pdf file]
The results in this unpublished paper were generalized in subsequent
joint work with Brian Dunphy, documented in his PhD thesis. The categorical
ideas of the work were published in "Parametric Limits," LICS 2004. The ideas
regarding the semantics of Algollike languages are in the Chapter 6 of
Dunphy's thesis.
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 
pdf file]
Summary of Research
 Concurrent Separation Logic:
A challenging exercise in proving the correctness of a concurrent program,
"Onthefly garbage collector" of Dijkstra et al., is in
[KLR11]. A clean formulation of Concurrent Separation Logic
bringing structure to its traditional variable conditions is found in this
[RR12].
 Relational Parametricity:
John Reynolds proposed relational parametricity as a uniformity condition
implicit in polymorphic functions. A categorical axiomatization of this
notion is in [DR04] and
[Dunphy's PhD thesis]. The
application of these ideas to the semantics of polymorphic Algollike
languages is in a [manuscript].
 Semantics:
The language Idealized Algol+ is proposed as a foundation for
Algollike objectoriented languages[Red98].
Objects with state form the foundation for a new semantics for
higherorder imperative programs without a global state
[Red96].
It has been proved fully abstract up to second order
[OR95]. A newer model that combines the traditional
statebased semantics and objectbased semantics is in
[RD11].
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 objectbased semantics.
 Objectoriented programming:
An attempt at a sane definition of core C++ is
here.
Illinois Concert C++
is a simple and powerful extension of C++ for
highperformance parallel computing
[CRPD96].
 Logic Programming:
Typed Prolog is an implementation of HindleyMilner 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 termrewriting and automated deduction techniques for program
transformation, is in
[Red91a].
The theoretical underpinnings of these techniques is found in
[DR93].
 Automated Deduction:
"Termrewriting 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.
Ph. D. Students

Brian Dunphy,
University of Illinois, 2002.
PhD Thesis:
Parametricity as a notion of uniformity in reflexive graphs.

Hongseok Yang,
University of Illinois, 2001.
PhD Thesis:
Local reasoning for stateful programs, Tech Report
UIUCDCSR20012227.

T. K. Lakshman,
University of Illinois, 1996.

Francois Bronsard,
University of Illinois, 1995.
PhD Thesis:
Using term ordering to control clausal deduction, Tech
Report UIUCDCSR951910.

Robert W. Hasker,
University of Illinois, 1994.
PhD Thesis:
Replay of Program Derivations, Tech Report
UIUCDCSR941890.

Vipin Swarup,
University of Illinois, 1992.
PhD Thesis:
Type Theoretic Properties of Assignments, Tech Report UIUCDCSR921777.

Changwoo Pyo,
University of Illinois, 1990.
PhD Thesis: Type inference for Logic Programs.
Bibliography
 [BOR14]

The Essence of Reynolds,
S. Brookes,
P.W. O'Hearn and
U.S. Reddy,
ACM Symp. on Principles of
Programming Languages 2014.
 [HRR14]

Logical relations and parametricity: A Reynolds programme for category
theory and programming languages,
C. Hermida, U.S. Reddy and E.P. Robinson,
Workshop
on Algebra, Coalgebra and Topology 2013, ENTCS, to appear, 2014.
 [R13]

Automatatheoretic semantics of Idealized Algol with Passive
Expressions,
U.S. Reddy,
Proc.
TwentyNinth Conf. on Math. Foundations of Prog. Semantics, MFPS
XXIX, ENTCS Vol. 298, pp. 325348, 2013.
 [RR12]

Syntactic Control of Interference for Separation Logic,
U. S. Reddy and J. C. Reynolds,
ACM Symp. on Principles
of Programming Languages, 2012.
 [RD11]

An AutomataTheoretic Model of Objects,
U. S. Reddy and B. P. Dunphy,
Foundations of ObjectOriented Languages, October, 2011.
 [KLR11]

Finegrained Concurrency with Separation Logic,
K. Kapoor, K. Lodaya and U. S. Reddy,
Journal
of Philosophical Logic, 40(5)583632, 2011.
.
 [DR04]

Parametric Limits,
B. P. Dunphy and U. S. Reddy,
IEEE Conf. Logic in Computer Science, 2004.
 [RY04]

Correctness of Data Representations involving Heap Data
Structures,
U. S. Reddy and H.Yang,
Science of Computer Programming, 50(13): 2004.
[PS 
PDF]
 [RY03]

Correctness of Data Representations involving Heap Data
Structures,
U. S. Reddy and H. Yang,
in P. Degano (ed) Programming Languages and Systems, 12th
European Symposium on Programming,
Springer LNCS, Vol. 2618, pp 223237, 2003.
 [BORT02]

Linear Continuation Passing,
J. Berdine, P. W. O'Hearn, U. S. Reddy, H. Thielecke,
Higher Order and Symbolic Computation, 15(2/3):181208,
September 2002.
 [Red02]

Objects and classes in Algollike Languages,
Information and Computation, 172:6397, 2002.
 [RY00]

On the Semantics of Refinement Calculi,
U. S. Reddy and H. Yang,
Foundations of Software Science and Computer Structures 2000.
 [Red99]

Programming Theory,
U. S. Reddy,
Wiley Encyclopedia of Electrical and Electronics
Engineering,
Vol. 17, John Wiley, 1999, pp. 358374.
 [Red98]

Objects and classes in Algollike languages,
U.S.Reddy,
FOOL 5,
San Diego, Jan. 1998.
 [SRI97]
 Assignments for Applicative Languages,
V.Swarup, U.S.Reddy, E.Ireland,
Chapter 9 of
Algollike Languages, Volume 1,
O'Hearn, P.W. and
Tennent, R.D. (eds) Birhauser, Boston, 1997.
 [Red96a]

Imperative Functional Programming,
U.S.Reddy,
Computing Surveys, 28:2(312314), ACM, June 1996.
 [BR96]

Clausal completion,
F.Bronsard and U.S.Reddy,
Manuscript, Jan. 1996.
[PS 
PDF]
 [CRPD96]

ICC++: A C++ dialect for high performance parallel computing,
in
ISOTAS 96.
 [Red96]

Global state considered unnecessary: An introduction to
objectbased semantics,
J. Lisp and Symbolic Computation, 9(1996):776.
[PS 
PDF]
 [HR96]

Type reconstruction for SCI,
Glasgow Functional Programming Workshop, 1995.
 [OR95]

Objects, interference and the Yoneda embedding,
(joint with
Peter
O'Hearn),
MFPS XI,
Vol 1. of
ENTCS, 1995.
 [BRH94]

Induction using term orderings,
F.Bronsard, U.S.Reddy and R.W.Hasker,
in A.Bundy (ed), CADE 94, LNAI Vol. 814, SpringerVerlag,
1994, pp. 102117.
 [KR94]

Two semantic models of objectoriented languages,
S.N.Kamin and U.S.Reddy,
in C.A.Gunter and J.C.Mitchell (eds)
Theoretical Aspects of ObjectOriented Programming,
MIT Press, 1994, pp. 463496.
 [Red94]

Higherorder aspects of logic programming,
in R.Dyckhoff (ed), Extensions of Logic Programming,
LNAI Vol. 798, SpringerVerlag, 1994.
(Also) Extended Abstract in P.Van Hentenryck (ed),
Logic Programming: Eleventh International Conf., MIT Press,
1994. pp. 402418.
 [Red94a]

Passivity and Independence,
LICS 94, pp. 342352.
 [Red94b]

The design of core C++,
Manuscript, May 1994.
 [DR93]

Deductive and inductive synthesis of equational programs,
N.Dershowitz and U.S.Reddy,
J. Symbolic Computation, 15(1993):467494.
[PS 
PDF]
 [Red93]

A typed foundation for directional logic programming,
in E.Lamma and P.Mello (eds) Extensions of Logic Programming,
LNAI Vol. 660, SpringerVerlag, 1993, pp. 282318.
 [Red93a]

A linear logic model of state,
Manuscript, Oct. 1993.
 [KR93]

On the power of abstract interpretation,
S.N.Kamin and U.S.Reddy,
Computer Languages, 19(1993):2:7989.
[PS 
PDF]
 [BLR92]

A framework of directionality for proving terminatin of
logic programs,
F.Bronsard, T.K.Lakshman and U.S.Reddy,
in K.Apt (ed), Logic Programming: 1992 Joint International
Conference and Symposium, MIT Press, 1992, pp. 321335.
 [BR92]

Reduction techniques for firstorder reasoning,
F.Bronsard and U.S.Reddy,
in M.Rusinowitch and J.L.Remy (eds), Conditional Term
rewriting systems, LNCS Vol. 656, SpringerVerlag, 1992, pp.
242256.
 [SR92]

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,
SpringerVerlag, 1992.
 [LR91]

Typed Prolog: A Semantic Reconstruction of the MycroftO'Keefe
Type System,
T.K.Lakshman and U.S. Reddy,
in V.Saraswat and K.Ueda (eds) Logic Programming: 1991
International Symposium, MIT Press, 1991, pp. 202217.
[PS 
PDF]
 [Red91]

Acceptors as values: Functional Programming in classical
linear logic,
Manuscript, Dec. 1991.
 [Red91a]

Design principles for an interactive program derivation
system, in M.Lowry and R.D.McCartney (eds),
Automating Software Design, AAAI Press, 1991, Chapter 18.
 [SRI91]

Assignments for applicative languages,
V.Swarup, U.S.Reddy and E.Ireland,
in R.J.M.Hughes (ed), FPCA 91,
LNCS Vol. 523, SpringerVerlag, 1991, pp. 192214.
 [Red90]

Term Rewriting Induction,
in M.Stickel (ed) CADE 90, LNAI Vol. 449, 1990, pp. 162177.
[PS 
PDF]
 [Red88]
 Objects as closures: Abstract semantics of objectoriented
languages,
U.S.Reddy,
Lisp & Functional Porg, 1988, pp. 289297
Uday S. Reddy /
School of Computer Science /
Univ of Birmingham /
U.S.Reddy AT cs.bham.ac.uk