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 cs.bham.ac.uk, +44 121 414 2740.

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!

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, 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.

Research

Recent activities
Summary of research
Ph.D. Students
Bibliography
Paper Archive

Teaching

Computing Resources

Recent papers/manuscripts

Fine-grained concurrency with Separation Logic (Kalpesh Kapoor, Kamal Lodaya and Uday Reddy)

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. [ 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]

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] ]

This paper is an expanded version of a FOOL 98 paper: [ps 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 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]

Summary of Research

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.

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 UIUCDCS-R-2001-2227.
T. K. Lakshman, University of Illinois, 1996.
Francois Bronsard, University of Illinois, 1995.
PhD Thesis: Using term ordering to control clausal deduction, Tech Report UIUCDCS-R-95-1910.
Robert W. Hasker, University of Illinois, 1994.
PhD Thesis: Replay of Program Derivations, Tech Report UIUCDCS-R-94-1890.
Vipin Swarup, University of Illinois, 1992.
PhD Thesis: Type Theoretic Properties of Assignments, Tech Report UIUCDCS-R-92-1777.
Changwoo Pyo, University of Illinois, 1990.
PhD Thesis: Type inference for Logic Programs.

Bibliography

[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 223-237, 2003.
[BORT02]: 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.
[Red02]: Objects and classes in Algol-like Languages, Information and Computation, 172:63-97, 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. 358-374.
[Red98]: Objects and classes in Algol-like 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 Algol-like Languages, Volume 1, O'Hearn, P.W. and Tennent, R.D. (eds) Birhauser, Boston, 1997.
[BR96]: Clausal completion, F.Bronsard and U.S.Reddy, Manuscript, Jan. 1996.
[CRPD96]: ICC++: A C++ dialect for high performance parallel computing, in ISOTAS 96.
[Red96]: Global state considered unnecessary: An introduction to object-based semantics, J. Lisp and Symbolic Computation, 9(1996):7-76.
[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, Springer-Verlag, 1994, pp. 102-117.
[KR94]: Two semantic models of object-oriented languages, S.N.Kamin and U.S.Reddy, in C.A.Gunter and J.C.Mitchell (eds) Theoretical Aspects of Object-Oriented Programming, MIT Press, 1994, pp. 463-496.
[Red94]: 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.
[Red94a]: Passivity and Independence, LICS 94, pp. 342-352.
[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):467-494.
[Red93]: A typed foundation for directional logic programming, in E.Lamma and P.Mello (eds) Extensions of Logic Programming, LNAI Vol. 660, Springer-Verlag, 1993, pp. 282-318.
[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:79-89.
[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. 321-335.
[BR92]: 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.
[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, Springer-Verlag, 1992.
[LR91]: Typed Prolog: A Semantic Reconstruction of the Mycroft-O'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. 202-217.
[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, Springer-Verlag, 1991, pp. 192-214.
[Red90]: Term Rewriting Induction, in M.Stickel (ed) CADE 90, LNAI Vol. 449, 1990, pp. 162-177.
[Red88]: Objects as closures: Abstract semantics of object-oriented languages, U.S.Reddy, Lisp & Functional Porg, 1988, pp. 289-297

Uday S. Reddy / School of Computer Science / Univ of Birmingham / U.S.Reddy AT cs.bham.ac.uk