Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
% jwrhtml.bib -- % Created: 1998/12/05 12:40 by James Riely % Revised: 2006/08/25 13:19 % @InProceedings{04concur, author = {Glen Bruns and Radha Jagadeesan and Alan Jeffrey and James Riely}, title = {muABC: A Minimal Aspect Calculus}, editor = {Philippa Gardner and Nobuko Yoshida}, booktitle = {CONCUR 2004: Concurrency Theory}, rate = {22\%}, month = aug, address = {London}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 3170, year = 2004, pages = "209--224", file = {04concur}, pdf = {}, urlbooktitle = {http://www.doc.ic.ac.uk/concur2004/}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, abstract = {Aspect-oriented programming is emerging as a powerful tool for system design and development. In this paper, we study aspects as primitive computational entities on par with objects, functions and horn-clauses. To this end, we introduce muABC, a name-based calculus, that incorporates aspects as primitive. In contrast to earlier work on aspects in the context of object-oriented and functional programming, the only computational entities in muABC are aspects. We establish a compositional translations into muABC from a functional language with aspects and higher-order functions. Further, we delineate the features required to support an aspect-oriented style by presenting a translation of muABC into an extended pi-calculus.} } @InProceedings{06fossacs, author = {Corin Pitcher and James Riely}, title = {Dynamic Policy Discovery with Remote Attestation}, editor = {Luca Aceto and Anna Ing{\'o}lfsd{\'o}ttir}, OPTbooktitle = {Foundations of Software Science and Computation Structures, 9th International Conference, FOSSACS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25-31, 2006, Proceedings}, pages = {111-125}, booktitle = {FOSSACS 2006}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {3921}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, urlbooktitle = {http://fossacs06.ru.is/}, url = {http://dx.doi.org/10.1007/11690634_8}, year = 2006, isbn = {3-540-33045-3}, file = {06fossacs}, pdf = {}, abstract = {Remote attestation allows programs running on trusted hardware to prove their identity (and that of their environment) to programs on other hosts. Remote attestation can be used to address security concerns if programs agree on the meaning of data in attestations. This paper studies the enforcement of code-identity based access control policies in a hostile distributed environment, using a combination of remote attestation, dynamic types, and typechecking. This ensures that programs agree on the meaning of data and cannot violate the access control policy, even in the presence of opponent processes. The formal setting is a pi-calculus with secure channels, process identity, and remote attestation. Our approach allows executables to be typechecked and deployed independently, without the need for secure initial key and policy distribution beyond trusted hardware.} } @InProceedings{06lambda-rbac, author = "Radha Jagadeesan and Alan Jeffrey and Corin Pitcher and James Riely", title = "Lambda-RBAC: Programmatic Role-Based Access Control", booktitle = "ICALP 2006", urlbooktitle = {http://icalp06.dsi.unive.it/}, file = {06lambda-rbac}, pdf = {}, OPTcrossref = "", OPTkey = "", pages = "456--467", year = 2006, publisher = {Springer}, series = {Lecture Notes in Computer Science}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTmonth = "", OPTorganization = "", OPTpublisher = "", OPTnote = "", OPTannote = "", abstract = { We study mechanisms that permit program components to express role constraints on clients, focusing on programmatic security mechanisms, which permit access controls to be expressed, in situ, as part of the code realizing basic functionality. In this setting, two questions immediately arise: (1) The user of a component faces the issue of safety: is a particular role sufficient to use the component? (2) The component designer faces the dual issue of protection: is a particular role demanded in all execution paths of the component? We provide a formal calculus and static analysis to answer both questions. } } @Article{06scp, urljournal = {http://www.elsevier.com/locate/scico}, journal = {Science of Computer Programming}, year = {2006, To Appear}, author = {Radha Jagadeesan and Alan Jeffrey and James Riely}, title = {Typed Parametric Polymorphism for Aspects}, file = {06scp}, pdf = {}, abstract = {We study the incorporation of generic types in aspect languages. Since advice acts like method update, such a study has to accommodate the subtleties of the interaction of classes, polymorphism and aspects. Indeed, simple examples demonstrate that current aspect compiling techniques do not avoid runtime type errors. We explore type systems with polymorphism for two models of parametric polymorphism: the type erasure semantics of Generic Java, and the type carrying semantics of designs such as generic C\#. Our main contribution is the design and exploration of a source-level type system for a parametric OO language with aspects. We prove progress and preservation properties. We believe our work is the first source-level typing scheme for an aspect-based extension of a parametric object-oriented language.}, } @Misc{04typed, author = {Radha Jagadeesan and Alan Jeffrey and James Riely}, title = {A Typed Calculus of Aspect-Oriented Programs}, note = {Manuscript}, htmlnote = {Manuscript}, year = 2003, file = {04typed}, pdf = {}, abstract = {Aspects have emerged as a powerful tool in the design and development of systems, allowing for the encapsulation of program transformations. In earlier work, we described an untyped calculus of aspect programs with a direct description of the dynamic semantics. This calculus provides a specification for the correctness of weaving. In this paper, we turn our attention to the interaction of aspects and types, whose subtleties are amply illustrated by the difficulties encountered by current compilers of aspect languages. We develop a typed calculus of aspect programs that includes inner classes, concurrency and dynamic arrival of new advice. To our knowledge, this is the first source-level typing system for a class-based aspect-oriented language. We prove that types are preserved by reduction in the aspect calculus and that well-typed programs make progress. We also show that weaving preserves typability of programs by mapping well-typed aspect programs to well-typed class based programs.} } @InProceedings{03ecoop, author = {Radha Jagadeesan and Alan Jeffrey and James Riely}, title = {A Calculus of Untyped Aspect-Oriented Programs}, booktitle = {Proceedings of the European Conference on Object-Oriented Programming}, editor = {L. Cardelli}, volume = 1853, rate = {20\%}, pages = {415--427}, year = 2003, month = jul, address = {Geneva}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, file = {03ecoop}, pdf = {}, urlbooktitle = {http://www.ecoop.tu-darmstadt.de/}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, abstract = {Aspects have emerged as a powerful tool in the design and development of systems, allowing for the encapsulation of program transformations. The dynamic semantics of aspects is typically specified by appealing to an underlying object-oriented language via a compiler transformation known as weaving. This treatment is unsatisfactory for several reasons. Firstly, this semantics violates basic modularity principles of object-oriented programming. Secondly, the converse translation from object-oriented programs into an aspect language has a simple canonical flavor. Taken together, these observations suggest that aspects are worthy of study as primitive computational abstractions in their own right. In this paper, we describe an aspect calculus and its operational semantics. The calculus is rich enough to encompass many of the features of extant aspect-oriented frameworks that do not involve reflection. The independent description of the dynamic semantics of aspects enables us to specify the correctness of a weaving algorithm. We formalize weaving as a translation from the aspect calculus to a class-based object calculus, and prove its soundness.} } @InProceedings{06foal, author = "Peter Hui and James Riely", title = "Temporal Aspects as Security Automata", booktitle = "Foundations of Aspect-Oriented Languages (FOAL)", urlbooktitle = {http://www.cs.iastate.edu/~leavens/FOAL/}, file = "06foal", pages = {19--28}, pdf = {}, year = 2006, abstract = {Aspect-oriented programming (AOP) has been touted as a promising paradigm for managing complex software-security concerns. Roughly, AOP allows the security-sensitive events in a system to be specified separately from core functionality. The events of interest are specified in a pointcut. When a pointcut triggers, control is redirected to advice, which intercepts the event, potentially redirecting it to an error handler. Many interesting security properties are history-dependent; however, currently deployed pointcut languages cannot express history-sensitivity (mechanisms like cflow in AspectJ capture only the current call stack.) We present a language of pointcuts with past-time temporal operators and discuss their implementation using a variant of security automata. The main result is a proof that the implementation is correct. Refining our earlier work, we define a minimal language of events and aspects in which ``everything is an aspect''. The minimalist approach serves to clarify the issues and may be of independent interest.} } @Article{00TR-pisec, author = {Matthew Hennessy and James Riely}, title = {Information Flow vs. Resource Access in the Asynchronous Pi-Calculus}, journal = {ACM Transactions on Programming Languages and Systems}, volume = 24, number = 5, pages = {566--591}, urljournal = {http://www.acm.org/pubs/contents/journals/toplas/}, year = 2002, Xnote = {Extended abstract in \emph{ICALP'00}, LNCS 1853, Springer, 2000.}, abstract = {We propose an extension of the asynchronous pi-calculus in which a variety of security properties may be captured using types. The types are an extension of the Input/Output types for the pi-calculus in which I/O capabilities are assigned specific security levels. We define a typing system that ensures that processes running at security level sigma cannot access resources that have a security level higher than sigma. The notion of access control guaranteed by this system is formalized in terms of a Type Safety theorem. We then show that, for a certain class of processes, our system prohibits implicit information flow from high-level to low-level processes. We prove that low-level behavior can not be influenced by changes to high-level behavior. This is formalized as a Non-Interference Theorem with respect to may testing.}, file = {00TR-pisec}, pdf = {}, urltype = {http://www.cogs.susx.ac.uk/cgi-bin/htmlcogsreps?cs}, urlinstitution ={http://www.cogs.susx.ac.uk/}, } @InProceedings{00icalp, author = {Matthew Hennessy and James Riely}, title = {Information Flow vs. Resource Access in the Asynchronous Pi-Calculus}, booktitle = {Proceedings of the International Colloquium on Automata, Languages and Programming}, editor = {U. Montanari and J. Rolim and E. Welzl}, rate = {35\%}, volume = 1853, pages = {415--427}, year = 2000, month = aug, address = {Geneva}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, Xnote = {Full version available as Sussex CSTR 2000:03. Available from \url{http://www.cogs.susx.ac.uk/}}, file = {00icalp}, pdf = {}, urlbooktitle = {http://cui.unige.ch/~icalp/}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, } @InProceedings{00sas, author = {James Riely and Jan Prins}, title = {Flattening is an Improvement}, booktitle = {Proceedings of the Seventh Static Analysis Symposium SAS'2000}, year = 2000, pages = {360-376}, rate = {38\%}, month = jun, address = {Santa Barbara}, editor = {J.~Palsberg}, volume = 1824, series = {Lecture Notes in Computer Science}, publisher = {Springer}, abstract = {Flattening is a program transformation that eliminates nested parallel constructs, introducing flat parallel (vector) operations in their place. We define a sufficient syntactic condition for the correctness of flattening, providing a static approximation of Blelloch's ``containment''. This is acheived using a typing system that tracks the control flow of programs. Using a weak improvement preorder, we then show that the flattening transformations are intensionally correct for all well-typed programs.}, file = {00sas}, pdf = {}, urlbooktitle = {http://www.cis.ksu.edu/santos/sas/}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, } @Misc{99sl-draft, author = {James Riely and Matthew Hennessy}, title = {Secure Resource Access for Open Systems}, year = 1999, abstract = {In open distributed systems of mobile agents, where code from remote sites may run locally, protection of sensitive data and system resources is of paramount importance. We present a capability-based typing system that provides such protection, using a mix of static and runtime typing. We formalize security violations as runtime errors and prove that, using our semantics, runtime errors cannot occur at ``good'' sites, i.e., sites under control of a particular administrative domain.}, comment = {Manuscript}, file = {99sl-draft}, pdf = {}, } @PhdThesis{99diss, author = "James Riely", title = "Applications of Abstraction for Concurrent Programs", school = "University of North Carolina at Chapel Hill", year = 1999, abstract = {We study the use of abstraction to reason operationally about concurrent programs. Our thesis is that abstraction can profitably be combined with operational semantics to produce new proof techniques. We study two very different applications: In the first case, we develop a typing system for a nested data-parallel programming language and use it to prove the correctness of flattening, an important compilation technique. In the second, we demonstrate that abstract interpretations of values domains can be applied to process description languages, extending the applicability of finite-state methods to infinite-state processes.}, comment = {}, file = {99diss}, urlschool = {http://www.cs.unc.edu/}, } @Article{98TR-partial, author = {James Riely and Matthew Hennessy}, title = {Trust and Partial Typing in Open Systems of Mobile Agents}, journal = {Journal of Automated Reasoning}, year = {2003}, volume = {31}, doi = {http://dx.doi.org/10.1023/B:JARS.0000021016.61054.3b} urljournal = {http://www.kluweronline.com/issn/0168-7433}, number = {3-4}, pages = {335--370}, Xnote = {Extended abstract in \emph{POPL'99}, ACM Press, 1999}, Xnote = {Available from \protect\url{http://www.cogs.susx.ac.uk/}}, abstract = {We present a partially-typed semantics for Dpi, a distributed pi-calculus. The semantics is designed for mobile agents in open distributed systems in which some sites may harbor malicious intentions. Nonetheless, the semantics guarantees traditional type-safety properties at ``good'' locations by using a mixture of static and dynamic type-checking. We show how the semantics can be extended to allow trust between sites, improving performance and expressiveness without compromising type-safety.}, file = {98TR-partial}, longof = {99popl}, pdf = {}, urltype = {http://www.cogs.susx.ac.uk/cgi-bin/htmlcogsreps?cs}, urlinstitution ={http://www.cogs.susx.ac.uk/}, } @InProceedings{99popl, author = {James Riely and Matthew Hennessy}, title = {Trust and Partial Typing in Open Systems of Mobile Agents}, booktitle = {Conference Record of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, rate = {18\%}, pages = {93--104}, year = 1999, address = {San Antonio}, month = jan, publisher = {ACM Press}, Xnote = {Full version available as Sussex CSTR 1998:04. Available from \url{http://www.cogs.susx.ac.uk/}}, file = {99popl}, shortof = {98TR-partial}, pdf = {}, urlbooktitle = {http://www.cs.princeton.edu/~appel/popl99/}, urlpublisher = {http://www.acm.org}, } @InCollection{98TR-anetworks, author = {Matthew Hennessy and James Riely}, title = {Type-Safe Execution of Mobile Agents in Anonymous Networks}, editor = {J. Vitek and C. Jensen}, booktitle = {Secure Internet Programming: Security Issues for Distributed and Mobile Objects}, volume = {1603}, pages = {95--117}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, year = 1999, Xnote = {Preliminary version available as Sussex CSTR 1998:03. Available from \protect\url{http://www.cogs.susx.ac.uk/}}, abstract = {We study type-safety properties of open distributed systems of mobile agents, where not all sites are known to be well-typed. We adopt the underlying model of an anonymous network, allowing that code may be corrupted on transmission and that the source of incoming code is unknowable. Nonetheless, we are able to guarantee a weak form of type-safety at ``good'' sites using a mix of static and dynamic typing.}, htmlnote = {Preliminary version available as Sussex CSTR 1998:03.
Presented at Mobile Object Systems, (satellite of ECOOP '98)}, Xurlbooktitle = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-66130-1}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, file = {98TR-anetworks}, pdf = {}, } @InProceedings{98ecoop, author = {Matthew Hennessy and James Riely}, title = {Type-Safe Execution of Mobile Agents in Anonymous Networks}, booktitle = {Object-Oriented Technology. ECOOP'98 Workshop Reader }, publisher = {Springer}, note = {(Acceptance unknown)}, pages = 304, year = 1998, month = jul, address = {Brussles}, editor = {Demeyer, S. and Bosch, J.}, volume = 1543, series = {Lecture Notes in Computer Science}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, file = {98ecoop}, pdf = {}, } @Article{98TR-resources, author = {Matthew Hennessy and James Riely}, title = {Resource Access Control in Systems of Mobile Agents}, journal = {Information and Computation}, urljournal = {http://theory.lcs.mit.edu/~iandc/}, year = {2002}, volume = {173}, pages = {82--120}, Xnote = {Extended abstract in {\em 3rd International Workshop on High-Level Concurrent Languages (HLCL'98)}, volume~16 of {\em Electronic Notes in Theoretical Computer Science}, Elsevier, 1998}, abstract = {We describe a typing system for a distributed pi-calculus which guarantees that distributed agents cannot access the resources of a system without first being granted the capability to do so. The language studied allows agents to move between distributed locations and to augment their set of capabilities via communication with other agents. The type system is based on the novel notion of a location type, which describes the set of resources available to an agent at a location. Resources are themselves equipped with capabilities, and thus an agent may be given permission to send data along a channel at a particular location without being granted permission to read data along the same channel. We also describe a tagged version of the language, where the capabilities of agents are made explicit in the syntax. Using this tagged language we define access violations as runtime errors and prove that well-typed programs are incapable of such errors.}, Xhtmlnote = {Presented at MFPS XIV.
Preliminary version available as Sussex CSTR 1998:02.}, file = {98TR-resources}, longof = {98hlcl}, pdf = {}, urltype = {http://www.cogs.susx.ac.uk/cgi-bin/htmlcogsreps?cs}, urlinstitution ={http://www.cogs.susx.ac.uk/}, } @InProceedings{98hlcl, author = {Matthew Hennessy and James Riely}, title = {Resource Access Control in Systems of Mobile Agents}, booktitle = {3rd International Workshop on High-Level Concurrent Languages (HLCL'98)}, year = 1998, address = {Nice}, note = {(Acceptance unknown)}, pages = {1--15}, month = sep, editor = {Uwe Nestmann and {Benjamin C.} Pierce}, volume = {16(3)}, series = {Electronic Notes in Theoretical Computer Science}, publisher = {Elsevier}, Xnote = {Available from \protect\url{http://www.elsevier.com/locate/entcs}}, file = {98hlcl}, shortof = {98TR-resources}, pdf = {}, urlseries = {http://www.elsevier.com/locate/entcs}, urlbooktitle = {http://www.cs.auc.dk/hlcl98/}, urlpublisher = {http://www.elsevier.com}, } @InProceedings{98popl, author = {James Riely and Matthew Hennessy}, title = {A Typed Language for Distributed Mobile Processes}, booktitle = {Conference Record of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, rate = {18\%}, pages = {378--390}, year = 1998, address = {San Diego}, month = jan, publisher = {ACM Press}, abstract = {We describe a foundational language for specifying dynamically evolving networks of distributed processes, Dpi. The language is a distributed extension of the pi-calculus which incorporates the notions of remote execution, migration, and site failure. Novel features of Dpi include: A type system is proposed in which the types control the allocation of permissions; in well-typed processes all names are used in accordance with the permissions allowed by the types. We prove Subject Reduction and Type Safety Theorems for the type system. In the final section we define a semantic theory based on barbed bisimulations and discuss its characterization in terms of a bisimulation relation over a relativized labelled transition system.}, file = {98popl}, pdf = {}, urlbooktitle = {http://cm.bell-labs.com/cm/cs/who/dbm/popl98/}, urlpublisher = {http://www.acm.org}, } @Article{97TR-loc-fail, author = {James Riely and Matthew Hennessy}, title = {Distributed Processes and Location Failures}, journal = {Theoretical Computer Science}, year = {2001}, pages = {693--735}, volume = {226}, Xnote = {Extended abstract in \emph{ICALP'97}, LNCS 1256, Springer, 1997.}, Xhtmlnote = {Preliminary version available as Sussex CSTR 1997:02.}, abstract = {Site failure is an essential aspect of distributed systems; nonetheless its effect on programming language semantics remains poorly understood. To model such systems, we define a process calculus in which processes are run at distributed locations. The language provides operators to kill locations, to test the status (dead or alive) of locations, and to spawn processes at remote locations. Using a variation of bisimulation, we provide alternative characterizations of strong and weak barbed congruence for this language, based on an operational semantics that uses configurations to record the status of locations. We then derive a second, symbolic characterization in which configurations are replaced by logical formulae. In the strong case the formulae come from a standard propositional logic, while in the weak case a temporal logic with past time modalities is required. The symbolic characterization establishes that, in principle, barbed congruence for such languages can be checked efficiently using existing techniques.}, file = {97TR-loc-fail}, longof = {97icalp}, pdf = {}, urltype = {http://www.cogs.susx.ac.uk/cgi-bin/htmlcogsreps?cs}, urlinstitution ={http://www.cogs.susx.ac.uk/}, urljournal = {http://www.elsevier.com/locate/tcs}, } @InProceedings{97icalp, author = {James Riely and Matthew Hennessy}, title = {Distributed Processes and Location Failures}, booktitle = {Proceedings of the International Colloquium on Automata, Languages and Programming}, rate = {37\%}, pages = {471--481}, address = {Bologna}, month = jul, year = 1997, editor = {P. Degano and R. Gorrieri and A. Marechetti-Spaccamela}, volume = 1256, series = {Lecture Notes in Computer Science}, publisher = {Springer}, Xnote = {Full version available as Sussex CSTR 97/02, 1997. Available from \url{http://www.cogs.susx.ac.uk/}}, file = {97icalp}, shortof = {97TR-loc-fail}, pdf = {}, urlbooktitle = {http://www.cs.unibo.it/icalp97/}, urltype = {http://www.cogs.susx.ac.uk/cgi-bin/htmlcogsreps?cs}, urlinstitution ={http://www.cogs.susx.ac.uk/}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, } @InProceedings{95mppm, author = {James Riely and Jan Prins and {S. Purushothoman} Iyer}, title = {Provably Correct Vectorization of Nested-Parallel Programs}, booktitle = {Programming Models for Massively Parallel Computers (MPPM'95)}, editor = {W. K. Giloi and S. J\"ahnichen and B. D. Shriver}, note = {(Acceptance unknown)}, pages = {213--222}, publisher = {IEEE Computer Society Press}, year = 1995, address = {Berlin}, month = dec, abstract = {The work/step framework provides a high-level cost model for nested data-parallel programming languages, allowing programmers to understand the efficiency of their codes without concern for the eventual mapping of tasks to processors. Vectorization, or flattening, is the key technique for compiling nested-parallel languages. This paper presents a formal study of vectorization, considering three low-level targets: the EREW, bounded-contention CREW, and CREW variants of the VRAM. For each, we describe a variant of the cost model and prove the correctness of vectorization for that model. The models impose different constraints on the set of programs and implementations that can be considered; we discuss these in detail.}, file = {95mppm}, urlpublisher = {http://www.computer.org/}, } @InCollection{94dimacs, author = {Allen Goldberg and Peter Mills and Lars Nyland and Jan Prins and John Reif and James Riely}, title = {Specification and Development of Parallel Algorithms with the Proteus System}, booktitle = {Specification of Parallel Algorithms}, year = 1994, pages = {383--399}, editor = {G.~E.~Blelloch and K.~M.~Chandy and S.~Jagannathan}, series = {DIMACS Series in Discrete Mathematics and Theoretical Computer Science}, publisher = {AMS Press}, abstract = {The Proteus language is a wide-spectrum parallel programming notation that supports the expression of both high-level architecture-independent specifications and lower-level architecture-specific implementations. A methodology based on successive refinement and interactive experimentation supports the development of parallel algorithms from specification to various efficient architecture-dependent implementations. The Proteus system combines the language and tools supporting this methodology. This paper presents a brief overview of the Proteus system and describes its use in the exploration and development of several non-trivial algorithms, including the fast multipole algorithm for N-body computations.}, file = {94dimacs}, pdf = {}, urlpublisher = {http://www.ams.org/}, urlseries = {http://dimacs.rutgers.edu/Volumes/}, } @InCollection{94TR-proteus, author = {Allen Goldberg and Jan Prins and John Reif and Rickard Faith and Zhiyong Li and Peter Mills and Lars Nyland and Daniel Palmer and James Riely and Stephen Westfold}, title = {The Proteus System for the Develepment of Parallel Applications}, booktitle = {Prototyping Languages and Prototyping Technology}, publisher = {Unpublished}, NOpublisher = {Springer}, NOpages = {151--190}, year = 1994, editor = {M.~Harrison}, abstract = {We summarize work on the Proteus project for prototyping and refining parallel applications. We describe the programming notation, the development methodology, the refinement system, and performance metrics. Several case studies are presented.}, file = {94TR-proteus}, } @InProceedings{94concur, author = {Rance Cleaveland and James Riely}, title = {Testing-Based Abstractions for Value-Passing Systems}, booktitle = {CONCUR '94: Concurrency Theory}, url = {http://dx.doi.org/10.1007/BFb0015023}, rate = {27\%}, year = 1994, month = aug, address = {Uppsala}, editor = {B.~Jonsson and J.~Parrow}, volume = 836, series = {Lecture Notes in Computer Science}, publisher = {Springer}, pages = {417--432}, abstract = {This paper presents a framework for the abstract interpretation of processes that pass values. We define a process description language that is parameterized with respect to the set of values that processes may exchange and show that an abstraction over values induces an abstract semantics for processes. Our main results state that if the abstract value interpretation safely/optimally approximates the ground interpretation, then the resulting abstracted processes safely/optimally approximate those derived from the ground semantics (in a precisely defined sense). As the processes derived from an abstract semantics in general have far fewer states than those derived from a concrete semantics, our technique enables the automatic analysis of systems that lie beyond the scope of existing techniques.}, file = {94concur}, pdf = {}, urlseries = {http://link.springer.de/series/lncs/}, urlpublisher = {http://www.springer.de/}, } talk{, author = {James Riely}, title = {}, booktitle = {}, address = {}, month = , year = , } @talk{05sass, author = {James Riely}, title = {Modern Runtime Systems: Java Virtual Machine and Microsoft Common Language Runtime}, booktitle = {Silver Anniversary Seminar Series}, file = {05sass}, pdf = {}, urlbooktitle = {http://www.cti.depaul.edu/sass/introduction.htm}, address = {DePaul CTI}, month = jul, year = 2005, abstract = {The JVM and CLR sitting on most desktop computers include sophisticated technology that, until very recently, was confined to unpopular programming languages used mostly in research laboratories. This talk will describe what\u2019s going on beneath the hood of these now ubiquitous multi-megabyte behemoths. Topics will include dynamic class loading, just-in-time compilation, bytecode verification, security management and garbage collection.} } @talk{04foal, author = {James Riely}, title = {Formal AOP: Opportunities Abound}, booktitle = {FOAL 2004}, urlbooktitle = {http://www.cs.iastate.edu/~leavens/FOAL/index-2004.shtml}, htmlnote = {Slides from invited lecture}, file = {04foal}, pdf = {}, address = {Lancaster}, month = mar, year = 2004, abstract = { Aspect-oriented programming (AOP) is a polarizing paradigm -- attractive to some and repulsive to others. On the up side, AOP allows for new forms of encapsulation: each concern (eg, functionality, security) can be coded separately rather than interleaved in the same code base. On the down side, AOP destroys old forms of encapsulation: straight-line code no longer runs in a straight line. Static weaving has proven eminently practical, but many potential applications depend upon dynamic properties which do not lend themselves to this implementation technique. To realize its full potential, AOP must become both more controlled and more expressive. In each case, the issues are complex and difficult to arbitrate without formal models.} } @talk{03mspls, author = {James Riely}, title = {A Calculus of Aspect-Oriented Programs}, booktitle = {MSPLS 2003}, urlbooktitle = {http://dynamo.ecn.purdue.edu/~mspls/}, address = {Chicago, IL}, month = nov, year = 2003, } @talk{03stevens, author = {James Riely}, title = {A Calculus of Aspect-Oriented Programs}, address = {Stevens Institute of Technology}, urladdress = {http://www.cs.stevens.edu/}, month = apr, year = 2003, host = {Adriana Compagnoni}, } @talk{98cambridge, author = {James Riely}, title = {Resource Access Control in Systems of Mobile Agents}, address = {Cambridge Univ\xperiod}, urladdress = {http://www.cl.cam.ac.uk/}, month = jan, year = 1998, } @talk{97confer, author = {James Riely}, title = {Distributed Processes and Location Failures}, booktitle = {CONFER-2 WG Workshop}, urlbooktitle = {http://www.cs.unibo.it/~asperti/CONFER/bologna.html}, address = {Bologna}, month = mar, year = 1997, } @talk{94madrid, author = {James Riely}, title = {Testing-Based Abstractions for Concurrent Systems}, address = {Univ.\ Polit\'ecnica de Madrid}, urladdress = {http://www.upm.es/}, month = may, year = 1994, } \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Univ\xperiod of Illinois at Chicago} {1999} {}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Univ\xperiod of Delaware} {1999} {}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Colorado State Univ\xperiod} {1999} {}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Old Dominion Univ\xperiod} {1999} {}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Univ\xperiod of Texas at Dallas} {1999} {}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Univ\xperiod of Maryland Baltimore County} {1999} {}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Stevens Institute of Technology} {March 1999} {Karen Bernstein}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {DePaul Univ\xperiod} {March 1999} {Karen Bernstein}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Illinois Institute of Technology} {1999} {}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Santa Clara Univ\xperiod} {1999} {}. \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {Notre Dame Univ\xperiod} {1998} {}, \jobtalk {Resource Access Control in Systems of Mobile Agents} {The Kestrel Institute} {January 1998} {}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {DePaul Univ\xperiod} {May 1998} {Alan Jeffrey}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {\acro{UNC} Wilmington} {1998} {}, \jobtalk {Trust and Partial Typing in Open Systems of Mobile Agents} {North Carolina \acro{A\&T} Univ\xperiod} {1998} {}. \jobtalk {Abstract Interpretation of Parametric Value-Passing Process Calculi} {Univ.\ of Sussex} {July 1995} {Matthew Hennessy}, \jobtalk {Testing-based abstractions for message-passing systems} {\acro{UNC} Charlotte} {April 1995} {Bill Chu}, \jobtalk {Testing-based abstractions for message-passing systems} {\acro{NC} State Univ\xperiod} {January 1995} {Alan Tharp}.