Zobrazeno 1 - 10
of 79
pro vyhledávání: '"John C. Reynolds"'
Publikováno v:
POPL
O'Hearn, P W, Yang, H, Reynolds, J C, Jones, N D (ed.) & Leroy, X (ed.) 2004, Separation and Information Hiding . in Ikke angivet . Association for Computing Machinery, pp. 268-280, Venedig, Italy, 14/01/2004 .
O'Hearn, P W, Yang, H, Reynolds, J C, Jones, N D (ed.) & Leroy, X (ed.) 2004, Separation and Information Hiding . in Ikke angivet . Association for Computing Machinery, pp. 268-280, Venedig, Italy, 14/01/2004 .
We investigate proof rules for information hiding, using the recent formalism of separation logic. In essence, we use the separating conjunction to partition the internal resources of a module from those accessed by the module's clients. The use of a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1c61661540a0eba68171265d69fead4c
https://ora.ox.ac.uk/objects/uuid:95e237fe-d9a2-44aa-a70f-3d182f098a29
https://ora.ox.ac.uk/objects/uuid:95e237fe-d9a2-44aa-a70f-3d182f098a29
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
Autor:
Peter W. O'Hearn, John C. Reynolds
Publikováno v:
Journal of the ACM. 47:167-223
In a linearly-typed functional language, one can define functions that consume their arguments in the process of computing their results. This is reminiscent of state transformations in imperative languages, where execition of an assignment statement
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b1ca3263796ff360db9450b0482d5d37
https://doi.org/10.1145/331605.331611
https://doi.org/10.1145/331605.331611
Autor:
John C. Reynolds
Publikováno v:
ACM SIGPLAN Notices. 43:108-110
It is argued that the teaching of programming is central to the education of skilled computer professionals, that the teaching of programming languages is central to the teaching of programming. that these topics must include the specification, struc
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a0170fa417a5db3899f741988c3a21f1
https://doi.org/10.1145/1480828.1480852
https://doi.org/10.1145/1480828.1480852
Autor:
John C. Reynolds
Publikováno v:
Theories of Programming Languages. :447-466
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a2d0f47ede959868c2f46c393d9eb756
https://doi.org/10.1017/cbo9780511626364.021
https://doi.org/10.1017/cbo9780511626364.021
Autor:
John C. Reynolds
Publikováno v:
Higher Order Symbolic Computation. 11:363-397
Higher-order programming languages (i.e., languages in which procedures or labels can occur as values) are usually defined by interpreters that are themselves written in a programming language based on the lambda calculus (i.e., an applicative langua
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2239ee58370bbbf629a8954f4aad5426
https://doi.org/10.1023/a:1010027404223
https://doi.org/10.1023/a:1010027404223
Autor:
John C. Reynolds
Publikováno v:
Higher Order Symbolic Computation. 11:355-361
To introduce the republication of “Definitional Interpreters for Higher-Order Programming Languages”, the author recounts the circumstances of its creation, clarifies several obscurities, corrects a few mistakes, and briefly summarizes some more
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::45e1952496d92f4c7b50d5c115693fcc
https://doi.org/10.1023/a:1010075320153
https://doi.org/10.1023/a:1010075320153
Autor:
John C. Reynolds
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540068594
Symposium on Programming
Symposium on Programming
7)(D) = B[w][71t]#D] and delta is a functor from Funct(C, C) into C. Even before defining the functors arrow and delta, it can be shown that B maps every type expression into a functor from C T into C, that w = w' implies B[w] = B[w'], and that B[WlI
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::116dfc599fe46fd4f5a6436b50aaff17
Autor:
John C. Reynolds
Publikováno v:
TASE
To verify program specifications, rather than generic safety properties, it will be necessary to integrate verification into the process of programming. Program proving is unlike theorem proving in mathematics - mathematical conjectures may give no h
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::effcefdbbd572d26b460c0cfd32fb244
https://doi.org/10.1109/tase.2011.48
https://doi.org/10.1109/tase.2011.48
Autor:
John C. Reynolds
Publikováno v:
LISP and Symbolic Computation. 6:233-247
We give a brief account of the discoveries of continuations and related concepts by A. van Wijngaarden, A. W. Mazurkiewicz, F. L. Morris, C. P. Wadsworth, J. H. Morris, M. J. Fischer, and S. K. Abdali.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d12be903b80ac07e53d84d6c2339a640
https://doi.org/10.1007/bf01019459
https://doi.org/10.1007/bf01019459