Zobrazeno 1 - 10
of 45
pro vyhledávání: '"Uday S. Reddy"'
Publikováno v:
MFPS
This paper extends the results of Hermida's thesis about logical predicates to more general logical relations and a wider collection of types. The extension of type constructors from types to logical relations is derived from an interpretation of tho
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5fc1bcc398c6ffc18dbe794a64a31f62
https://doi.org/10.1016/j.entcs.2019.09.013
https://doi.org/10.1016/j.entcs.2019.09.013
Publikováno v:
Electronic Notes in Theoretical Computer Science. 303:149-180
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” (repre
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e43b7039469100daac1d661ca8ea5b77
https://doi.org/10.1016/j.entcs.2014.02.008
https://doi.org/10.1016/j.entcs.2014.02.008
Autor:
Uday S. Reddy
Publikováno v:
MFPS
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 Rey
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::716e3882dfa81a7f82da1764b6dbd8c1
Autor:
John C. Reynolds, Uday S. Reddy
Publikováno v:
POPL
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 reaso
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5d393a644642b21c973f7ae59c46a55f
https://doi.org/10.1145/2103621.2103695
https://doi.org/10.1145/2103621.2103695
Publikováno v:
Journal of Philosophical Logic. 40:583-632
Reasoning about concurrent programs involves representing the information that concurrent processes manipulate disjoint portions of memory. In sophisticated applications, the division of memory between processes is not static. Through operations, pro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d850a261da6e2adbe3c28ef43c9c8005
https://doi.org/10.1007/s10992-011-9195-1
https://doi.org/10.1007/s10992-011-9195-1
Publikováno v:
Higher-Order and Symbolic Computation. 15:181-208
Continuations can be used to explain a wide variety of control behaviours, including calling/returning (procedures), raising/handling (exceptions), labelled jumping (\tt goto statements), process switching (coroutines), and backtracking. However, con
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c493e6c6be9ba07a8a8021232a342745
https://doi.org/10.1023/a:1020891112409
https://doi.org/10.1023/a:1020891112409
Autor:
Uday S. Reddy
Publikováno v:
Information and Computation. 172:63-97
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 cl
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::af5e1021645dac63da398e5c8a16c8a1
https://doi.org/10.1006/inco.2001.2927
https://doi.org/10.1006/inco.2001.2927
Publikováno v:
POPL
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.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6bda700f4dbaa7846ac28c130eb99c33
https://doi.org/10.1145/2535838.2537851
https://doi.org/10.1145/2535838.2537851
Autor:
Uday S. Reddy, Peter W. O'Hearn
Publikováno v:
MFPS
We present a new semantics for Algol-like languages that combines methods from two prior lines of development: • the object-based approach of [21,22], where the meaning of an imperative program is described in terms of sequences of observable actio
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1db788a806813c4ac9e630bb3ba588e9
https://doi.org/10.1016/s0304-3975(98)00360-0
https://doi.org/10.1016/s0304-3975(98)00360-0
Publikováno v:
Journal of Automated Reasoning. 16:3-37
We present a procedure for proving inductive theorems which is based on explicit induction, yet supports mutual induction. Mutual induction allows the postulation of lemmas whose proofs use the theorems ex hypothesi while the theorems themselves use
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a99ee9a4695aa8eb0f712d0ff1074a70
https://doi.org/10.1007/bf00244458
https://doi.org/10.1007/bf00244458