Prof. Uday S. Reddy

School of Computer Science, University of Birmingham.

Appointments See my 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: Looking into the applications of relational parametricity in mathematics and type theories in general, and programming language semantics in particular.

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

Discussions

Teaching

Recent papers/talks/manuscripts

Parametric polymorphism and Models of storage (November 2016)

A talk in memory of Christopher Strachey at the Strachey 100 Centenary Conference[slides]

The Essence of Reynolds

(with Stephen Brookes and Peter O'Hearn, POPL 2014.)

John Reynolds (1935-2013) 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, 1935-2013, 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 type-based “abstraction” (representation independence, information hiding, naturality or parametricity) to be captured in a mathematical theory, while accounting for higher-order 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]

Automata-Theoretic Semantics of Idealized Algol with Passive Expressions (MFPS 2013)

Passive expressions in Algol-like languages represent computations that read the state but do not modify it. The need for such read-only 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 automata-theoretic 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 state-based models and the more recent event-based models to synthesize new "automata-based" 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 Automata-Theoretic Model of Idealized Algol (with Brian Dunphy, ICALP 2012, July 2012)

In this paper, we present a new model of class-based Algol-like programming languages inspired by automata-theoretic concepts. The model may be seen as a variant of the "object-based" 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 state-based 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 state-based and event-based 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 Automata-Theoretic Model of Objects (with Brian P. Dunphy, Foundations of Object-oriented Languages, October 2011)

In this paper, we present a new model of class-based Algol-like programming languages inspired by automata-theoretic concepts. The model may be seen as a variant of the "object-based" 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 state-based 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 state-based and event-based 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 non-compositional 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 Modula-3 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 "higher-order" reflexive graphs. [pdf file]

Fine-grained 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 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] | 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 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. [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 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: [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 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. [ 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 Hindley-Milner 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 Algol-like 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 first-order 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 Algol-like 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 Algol-like 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

Ph. D. Students

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]
Automata-theoretic semantics of Idealized Algol with Passive Expressions, U.S. Reddy, Proc. Twenty-Ninth Conf. on Math. Foundations of Prog. Semantics, MFPS XXIX, ENTCS Vol. 298, pp. 325-348, 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 Automata-Theoretic Model of Objects, U. S. Reddy and B. P. Dunphy, Foundations of Object-Oriented Languages, October, 2011.
[KLR11]
Fine-grained Concurrency with Separation Logic, K. Kapoor, K. Lodaya and U. S. Reddy, Journal of Philosophical Logic, 40(5)583-632, 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(1-3): 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 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.
[Red96a]
Imperative Functional Programming, U.S.Reddy, Computing Surveys, 28:2(312-314), 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 object-based semantics, J. Lisp and Symbolic Computation, 9(1996):7-76. [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, 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. [PS | PDF]

[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. [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. 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. [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, Springer-Verlag, 1991, pp. 192-214.

[Red90]
Term Rewriting Induction, in M.Stickel (ed) CADE 90, LNAI Vol. 449, 1990, pp. 162-177. [PS | PDF]

[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