%================================================= %== BIBLIOGRAPHIE == %================================================== %=========== BOOKS ====================== @Book{Java_tutorial, author = {M. Campione and K. Walrath}, title = {The Java Tutorial (Object-Oriented Programming for the Internet)}, publisher = {Addison--Wesley}, address = {}, year = 1998} @Book{Java_specif, author = {J. Gosling and B. Joy and G. Steele}, title = {The Java Language Specification}, publisher = {Addison--Wesley}, address = {}, year = 1996} @Book{Java_threads, author = {S. Oaks and H. Wong}, title = {Java Threads}, publisher = {O'Reilly}, pages = {29--33}, address = {}, year = 1997} @book{Mey92, author= {B. Meyer}, title="{E}iffel, the {L}anguage", publisher="Prentice-Hall", address={}, year=1992 } @Book{shaw96a, author = "Mary Shaw and David Garlan", title = "Software Architecture", publisher = "PH", year = "1996", address = "Upper Saddle River, NJ 07458", note = "INF 410/359", } @Article{Reiss:1990:CTU, author = "Steven P. Reiss", title = "Connecting tools using message passing in the {Field} environment", journal = "IEEE Software", volume = "7", number = "4", pages = "57--66", month = jul, year = "1990", coden = "IESOEG", ISSN = "0740-7459", bibdate = "Sat Jan 25 07:35:26 MST 1997", abstract = "Field connects tools with selective broadcasting, which follows the Unix philosophy of letting independent tools cooperate through simple conventions. Field demonstrates that this simple approach is feasible and desirable.", acknowledgement = ack-nhfb, affiliation = "Brown Univ, Providence, RI, USA", classification = "722; 723", journalabr = "IEEE Software", keywords = "Brown Workstation Environment; Computer Operating Systems; Computer Software --- Software Engineering; Design; Message Passing; Software Development Environments", } %============= OUTILS DU COMMERCE ===================== @Article{JDB-article, author = "Russel Winder and Joe Nicolson", title = "{JDB}: an Adaptable Interface for Debugging", journal = "Software--Practice and Experience", volume = "18", number = "3", pages = "221--238", month = mar, year = "1988", coden = "SPEXBL", ISSN = "0038-0644", bibdate = "Sat May 31 13:36:16 MDT 1997", acknowledgement = ack-nhfb, } @techreport{JDI, title={{J}ava {D}ebugger {I}nterface}, author={{Sun}}, institution={Palo Alto, Ca}, type={Commercial Product}, number="available at ", year={1998} } @techreport{JProbe, title={{JP}robe {P}rofiler}, author={{Nova Software Labs}}, institution={Paris, France}, type={Commercial Product}, number="available at ", year={1998} } @techreport{jdb, title={{JDB} {T}he {J}ava {D}ebugger}, author={{Sun}}, institution={Palo Alto, CA}, type={Commercial Product}, number="available at ", year={1997} } @techreport{Metamata, title={{M}etamata {D}ebug}, author={{Metamata}}, institution={Fremont, SA}, type={Commercial Product}, number="available at ", year={1997} } @techreport{NuMega, title={{N}u{M}ega {JC}heck}, author={{NuMega Technologies}}, institution={Compuware, Nashua, NH}, type={Commercial Product}, number="available at ", year={1998} } @techreport{Supercede, title={{S}UPER{C}EDE {J}AVA}, author={{SuperCede, Inc.}}, institution={Bellevue, WA}, type={Commercial Product}, number="available at ", year={1998} } @Manual{cent92, title = "Code{C}enter, The Programming Environment", key = "CenterLine", organization = "CenterLine Software", address = "Cambridge, MA", year = "1992", } @techreport{Dichter, title={{We test the top 6 Java visual IDEs}}, author={C. Dichter}, institution={JavaWorld: IDG's magazine for the Java community}, type={Product Reviews}, number={available at }, year={1998} } @techreport{Dyer:1998:CAS, title={{Can {Assure} save {Java} from the perils of multithreading?}}, author={D. Dyer}, institution={JavaWorld: IDG's magazine for the Java community}, type={article}, number={available at }, year={1998} } @techreport{Metrowerks:1995:MCS, title={{M}etrowerks {C}ode{W}arrior}, author={{Metrowerks}}, institution={Austin, TX}, type={Commercial Product}, number="available at ", year={1995} } @InProceedings{Price91, author = "Blaine A. Price and Ronald M. Baecker", title = "The Automatic Animation of Concurrent Programs", booktitle = "First Moscow International HCI'91 Workshop Proceedings", series = "III. Visualization", pages = "128--137", year = "1991", copyright = "(c) Copyright 1991 Intl. Centre for Scientific \& Technical Information", mrnumber = "C.EWHCI.91.128", abstract = "Much of the program visualization research to date has been devoted to hand-crafted animations of small sequential programs for use in computer science education. Instead, our work focuses on the development of automatic concurrent program visualization tools for use in software engineering. This paper describes a framework for concurrent program animation and a prototype tool based on this framework. Our user testing experiments with the prototype showed a significant increase in programmer insights when compared with conventional tools.", } @InProceedings{Muller:1990:PAU, author = "H. Muller and J. Winckler and S. Grzybek and M. Otte and B. Stoll and F. Equoy and N. Higelin", title = "{PASTIS}-program animation using {X}", editor = "Anonymous", booktitle = "European {X} Window System Conference", publisher = "CEP Consultants", address = "Edinburgh, UK", year = "1990", pages = "104--111", year = "1990", bibdate = "Wed Oct 30 06:04:36 MST 1996", abstract = "The software animation system PASTIS (Program Animation System with Interactive Solutions) for program animation with emphasis on the visualization of the dynamic behavior of algorithms and data structures is presented. Its main properties are unmodified source code of the visualized program, concurrent multiple and hierarchical views on algorithms and data structures, and interactive alterations of views during run time. The interface between program and animations is a relational data model. PASTIS is distinguished by high modularity and strict separation of its components. This makes it particularly suitable for distributed computing environments. A prototype of PASTIS was implemented under UNIX using the GNU source level debugger gdb and the X-window system.", acknowledgement = ack-nhfb, affiliation = "Inst. fur Inf., Freiburg Univ., Germany", classification = "C6115 (Programming support); C6180G (Graphical user interfaces); C6130B (Graphics techniques)", keywords = "Concurrent views; Software animation system; PASTIS; Program animation; Visualization; Dynamic behavior; Algorithms; Data structures; Hierarchical views; Interactive alterations; Relational data model; Modularity; Distributed computing environments; UNIX; GNU source level debugger; Gdb; X-window system", thesaurus = "Computer animation; Data structures; Graphical user interfaces; Visual programming", } @Article{Myers:1983:IAS, author = "B. A. Myers", key = "Myers", title = "Incense: {A} System for Displaying Data Structures", journal = "Computer Graphics", volume = "17", number = "3", pages = "115--125", month = jul, year = "1983", coden = "CGRADI", ISSN = "0097-8930", bibdate = "Mon Mar 4 10:01:14 1985", abstract = "Many modern computer languages allow the programmer to define and use a variety of data types. Few programming systems, however, allow the programmer similar flexibility when displaying the data structures for debugging, monitoring and documenting programs. Incense is a working prototype system that allows the programmer to interactively investigate data structures in actual programs. The desired displays can be specified by the programmer or a default can be used. The default displays provided by Incense present the standard form for literals of the basic types, the actual names for scalar types, stacked boxes for records and arrays, and curved lines with arrowheads for pointers. In addition to displaying data structures, Incense also allows the user to select, move, erase and redimension the resulting displays. These interactions are provided in a uniform, natural manner using a pointing device (mouse) and keyboard.", conference = "held in Detroit, Michigan; 25--29 July 1983", keywords = "human factors; I35 data structures, I35 data types, design; languages", } @techreport{IDEreviews, title={{Capsule Reviews of JAVA tools}}, author={D. Dyer}, institution={Andromeda Software}, type={Product Reviews}, number={Available at }, year={1998} } @techreport{Javelin, title={{Javelin}}, author={{Step Ahead Software Pty Ltd}}, institution={NSW 2077 Australia}, type={Commercial Product}, number={available at }, year={1998} } @techreport{Kawa, title={{Kawa}}, author={{Tek-Tools, Inc}}, institution={Dallas TX}, type={Commercial Product}, number={available at }, year={1998} } @techreport{vajava, title={{Visual Age for Java}}, author={{IBM Corporation}}, type={Commercial Product}, number={available at }, year={1997} } @book{VisualJ++, title={Using Visual J++}, author={P. Greg}, publisher={Que}, year={1996}, note={ISBN 078970899X} } @book{JavaWS, title={Teach Yourself SunSoft Java Workshop in 21 Days}, author={L. Lemay and Charlesworth}, publisher={SAMS}, year={1996}, note={ISBN 1575211599} } @techreport{Beck, title={Object Explorer for Visual Works}, author={K. Beck}, institution={First Class Software, Inc.}, type={Commercial Product}, number="available at " } @techreport{BridgePoint, title={Bridge{P}oint}, author={{Project Technology, Inc.}}, institution={Berkeley, California}, type={Commercial Product}, number="available at " } @techreport{SES, title={{SES}/objectbench, {SES}/workbench }, author={{SES, Inc.}}, institution={Austin, Texas}, type={Commercial Product}, number="available at " } @techreport{ObjecTime, title={Objec{T}ime}, author={ObjecTime Ltd.}, institution={Ontario, Canada}, type={Commercial Product}, number="available at " } %============ ARTICLES ==================== %=========== Semantique naturelle et preuves @InProceedings{Despeyroux86, author={Jo{\"e}lle Despeyroux}, title={Proof of Translation in Natural Semantics}, pages={193--205}, crossref={LICS1}, source={ftp://theory.lcs.mit.edu/pub/meyer/lics.bib} } @Proceedings{LICS1, title={Proceedings, Symposium on Logic in Computer Science}, booktitle={Proceedings, Symposium on Logic in Computer Science}, year=1986, month={16--18 } # jun, address={Cambridge, Massachusetts}, organization={IEEE Computer Society}, crossrefonly=1, comment={IEEE Computer Society Order Number 720; Library of Congress Number 86-81090; IEEE Catalog Number 86CH2321-8; ISBN 0-8186-0720-3}, source={ftp://theory.lcs.mit.edu/pub/meyer/lics.bib} } %=========== Objets @book{Shlaer, title={Object Lifecyles: Modeling the World in States}, author={S. Shlaer and S. Mellor}, publisher={Prentice Hall, Englewood Cliffs, NJ.}, year={1992} } @article{Car90a, author= {D. Caromel}, title="{C}oncurrency: an {O}bject-{O}riented {A}pproach", journal="TOOLS'90, Paris", year=1990 } @article{Car93, author= {D. Caromel}, title="{T}owards a {M}ethod of {O}bject-{O}riented {C}oncurrent {P}rogramming", journal="Communications of the ACM, 36 (9), pages 90-102", year=1993 } @inproceedings{Chambers97, author = {D. Grove and G. DeFouw and J. Dean and G. Chambers}, title = {Call Graph Construction in Object-Oriented Languages}, booktitle={Proc. OOPSLA'97 (Object-Oriented Programming: Systems, Languages, and Applications)}, publisher={ACM Press, Sigplan Notices}, volume = "32, number 10", year={1997}, month={Oct} } @inproceedings{Holzle97, author = {R. Lencevicius and U. Hölzle and A. K. Singh}, title = {Query-Based Debugging of Object-Oriented Programs}, booktitle={Proc. OOPSLA'97 (Object-Oriented Programming: Systems, Languages, and Applications)}, publisher={ACM Press, Sigplan Notices}, volume = "32, number 10", year={1997}, month={Oct} } @article{Holzle96, author= {U. Hölzle and O. Agensen}, title="Dynamic vs Static Optimization Techniques for Object-Oriented Languages", journal="Theory and practice of Object Systems", volume={1}, number={3}, year={1996} } @inproceedings{Kent97, author = {S. Kent}, title = {Constraint Diagrams: Visualizing Invariants in Object-Oriented Models}, booktitle={Proc. OOPSLA'97 (Object-Oriented Programming: Systems, Languages, and Applications)}, publisher={ACM Press, Sigplan Notices}, volume = "32, number 10", year={1997}, month={Oct} } @InProceedings{Frie89a, author = "G. Friedrich and W. H. and C. Stary and M. Stumptner", title = "ObjView: {A} Task-Oriented, Graphics-Based Tools for Object Visualization and Arrangement", booktitle = "Proc. ECOOP '89", publisher = "Cambridge University Press", pages = "299--310", address = "Nottingham", month = jul, year = "1989", keywords = "olit-oopl objview ecoop89", } @book{Mey88, author= {B. Meyer}, title="{O}bject-{O}riented {S}oftware {C}onstruction", publisher="Prentice-Hall", address={}, year=1988 } @article{Wie91, author= {R. J. Wieringa}, title="{A} {F}ormalization of {O}bjects {U}sing {E}quational {D}ynamic {L}ogic", journal="DOOD'91, LNCS N. 566, pages 430-452", year=1991 } @InProceedings{Haar90a, author = "V. Haarslev and R. M{\"o}ller", title = "A Framework for Visualizing Object-Oriented Systems", booktitle = "Proc. OOPSLA/ECOOP '90, ACM SIGPLAN Notices 25 (10)", pages = "237--244", month = oct, year = "1990", keywords = "olit oopsla90 ecoop90", } @InProceedings{Pauw93a, author = "W. De Pauw and R. Helm and D. Kimelman and J. Vlissides", title = "Visualizing the Behavior of Object-Oriented Systems", booktitle = "Proc. OOPSLA '93, ACM SIGPLAN Notices, 28 (10)", pages = "326--337", month = oct, year = "1993", keywords = "olit oopsla93" } @InProceedings{Nier90b, author = "O. Nierstrasz and M. Papathomas", title = "Viewing Objects as Patterns of Communicating Agents", booktitle = "Proc. OOPSLA/ECOOP '90, ACM SIGPLAN Notices, 25 (10)", year = "1990", url = "ftp://iamftp.unibe.ch/pub/scg/Papers/viewingObjectsAsPatterns.ps.gz", abstract = "Following our own experience developing a concurrent object-oriented language as well of that of other researchers, we have identified several key problems in the design of a obc model compatible with the mechanisms of object-oriented programming. We propose an approach to language design in which an executable notation describing the behaviour of communicating agents is extended by syntactic patterns that encapsulate language constructs. We indicate how various language models can be accommodated, and how mechanisms such as inheritance can be modeled. Finally, we introduce a new notion of types that characterizes concurrent objects in terms of their externally visible behaviour.", } @Book{Burn95a, editor = "M. Burnett and A. Goldberg and T. Lewis", title = "Visual Object-Oriented Programming, Concepts and Environments", publisher= "Manning Publications", address = "Greenwich, CT", year = "1995", ISBN = "1-884777-01-5" } @InProceedings{Koba94, author = "N. Kobayashi and A. Yonezawa", title = "Type-Theoric Foundations for Concurrent Object-Oriented Programming", booktitle = "Proc. OOPSLA '94, ACM SIGPLAN Notices", month = oct, year = "1994", } @InProceedings{Vasc93a, author = "V. Vasconcelos and M. Tokoro", title = "A Typing System for a Calculus of Objects", booktitle = "Object Technologies for Advanced Software, First JSSST International Symposium", series = "LNCS 742", pages = "460--474", month = nov, year = "1993", keywords = "olit isotas93", abstract = "The present paper introduces an implicitly typed object calculus intended to capture intrinsic aspects of concurrent objects communicating via asynchronous message passing, together with a typing system assigning typings to terms in the calculus. Types meant to describe the kind of messages an object may receive are assigned to the free names in a program resulting in a scenario where a program is assigned multiple name-type pairs, constituting a typing for the process. Programs that comply to the typing discipline are shown not to suffer from runtime errors. Furthermore the calculus possesses a notation of principal typings, from which all typings that make a program well-typed can be extracted. We present an efficient algorithm to extract the principal typing of a process.", } %========== Parallelisme @incollection{PPUCDC, author={D. Caromel and F. Belloncle and Y. Roudier}, title= {The C++// System}, editor= {G. Wilson and P. Lu}, booktitle = {Parallel Programing Using C++}, note={To Appear}, year = 1996, publisher= "MIT Press" } @book{PPUC, editor= {G. Wilson and P. Lu}, title = {Parallel Programing Using C++}, note={To Appear}, year = 1996, publisher= "MIT Press" } @article{Car90, author= {D. Caromel}, title="Concurrency and Reusability: From Sequential to Parallel", journal="Journal of Object-Oriented Programming, 3(3)", year=1990 } @article{Car91, author= {D. Caromel}, title="Programmation {P}arall\`ele {A}synchrone et {I}mp\'e\-ra\-tive\,: Etudes et Propositions", journal="Th\`ese de Doctorat de l'Universit\'e de Nancy I, France, Fevrier", year=1991 } @book{cacm, key="cacm", title="Concurrent Object-Oriented Programming", publisher="Communications of the ACM, 36 (9)", note={Special issue}, year=1993 } @InProceedings{Amer87b, author = "P. America", title = "Inheritance and Subtyping in a Parallel Object-Oriented Language", booktitle = "Proc. ECOOP '87", series = "LNCS 276", pages = "234--242", address = "Paris, France", month = jun , year = "1987", keywords = "olit-obcl inheritance types pool ecoop87", } @article{Ame89, author= {P. America}, title="Issues in the {D}esign of a {P}allel {O}bject-{O}riented {L}anguage", journal="Formal Aspects of Computing, 1", pages= "366--411", year=1989 } @article{Wal00, author= {D. Walker}, title="{P}rocess {C}alculus and {P}arallel {O}bject-{O}riented {P}rogramming {L}anguages", journal="", year=1900 } @article{SNW93, author= {V. Sassone and M. Nielsen and G. Winskel}, title="{A} {C}lassification of {M}odels for {C}oncurrency", journal="LNCS: CONCUR'93, Springer-Verlag", year=1993 } @article{Sag95, author= {D. Sagnol}, title="$\pi$-calcul {P}our les {L}angages \`a {O}bjets {P}arall\`eles", journal="Rapport de DEA, Universit\'e de Nice-Sophia Antipolis", year=1995 } @Book{Yone87a, author = "A. Yonezawa and M. Tokoro", title = "Object-Oriented Concurrent Programming", publisher = "MIT Press", address = "Cambridge, Mass.", year = "1987", keywords = "olit-obc oobib(obcp) book scglib", } @InProceedings{Hond91a, author = "K. Honda and M. Tokoro", title = "An Object Calculus for Asynchronous Communication", booktitle = "Proc. ECOOP '91", series = "LNCS 512", pages = "133--147", address = "Geneva, Switzerland", month = jul, year = "1991", keywords = "pcalc-obc mobility equivalence ecoop91", } @InProceedings{Nier89c, author = "O. Nierstrasz", title = "Two Models of Concurrent Objects", booktitle = "ACM SIGPLAN Notices 24 (4), Proc. Workshop on Object-Based Concurrent Programming (San Diego, Sept 1988)", pages = "174--176", month = apr, year = "1989", keywords = "olit-obc abacus obcp89", } @InProceedings{Toko94a, author = "M. Tokoro and K. Takashio", title = "Toward Languages and Formal Systems for Distributed Computing", booktitle = "Proc. of the ECOOP '93 Workshop on Object-Based Distributed Programming", series = "LNCS 791", pages = "93--110", year = "1994", keywords = "olit-obc obdp93", abstract = "In this paper, we attempt to reveal the most essential properties of distributed computations. We claim that the notions of asynchrony, real-time, and autonomy are vitally important to a widely distributed, open-ended, ever-changing environment. We then propose a programming language, called DROL, for asynchronous real-time computing. It supports self-contained active objects that have threads of control and a clock, and introduces the notion of timed invocation, that guarantees the survivability of each active object. We place DROL as a first step in constructing programming languages to realize the above three notions. We also classify distributed computation into four forms according to asynchrony and real-time properties, and try to develop formalisms for the four categories based on a process calculus. The formalisms allow us to describe and analyze both globally and locally temporal properties as well as the behavioral properties of distributed objects and the interactions among them. We discuss issues remaining to be solved and suggest some possibilities for future work.", } @InProceedings{Wegn92a, author = "P. Wegner", title = "Design Issues for Object-Based Concurrency", booktitle = "Proc. of the ECOOP '91 Workshop on Object-Based Concurrent Computing", series = "LNCS 612", pages = "245--256", year = "1992", keywords = "olit-obc obc91", } %========== Centaur @inproceedings{Centaur, author= {P. Borras and et al}, title="CENTAUR: the {S}ystem", booktitle="SIGSOFT'88 Third Annual Symposium on Software Development Environments", address={Boston}, year=1988 } @article{Met83, author= {G. Kahn and B. Lang and B. M\'{e}l\`{e}se}, title="{M}etal : {A} {F}ormalism to {S}pecify {F}ormalisms", journal="Science of Computer Programming, Volume 3, North-Holland", year=1983 } @article{Ppm86, author= {E. Morcos-Chounet and A. Conchon}, title="PPML: {A} {G}eneral {F}ormalism to {S}pe\-ci\-fy {P}ret\-ty-prin\-ting ", journal="Proc. of the IFIP Con\-gress Du\-blin, North-Hol\-land", year=1986 } @techreport{Typol, author= {T. Despeyroux}, title="{T}ypol: {A} {F}ormalism to {I}mplement {N}atural {S}emantics", institution="INRIA", type= {Research Report}, number= 94, year=1988 } @inproceedings{Kahn87, author= {G. Kahn}, title="{N}atural {S}emantics", booktitle="Proc. of Symposium on Theoretical Aspects of Computer Science, Passau, Germany, LNCS 247", year=1987 } %========== Semantique @inproceedings{Fuj, author = "Attali, I. and Caromel, D. and Russo, M.", title = "{A formal and executable semantics for Java}", booktitle = "{Proceedings of Formal Underpinnings of Java, an OOPSLA'98 Workshop}", address = "{Vancouver, CA}", year = "1998", month = "October", note="file://babar.inria.fr:/pub/croap/mrusso/OopslaWorkshop98.ps.gz", publisher = "Technical Report, Princeton University" } @inproceedings{Sisal, author= {I. Attali and D. Caromel and A. Wendelborn}, title={{A} {F}ormal {S}emantics and an {I}nteractive {E}nvironment for {S}isal}, booktitle={Tools and Environment for Parallel and Distributed Systems}, publisher = "Kluwer Academic Publishers", year = "1996", } @inproceedings{ACO93, author= {I. Attali and D. Caromel and M. Oudshoorn}, title="{A} {F}ormal {D}efinition of the {D}ynamic {S}emantics of the {E}iffel {L}anguage", booktitle = {Proc. of ACSC'16}, address= {Adelaide, Australia}, month = {February}, year=1993 } @article{ACE96, author = {I. Attali and D. Caromel and S. O. Ehmety}, title = {A {N}atural {S}emantics for {E}iffel {D}ynamic {B}inding}, journal={ACM Transactions on Programming Languages and Systems (TOPLAS)}, volume={18}, number={5}, month={Novembre}, year={1996} } @inproceedings{ACEL96, author = {I. Attali and D. Caromel and S. O. Ehmety and S. Lippi}, title = {Semantic-based visualization for parallel object-oriented programming}, booktitle={Proc. OOPSLA'96 (Object-Oriented Programming: Systems, Languages, and Applications)}, publisher={ACM Press, Sigplan Notices}, volume = "31, number 10", year={1996}, month={Oct} } @techreport{ACE95a, author= {I. Attali and D. Caromel and S.O. Ehmety}, title="{A} {N}atural {S}emantics for the {E}iffel {D}ynamic {B}inding", type = "Research Report", institution = "I3S CNRS", number = "95-60", year=1995 } @techreport{ACE95b, author= {I. Attali and D. Caromel and S.O. Ehmety}, title="{A} {N}atural {S}emantics for the {E}iffel// {L}anguage", type = "Research Report", institution = "INRIA", number = 2732, year=1995 } @article{ACE95c, author= {I. Attali and D. Caromel and S.O. Ehmety}, title="{U}ne {S}\'emantique {O}p\'erationnelle pour le {L}angage {E}iffel//", journal="Journ\'ees du GDR Programmation, Grenoble, 22-24 Novembre", year=1995 } @techreport{Plotkin81, author= {G. D. Plotkin}, title="{A} {S}tructural {A}pproach to {O}perational {S}emantics", type={Report}, institution={DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark}, year=1981 } @article{Knu68, author= {D.E. Knuth}, title="{S}emantics of {C}ontext-free {L}anguage", journal="Math. Systems Theory, N. 2", year=1968 } @article{Knu71, author= {D.E. Knuth}, title="{S}emantics of {C}ontext-free {L}anguage", journal="Math. Systems Theory, N. 5", year=1971 } @article{Str66, author= {C. Strachey}, title="{T}owards a {F}ormal {S}emantics", journal="{F}ormal {L}anguage {D}escription for {C}omputer {P}rogramming (T.B. Steel editeur)", year=1966 } @inproceedings{ABK86, author= {P. America and J. D. Bakker and J. N. Kok and J. Rutten}, title="{O}perational {S}emantics of a {P}arallel {O}bject-{O}riented {L}anguage ({P}{O}{O}{L})", booktitle="Proc. of the 13th Symposium on Principles of Programming Languages", adress={St. Petersburg, Florida}, year=1986 } @article{ABK89, author= {P. America and J. D. Bakker and J. N. Kok and J. Rutten}, title="{D}enotational {S}emantics of a {P}arallel {O}bject-{O}riented {L}anguage ({P}{O}{O}{L})", journal="Information and Computation 83, 152-205", year=1989 } @misc{JP93, author= {G. Jalloul and J. Potter}, title="{A}n {O}perational {S}emantics for a {M}odel of {C}oncurrent {E}iffel", note="TR UTS-SOCS-93, 10", year=1993 } @article{Wal91, author= {D. Walker}, title="{P}i-{C}alculus {S}emantics of {O}bject-{O}riented {P}rogramming {L}angage", journal="Proc. TACS'91, Springer-Verlag, LNCS Vol. 526, pages 532-547", year=1991 } @article{OH86, author= {E.R. Olderog and C.A.R Hoare}, title="{S}pecification-{O}riented {S}emantics for {C}ommunicating {P}rocesses", journal="Acta Informatica, Vol. 23, pages 167-183", year=1986 } @InProceedings{Lamp:hoa, author = "L. Lamport", title = "The `Hoare Logic' of Concurrent Programs", booktitle = "Acta Informatica 14", year = "1980", editor = "Springer-Verlag", pages = "21--37", enteredby = "Glenn S Benson (benson at dove)", timestamp = "6-Apr-89, 3:22pm", } @article{BL95, author= {F. Boussinot and C. Laneve}, title="{T}wo {S}emantics for a {L}anguage of {R}eactive {O}bjects", journal="Rapport de recherche INRIA, N. 2511, mars", year=1995 } @article{Che92, author= {F. Cherief}, title="{C}ontributions \`a la {S}\'emantique du {P}arall\'elime: {B}isimulations pour le {R}affinement et le {V}rai {P}arall\'elisme", journal="These de l'Institut National Plytechnique de Grenoble, octobre", year=1992 } @InProceedings{Hond92d, author = "Kohei Honda and Mario Tokoro", editor = "O. Nierstrasz and M. Tokoro and P. Wegner", title = "On Asynchronous Communication Semantics", booktitle = "Proc. of the ECOOP '91 Workshop on Object-Based Concurrent Computing", series = "LNCS 612", pages = "21--51", publisher = "Springer-Verlag", year = "1992", keywords = "pcalc-obc mobility equivalence concurrency91 binder", } %============ Logique @book{Gen69, author= {G. Gentzen}, title="{I}nvestigation into {L}ogical {D}eduction", publisher="Thesis 1935, reprinted in The Collected Papers of Gerhard Gentzen", address={E.~Szabo, North-Holland, Amsterdam"}, year=1969 } %============ Preuves @article{Gau80, author= {M.C. Gaudel}, title="{G}\'en\'eration et {P}reuve de {C}ompilateurs {B}as\'es sur une {S}\'emantique {F}ormelle des {L}angages de Progarmmation", journal="Th\`ese, Nancy, Mars", year=1980 } @article{Boe90, author= {F.S. de~Boer}, title="{A} {P}roof {S}ystem for the {L}anguage {P}{O}{O}{L}", journal="Foundations of {O}bject-{O}riented {L}anguages, LNCS N. 489, pages 125-150", year=1990 } %========== Program properties @InProceedings{Holzmann99d, author = "Stefan Leue and Gerard J. Holzmann", title = "{V}-Promela: {A} Visual, Object-Oriented Language for Spin", journal = "Proc. Second IEEE International Symposium on Object-Oriented Real-Time Distributed Computing", year = "1999", month = may, address = "Saint Malo, France", publisher = "IEEE Computer Society Press", } @InProceedings{MeyerPoetzsch-Heffter00, author = { J. Meyer and A. Poetzsch-Heffter }, title = { {A}n {A}rchitecture for {I}nteractive {P}rogram {P}rovers}, booktitle = { 6th International Conference, TACAS}, series = { Lecture Notes in Computer Science }, year = 2000, note = {to appear}, publisher = { Springer-Verlag }, } @InCollection{MuellerPoetzsch-Heffter99, author = {M{\"u}ller, P. and Poetzsch-Heffter, A.}, title = {Modular Specification and Verification Techniques for Object-Oriented Software Components}, booktitle = {Foundations of Component-Based Systems}, publisher = {Cambridge University Press}, year = 1999, editor = {Leavens, G. T. and Sitaraman, M.}, note = {(to appear)} } @InProceedings{Poetzsch-HeffterMueller99, author = { Poetzsch-Heffter, A. and M{\"u}ller, P. }, title = { A Programming Logic for Sequential {J}ava }, booktitle = { Programming Languages and Systems ({ESOP}~'99) }, editor = { Swierstra, S. D. }, series = { Lecture Notes in Computer Science }, volume = 1576, pages = {162--176}, year = 1999, publisher = { Springer-Verlag }, } @InProceedings{JacobsEA99a, author = {Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.}, title = {Formal Techniques for {J}ava Programs}, booktitle = {Object-Oriented Technology. {ECOOP}'99 Workshop Reader}, year = 1999, editor = {Moreira, A. and Demeyer, D.}, series = {Lecture Notes in Computer Science}, volume = 1743, publisher = {Springer-Verlag}, note = {Available from \verb+www.informatik.fernuni-hagen.de/pi5/publications.html+} } @Proceedings{JacobsEA99, title = {Formal Techniques for {J}ava Programs}, year = 1999, editor = {Jacobs, B. and Leavens, G. T. and M{\"u}ller, P. and Poetzsch-Heffter, A.}, organization = {Technical Report~251, Fernuniversit{\"at} Hagen}, note = {Available from \verb+www.informatik.fernuni-hagen.de/pi5/publications.html+} } @InProceedings{YiCh99, author = "Kwangkeun Yi and Byeong-Mo Chang", title = "Exception Analysis for Java", pages = "", booktitle = {ECOOP'99 Workshop on Formal Techniques for Java Programs}, year = 1999, month = "June" } @TechReport{CORNELLCS//TR86-732, pages = "116", year = "1986", type = "Technical Report", number = "TR86-732", title = "Proving Temporal Properties of Concurrent Programs: {A} Non-Temporal Approach", bibdate = "October 14, 1993", author = "Bowen Alpern", abstract = "This thesis develops a new method for proving properties of concurrent programs and gives formal definitions for safety and liveness. A property is specified by a property recognizer - a finite-state machine that accepts the sequences of program states in the property it specifies. A property recognizer can be constructed for any temporal logic formula. (ABRIDGED ABSTRACT)", language = "English", institution = "Cornell University, Computer Science Department", month = feb, copyright = "Bowen Lewis Alpern 1986 - All Rights Reserved", } @Article{Metayer:1996:SOS, author = "Daniel Le M{\'e}tayer and David Schmidt", title = "Structural Operational Semantics as a Basis for Static Program Analysis", journal = "ACM Computing Surveys", volume = "28", number = "2", pages = "340--343", month = jun, year = "1996", coden = "CMSVAN", ISSN = "0360-0300", bibdate = "Thu Jun 26 16:49:57 MDT 1997", url = "http://www.acm.org/pubs/toc/Abstracts/surveys/234744.html; http://www.acm.org/pubs/citations/journals/surveys/1996-28-2/p340-le_metayer/", acknowledgement = ack-nhfb, } @TechReport{ercim.inria.publications//RR-3375, pages = "40 p.", type = "Technical Report", number = "RR-3375", institution = "Inria, Institut National de Recherche en Informatique et en Automatique", title = "Dynamic Slicing: a Generic Analysis Based on a Natural Semantics Format", bibdate = "March 1, 1998", author = "Valerie Gouranton and Daniel Le Metayer", language = "A", abstract = "Il existe un certain nombre d\'analyses d\'\élagage pour diff\érents langages de programmation. Au lieu de d\éfinir une nouvelle analyse pour chacun des langages, nous aimerions sp\écifier l\'analyse d\'\élagage ind\épendamment du langage consid\ér\é, puis l\'instancier \à plusieurs langages. Pour atteindre cet objectif, nous proposons un format de s\émantique naturelle qui formalise une classe de s\émantiques naturelles et nous d\éfinissons un format d\'analyse dynamique d\'\élagage qui est g\én\érique au sens o\ù il est ind\épendant du langage. Nous \établissons ensuite la correction de l\'analyse g\én\érique d\'\élagage sous forme de relation entre les arbres de d\érivation du programme initial et du \{\\em slice\} (le programme transform\é). L\'analyse g\én\érique d\'\élagage est alors instanci\ée \à plusieurs langages de programmation (un langage imp\ératif, un langage de programmation logique et un langage fonctionnel) en conformit\é avec le format de s\émantique. Nous obtenons par la suite un analyseur dynamique pour chacun de ces langages. Slicing analyses have been proposed for different programming languages. Rather than defining a new analysis from scratch for each programming language, we would like to specify such an analysis once for all, in a language-independent way, and then specialise it for different programming languages. In order to achieve this goal, we propose a notion of natural semantics format and a dynamic slicing analysis format. The natural semantics format formalises a class of natural semantics and the analysis format is a generic, language-independent, slicing analysis. The correctness of the generic analysis is established as a relation between the derivation trees of the original program and the slice. This generic analysis is then instantiated to several programming languages conforming the semantics format (an imperative language, a logic programming language and a functional language), yielding a dynamic slicing analyser for each of these languages.", } @InProceedings{PEPM::Metayer1995, title = "Proving Properties of Programs Defined over Recursive Data Structures", author = "Daniel Le M{\'e}tayer", pages = "88--99", booktitle = "Proceedings of the {ACM} {SIGPLAN} Symposium on Partial Evaluation and Semantics-Based Program Manipulation", address = "La Jolla, California", month = "21-23~" # jun, year = "1995", ISBN = "ISBN 0-89791-720-0", } @InProceedings{dean97:security, author = "D. Dean", title = "The Security of Static Typing with Dynamic Linking", booktitle = "Proceedings of the Fourth ACM Conference on Computer and Communications Security", year = "1997", address = "Zurich, Switzerland", month = apr, url = "http://www.CS.Princeton.EDU/sip/pub/ccs4.html", abstract = "Dynamic linking is a requirement for portable executable content. Executable content cannot know, ahead of time, where it is going to be executed, nor know the proper operating system interface. This imposes a requirement for dynamic linking. At the same time, we would like languages supporting executable content to be statically typable, for increased efficiency and security. Static typing and dynamic linking interact in a security-relevant way. This interaction is the subject of this paper. One solution is modeled in PVS, and formally proven to be safe.", } @inproceedings{DrosEisen971, author= {S. Drossopoulou and S. Eisenbach}, title="Is the {J}ava {T}ype {S}ystem {S}ound?", booktitle="4th Int. Workshop Foundations of Object-Oriented Languages", year=1997 } @inproceedings{DrosEisen972, author= {S. Drossopoulou and S. Eisenbach}, title="Java is {T}ype {S}afe - {P}robably", booktitle="ECOOP'97 ", publisher = "Springer Verlag", series = "LNCS 1241", pages = "389--418", month = jan , year = "1997", } @InCollection{DE98, author= {S. Drossopoulou and S. Eisenbach}, title="Towards an {O}perational {S}emantics and {P}roof of {T}ype {S}oundness for {J}ava", booktitle="Formal Syntax and Semantics of Java", publisher={Springer-Verlag}, editor = "J. Alves-Foss", volume = "1523", series={LNCS}, year=1998 } @Article{Drossopoulou:1999:DSJ, author = "S. Drossopoulou and S. Eisenbach", title = "Describing the Semantics of {Java} and Proving Type Soundness", journal = "Lecture Notes in Computer Science", volume = "1523", year = "1999", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Mon Sep 13 16:57:02 MDT 1999", acknowledgement = ack-nhfb, } @InProceedings{Nipk-CADE99*398, author = "T. Nipkow", title = "Invited Talk: Embedding Programming Languages in Theorem Provers", pages = "398", ISBN = "3-540-66222-7", editor = "Harald Ganzinger", booktitle = "Proceedings of the 16th International Conference on Automated Deduction ({CADE}-16)", month = jul # "~7--10,", series = "LNAI", volume = "1632", publisher = "Springer-Verlag", address = "Berlin", year = "1999", } @InCollection{OheNip98, author = "T. Nipkow and D. {von Oheimb}", title = "Machine-checking the {J}ava Specification: Proving Type-Safety", year = "1998", publisher = "SV", editor = "J. Alves-Foss", volume = "1523", pages = "119+37", abstract = "In this article we present Bali, the formalization of a large (hitherto sequential) sublanguage of Java. We give its abstract syntax, type system, well-formedness conditions, and an operational evaluation semantics. Based on these definitions, we can express soundness of the type system, an important design goal claimed to be reached by the designers of Java, and prove that Bali is indeed type-safe. All definitions and proofs have been done formally in the theorem prover Isabelle/HOL. Thus this article demonstrates that machine-checking the design of non-trivial programming languages has become a reality.", booktitle = "Formal Syntax and Semantics of {J}ava", series = "LNCS", url = "http://www.in.tum.de/~isabelle/bali/doc/Springer98.html", } @inproceedings{Nipkow98, author= {T. Nipkow and D. Von Oheimb}, title="Java {L}ight is {T}ype {S}afe - {D}efinitely", booktitle="25st ACM Symp. Principles of Programming Languages ", year = "1998", } @InProceedings{Jen98, author = {T.~Jensen and D.~{Le M\'etayer} and T.~Thorn}, title = {Security and {D}ynamic {C}lass {L}oading in {J}ava: a {F}ormal isation}, url = {ftp://ftp.irisa.fr/local/lande/tjdlmtt-iccl98.ps.gz}, booktitle = {Proceedings of the 1998 IEEE International Conference on Computer Languages}, year = {1998}, pages = {4--15}, published = {New York:\ IEEE Computer Society}, month = {May}, abstract = {We give a formal specification of the dynamic loading of classes in the Java Virtual Machine (JVM) and of the visibi lity of members of the loaded classes. This specification is obtain ed by identifying the part of the run-time state of the JVM that is relevant for dynamic loading and visibility and consists of a set of inference rules defining abstract operations for loading, linking and verification of classes. The formalisation of visibility includes an axiomatisation of the rules for members hip of a class under inheritance, and of accessibility of a member in the presence of accessibility modifiers such as \texttt{privat e} and \texttt{protected}. The contribution of the formalisation is twofold. First, it provides a clear and concise description of the loading process and the rules for member visibility compared t o the informal definitions of the Java language and the JVM. Sec ond, it is sufficiently simple to allow calculations of the effects of load operations in the JVM.} } @techreport{Syme97, title={Proving {J}ava {T}ype {S}oundness}, author={D. Syme}, institution={University of Cambridge Computer Laboratory}, type={Technical Report 427}, year={1997} } @Article{Syme:1999:PJT, author = "D. Syme", title = "Proving {Java} Type Soundness", journal = "Lecture Notes in Computer Science", volume = "1523", year = "1999", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Mon Sep 13 16:57:02 MDT 1999", acknowledgement = ack-nhfb, } @Article{Qian:1999:FSJ, author = "Z. Qian", title = "A Formal Specification of {Java[TM]} Virtual Machine Instructions for Objects, Methods and Subroutines", journal = "Lecture Notes in Computer Science", volume = "1523", year = "1999", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Mon Sep 13 16:57:02 MDT 1999", acknowledgement = ack-nhfb, } @inproceedings{Qian98, title={A {F}ormal {S}pecification of the {J}ava {V}irtual {M}achine {I}nstructions for {O}bjects, {M}ethods and {S}ubroutines}, author={Z. Qian}, booktitle="Formal Syntax and Semantics of Java", publisher={Springer-Verlag, LNCS 1523}, year={1998} } @Article{BS99, author = {E. B\"orger and W. Schulte}, title = {{I}nitialization {P}roblems for {J}ava}, journal = "Software--Concepts and Tools", volume = "20", number = "4", year = "1999", } @inproceedings{BS992, author= {E. B\"orger and W. Schulte}, title= {{M}odular {D}esign for the {J}ava {V}irtual {M}achine {A}rchitecture}, booktitle="Architecture Design and Validation Methods", publisher={Springer-Verlag}, year=1999 } @inproceedings{BS98, author= {E. B\"orger and W. Schulte}, title="A {P}rogrammer {F}riendly {M}odular {D}efinition of the {S}emantics of {J}ava", booktitle="Formal Syntax and Semantics of Java", publisher={Springer-Verlag, LNCS 1523}, year=1998 } @inproceedings{BS982, author= {E. B\"orger and W. Schulte}, title="Defining the {J}ava {V}irtual {M}achine as {P}latform for {P}rovably {C}orrect {J}ava {C}ompilation", booktitle="23rd International Symposium on Mathematical Foundations of Computer Science", publisher = "Springer-Verlag", series = "LNCS", note="to appear", year = "1998", } @inproceedings{DC94, author={M. Dwyer and L. A. Clarke}, title={{D}ata {F}low {A}nalysis for {V}erifying {P}roperties of {C}oncurrent {P}rograms}, pages = "62-75", booktitle={Proc, of the Second ACM SIGSOFT Symposium on Foundations of Software Engineering}, year=1994, month= "December", } @inproceedings{HCDSZ99, author={J. Hatcliff and J. C. Corbett and M. B. Dwyer and S. Sokolowski and H. Zheng}, title={{A} {F}ormal {S}tudy of {S}licing for {M}ulti-threaded {P}rograms with {J}{V}{M} {C}oncurrency {P}rimitives}, booktitle={Proc, of the Static Analysis Symposium}, year=1999, month="September", note="to appear", } @inproceedings{NAC99, author={G. Naumovich and S. Avrunin and L. A. Clarke}, title={{D}ata {F}low {A}nalysis for {C}hecking {P}roperties of {C}oncurrent {J}ava {P}rograms}, booktitle={Proc. of the International Conference on Software Engineering}, location={Los Angeles}, year=1999, month= "May", } @article{Spin, author= {G. J. Holzmann}, title="{T}he {S}pin {M}odel {C}hecker", pages="279-295", journal="IEEE Trans. on Software Engineering, Volume 23", year="1997", month="May", } @inproceedings{HP98, author={K. Havelund and T. Pressburger}, title={{M}odel {C}hecking {J}ava {P}rograms using {J}ava {P}ath{F}inder}, booktitle={International Journal on Software Tools for Technology Transfer (STTT)}, year=1998, note= "To appear", } @inproceedings{DIS98, author={C. Demartini and R. Iosif and R. Sisto}, title={{M}odeling and {V}alidation of {J}ava {M}ultithreaded {A}pplications using {S}pin}, booktitle={Proc. of the 4th SPIN Workshop, Paris, France}, location={Paris}, year=1998, month="November", } @inproceedings{DS98, author={C. Demartini and R. Sisto}, title={{S}tatic {A}nalysis of {J}ava {M}ultithreaded and {D}istributed {A}pplications}, booktitle={Proc. of the 1998 International Symposium on Software Engineering for Parallel and Distributed Systems}, location={Los Angeles}, year=1998, month="April", } @TechReport{Corbett98-1, author = "J. C. Corbett", title = "{U}sing {S}hape {A}nalysis to {R}educe {F}inite-{S}tate {M}odels of {C}oncurrent {J}ava {P}rograms", note = "submitted for publication", year = "1998", month = "October", } @inproceedings{Corbett98-2, author={J. C. Corbett}, title={{C}onstructing {C}ompact {M}odels of {C}oncurrent {J}ava {P}rograms}, pages ="1-10", booktitle={ACM SIGSOFT Proc. of the 1998 International Symposium On Software Testing and Analysis}, location={Los Angeles}, year=1998, } @inproceedings{LiuWalker, author={X. Liu and D. Walker}, title={Confluence of Processes and Systems of Objects}, booktitle={Proc. of Theory and Practice of Software Development (TAPSOFT'95) 6th International Joint Conference CAAP/FASE}, location={Aarhus, Denmark}, year=1995 } @incollection{Jones96, author = "S. Hodges and C. B. Jones", title = "Non-Interferance Properties of a Concurrent Object-Based Langu age: Proofs based on an Operational Semantics", booktitle = "Object Orientation with Parallelism and Persistance", editors = "B. Freitag and C. B. Jones and C. Lengauer and H.-J. Schek", publisher="Kluwer Academic Publishers", year = "1996", note="ISBN 0-7923-9770-3 " } @inproceedings{pdta98, author = "Attali, I. and Caromel, D. and Ehmety, S. O.", title = "{About the automatic continuations in the Eiffel// Model}", booktitle = "{Proc. of the 1998 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'98)}", address = "{Las Vegas, USA}", year = "1998", month = "July", } @incollection{Hermes98, author = "I. Attali and D. Caromel and S. O. Ehmety", title = "{Formal Properties of the Eiffel// Model}", booktitle = "{Object-Based Parallel and Distributed Computing}", publisher = "{Hermes, France}", year = "1999", note = "To appear", } @inproceedings{FMPPTA98, author= {I. Attali and D. Caromel and S. Lippi}, title="From a Specification to an Equivalence Proof in Object-Oriented Parallelism", booktitle= " FMPPTA'99: Modeling and Proving (Fourth Workshop in Formal Methods for Parallel Programming, Theory and Applications)", publisher="Springer, LNCS", volume="1586", year=1999 } @InProceedings{heintze95, author = "N. Heintze", title = "Control Flow Analysis and Type Systems", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", number = "983", series = "LNCS", pages = "189-206", booktitle = "Proceedings SAS'95, International Static Analysis Symposium", year = "1995", OPTorganization = "", publisher = "Springer Verlag", address = "Glasgow, Scotland", month = "September", OPTnote = "", OPTannote = "" } @PhdThesis{Shivers:phd:1991, author = "Olin Grigsby Shivers", title = "Control-Flow Analysis of Higher-Order Languages or Taming Lambda", school = "Carnige-Mellon Univeristy", month = may, year = "1991", url = "ftp://theory.doc.ic.ac.uk/theory/imported/ShiversO/diss.dvi.Z", url = "ftp://theory.doc.ic.ac.uk/theory/imported/ShiversO/diss.ps.Z", note = "Also available as CMU-CS-91-145", supervisor = "Peter Lee", checked = "19940320", source = "Dept. Library / URL", abstract = "Programs written in powerful, higher-order languages like Scheme, ML, and Common Lisp should run as fast as their FORTRAN and C counterparts. They should, but they don't. A major reason is the level of optimisation applied to these two classes of languages. Many FORTRAN and C copmilers employ an aresenal of sophisticated global optimisations that depend upon data-flow analysis: common-subexpression elimination, loop-invariant detection, induction-variable elimination, and many, many more. Compilers for higher-order languages do not provide these optimisations. Without them, Scheme, LISP and ML compilers are doomed to produce code that runs lsower than their FORTRAN and C counterparts. The problem is the lack of an explicit control-flow graph at compile time, something which traditional data-flow analysis techniques require. In this dissertation, I present a technique for recovering the control-flow graph of a Scheme program at compile time. I give examples of how this information can be used to perform several data-flow analysis optimisations, including copy propagation, induction-variable elimination, useless-variable elimination, and type recovery. The analysis is defined in terms of a non-standard semantic interpretation. The denotational semantics is carefully developed, and several theorems establishing the correctness of the semantics and the implementing algorithms are proven.", reffrom = "Rozas:acm:lfp:1992", reffrom = "MacLachlan:acm:lfp:1992", reffrom = "Sabry:Felleisen:acm:lfp:1992", reffrom = "Huelsbergen:Larus:acm:lfp:1992", reffrom = "Flanagan:Sabry:Duba:Felleisen:acm:pldi:1993", reffrom = "Wright:Cartwright:acm:lfp:1994", reffrom = "Sabry:Felleisen:acm:pldi:1994", } @Book{mujo81, author = "S.S. Muchnick and N.D. Jones", title = "Program Flow Analysis, Theory and Applications", publisher = "Prentice Hall", year = "1981", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", OPTaddress = "", OPTedition = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @InProceedings{CC77, author = "P. Cousot and R. Cousot", title = "Abstract interpretation: a unified lattice model for static analysis of programs", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", OPTnumber = "", OPTseries = "", pages = "238-252", booktitle = "Proceedings of the 4th ACM Symposium on Principles of Programming Languages", year = "1977", OPTorganization = "", publisher = "ACM press", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Article{dlm97a, author = "D. Le M\'etayer", title = "Program analysis for software engineering: new applications, new requirements, new tools", OPTcrossref = "", OPTkey = "", journal = "ACM Sigplan Notices", year = "1997", volume = "32:1", OPTnumber = "", pages = "86-88", month = "January", OPTnote = "Pr\'econise l'usage d'analyseur statique pour le g\'enie logiciel. Il expose divers caract\'eristiques qui sont n\'ecessaires pour arriver \`a une utilisation pratique des techniques d'analyse statiques dans ce domaine. En particulier le probl\`eme de rendre compr\'ehensible les r\'esultats d'une analyse.\\ A mon avis le probl\`eme se pose aussi dans l'autre sens : quel est le sens des divers actions de l'utilisateur pour d\'esigner le but de l'analyse. Un autre probl\`eme est le temps de r\'eponse de l'analyse dans le cadre d'une utilisation interactive et le grain de pr\'ecision de la r\'eponse. L'incr\'ementalit\'e peut \^etre une bonne r\'eponse \`a \c{c}a.", OPTannote = "" } @inproceedings{Nipkow-Oheimb-POPL98, author = {Tobias Nipkow and David von Oheimb}, title = {Java$_{\ell{}ight}$ is Type-Safe --- Definitely}, booktitle = {Proc. 25th ACM Symp. Principles of Programming Languages}, year = {1998}, publisher = {ACM Press, New York}, editor = {}, url = {http://www4.informatik.tu-muenchen.de/~isabelle/bali/papers/POPL98.html}, abstract = {Java_light is a large sequential sublanguage of Java. We formalize its abstract syntax, type system, well-formedness conditions, and an operational evaluation semantics. Based on this formalization, we can express and prove type soundness. All definitions and proofs have been done formally in the theorem prover Isabelle/HOL. Thus this paper demonstrates that machine-checking the design of non-trivial programming languages has become a reality.}, CRClassification = {}, CRGenTerms = {}, pages={p. 161--170} } @InProceedings{pfdlm97, author = {P. Fradet and D. Le M\'etayer}, title = "Shape types ", booktitle = "Proc. of Principles of Programming Languages ", year = 1997, url = "ftp://ftp.irisa.fr/local/lande/pfdlm-popl97.ps.gz ", keywords = "Pointer structures and manipulations, graph grammars, type checking, program robustness, C. ", abstract = "Type systems currently available for imperative languages are too weak to detect a significant class of programming errors. For example, they cannot express the property that a list is doubly-linked or circular. We propose a solution to this problem based on a notion of {\em shape types} defined as context-free graph grammars. We define graphs in set-theoretic terms, and graph modifications as multiset rewrite rules. These rules can be checked statically to ensure that they preserve the structure of the graph specified by the grammar. We provide a syntax for a smooth integration of shape types in C. The programmer can still express pointer manipulations with the expected constant time execution and benefits from the additional guarantee that the property specified by the shape type is an invariant of the program. " , publisher = "ACM Press ", address = "Paris, France ", month = "Jan. ", OPTnote = "Ils d\'ecrivent une utilisation d'une forme de grammaire de graphe pour d\'ecrire les structures de donn\'ees r\'ecursives. Ils d\'ecrivent une application de type <>. Mais parlent d'une application possible au probl\`eme d'analyse de forme. En particulier pour les langages orient\'es-objets.Je pense que ce sera le point de d\'epart pour moi pour construire une analyse de forme." } @INPROCEEDINGS{Gouranton:98:DerivingSAS, AUTHOR = {V. Gouranton}, ADDRESS = {Pise, Italie}, BOOKTITLE = {International Static Analysis Symposium, SAS'98}, MONTH = {September}, PUBLISHER = {Springer-Verlag}, SERIES = {Lecture Notes in Computer Science}, TITLE = {Deriving analysers by folding/unfolding of natural semantics and a case study: slicing}, YEAR = {1998}, URL = {ftp://ftp.irisa.fr/local/lande/vg-sas98.ps.gz}, KEYWORDS = {systematic derivation, program transformation, natural semantics, proof tree, slicing analysis, logic programming language.}, ABSTRACT = {We consider specifications of analysers expressed as compositions of two functions: a semantic function, which returns a natural semantics derivation tree, and a property defined by recurrence on derivation trees. A recursive definition of a dynamic analyser can be obtained by fold/unfold program transformation combined with deforestation. A static analyser can then be derived by abstract interpretation of the dynamic analyser. We apply our framework to the derivation of a dynamic backward slicing analysis for a logic programming language.} } @InProceedings{ vgdlm97, author = "V. Gouranton and D. {Le M\'etayer} ", url = "ftp://ftp.irisa.fr/local/lande/vgdlm-ISySe97.ps.gz ", address = "Herzliya, Israel ", booktitle = "The 8th Israel Conference on Computer Systems and Sofware Engineering, IEEE, IFCC, ISySe'97 ", month = "june", title = "Formal development of static program analysers ", year = "1997 ", keywords = "functional languages, natural semantics, neededness analysis, paths analysis, program transformation, optimising compilers ", abstract = "We propose an approach for the formal development of static analysers which is based on transformations of inference systems. The specification of an analyser is made of two components: an operational semantics of the programming language and the definition of a property by recurrence on the proof trees of the operational semantics. The derivation is a succession of specialisations of inference systems with respect to properties on their proof trees. In this paper, we illustrate the methodology with the derivation of analysers for a non strict functional language. ", OPTnote = "Ils ne prennent en compte que les arbres de preuves finis et sont donc limites dans le nombre de cas qu'ils peuvent manipuler. Ils le disent et renvoient \`a~\cite{CC92} pour la prise en compte des aspects infinis de calculs. Ca suppose l'usage des techniques d'induction n\'egative ce qui est relativement compliqu\'e." } @InProceedings{Almeida97, author = {P. S. Almeida}, title = {Balloon Types:~Controlling Sharing of States in Data Types}, booktitle = {Proceedings of the European Conference on Object-Oriented Programming (ECOOP)}, OPTcrossref = {}, OPTkey = {}, pages = {32-59}, year = {1997}, OPTeditor = {}, OPTvolume = {}, number = {1241}, series = {LNCS}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, publisher = {Springer Verlag}, OPTnote = {}, OPTannote = {} } @InProceedings{Schmidt96, author = {D. A. Schmidt}, title = {Abstract Interpretation of Small-Step Semantics}, booktitle = {Proc. 5th LOMAPS Workshop on Analysis and Verification of Multiple-Agent Languages}, OPTcrossref = {}, OPTkey = {}, pages = {76-99}, year = {1996}, editor = {Springer Verlag}, OPTvolume = {}, number = {1192}, series = {LNCS}, OPTaddress = {}, month = {June}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {} } @InProceedings{Schmidt95, author = "D. A. Schmidt", title = "Natural-semantics-based abstract interpretation", OPTcrossref = "", OPTkey = "", editor = "A. Mycroft", OPTvolume = "", number = "983", series = "LNCS", pages = "1-18", booktitle = "Static Analysis Symposium", year = "1995", OPTorganization = "", publisher = "Springer Verlag", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "" } @Misc{NJ94, OPTcrossref = "", OPTkey = "", author = "Neil D. Jones and Flemming Nielson", title = "Abstract Interpretation: a Semantics-Based Tool for Program Analysis", howpublished = "Courses Notes", year = "1994", month = "June", OPTnote = "Downloaded from http://www.cs.uchicago.edu/~sagiv/courses/D-58.dvi. Presents a rather basic approach. To be used onl y as introductory material. It's aim is to provide an 'in breath first' view of the topic. In particular, nothing is s aid about {\em computational orderings} and the use of widenning-narrowing operators.", OPTannote = "" } @InProceedings{Plev93, author = "J. Plevyak and A. Chien and V. Karamcheti", title = "Analysis of Dynamic Structures for Parallel Execution", OPTcrossref = "", OPTkey = "", OPTeditor = "", OPTvolume = "", number = "768", series = "Lecture Notes In Computer Science", pages = "37-56", booktitle = "Proceedings of the 6th International Workshop on Languages and Compilers for Parallel Computing", year = "1993", OPTorganization = "", publisher = "Springer Verlag", OPTaddress = "", month = "1993", OPTnote = "", OPTannote = "" } %============ Mathematiques @article{GTW77, author= {J.A. Goguen and J.W. Thatcher and E.G. Wagner and J.B. Wright}, title="{I}nitial {A}lgebra {S}emantics and {C}ontinuous {A}lgebra", journal="JACM, N. 24", year=1977 } @article{Sco76, author= {D. S. Scott}, title="{D}ata {T}ypes as {L}attices", journal="SIAM Journal of computing, Vol. N. 3", year=1976 } @article{Gro90, author= {M. Gro$\beta$e-Rhode}, title="{T}owards {O}bject-{O}riented {A}lgebraic {S}pecification", journal="Recent Trends in Data Type Specification, LNCS N. 534, pages 98-116", year=1990 } @article{EPP87, author= {H. Ehring and F. Parisi-Presicce and P. Boehm}, title="{A}lgebraic {D}ata {T}ype and {P}rocess {S}pecification", journal="Recent Trends in Data Type Specification, LNCS N. 332, pages 23-43", year=1987 } %=========== Grammmaires Attribuees @book{Jou84, author= {M. Jourdan}, title="{L}es {G}rammaires {A}ttribu\'ees: {I}mpl\'ementation, {A}pplications, {O}ptimisations", publisher="Th\`ese de 3i\`eme Cycle, Universit\'e Paris VII, publication du LITP", address={2 place Jussieu 75221 Paris CEDEX 05}, year=1968 } %============ Processus de Communication @book{Mil80, author= {R. Milner}, title="{A} {C}alculus of {C}ommunicating {S}ystems", publisher = "Springer Verlag, LNCS 92", year=1980 } @book{JL92, author= {R. Janicki and Peter E. Lauer}, title="{S}pecifcation and {A}nalysis of {C}oncurrent {S}ystems: the {C}{O}{S}{Y} {A}pproach", publisher="Springer-Verlag", address="", year=1992 } @book{Hoa85, author= {C.A.R Hoare}, title="{C}ommunicating {S}equential {P}rocesses", publisher="Prentice Hall", year=1985 } @article{AB84, author= {D. Austry and G. Boudol}, title="{A}lg\`ebres de {P}rocessus et {S}ynchronisation", journal="TCS, 30(1):91-131", year=1984 } @article{Bou85, author= {G. Boudol}, title="{C}alculs de {P}rocessus et {V}\'erification", journal="Rapport de Recherche INRIA, N. 424", year=1985 } @book{MPW89a, author= {R. Milner and J. Parrow and D.J. Walker}, title="{A} {C}alculus of {M}obile {P}rocesses", publisher="Academic Press", year=1989 } @article{MPW89b, author= {R. Milner and J. Parrow and and D.J. Walker}, title="{A} {C}alculus of {M}obile {P}rocesses", journal="Part ii, Academic press, Inc. pages 41-77", year=1989 } @article{Ehr90, author= {H.-D. Ehrich}, title="{A} {C}ategorial {T}heory of {O}bjects as {O}bserved {P}rocesses", journal="Foundations of {O}bject-{O}riented {L}anguages, LNCS N. 489, pages 203-228", year=1990 } @InProceedings{Papa92b, author = "M. Papathomas", title = "A Unifying Framework for Process Calculus Semantics of Concurrent Object-Oriented Languages", booktitle = "Proc. of the ECOOP '91 Workshop on Object-Based Concurrent Computing", series = "LNCS 612", pages = "53--79", year = "1992", keywords = "olit-obc pcalc osg obc91", } %========== Acteurs @book{Agha86, author= {G. Agha}, title="Actors: A model of Concurrent Computation in Distributed Systems", publisher="MIT Press, Cambridge", year=1986 } @article{AMS92, author= {G. Agha and I. A. Mason and S. Smith and C. Talcott}, title="{T}owards a {T}heory of {A}ctor {C}omputation", journal="CONCUR'92, pages 565-580, Stony Brook, NY, USA, August", year=1992 } @TechReport{Agha93a, author = "G. Agha and I. Mason and S. Smith and C. Talcott", title = "A Foundation for Actor Computation", institution = "UIUC", type = "technical report", note= {To appear in Journal of Functional Programming}, year = {1995} , keywords = "olit-obc actors semantics binder", url = "ftp://sail.stanford.edu/pub/MT/95actors.ps.Z", abstract = "We present an actor language which is an extension of a simple functional language, and provide a precise operational semantics for this extension. Actor configurations are open distributed systems, meaning we explicitly take into account the interface with external components in the specification of an actor system. We define and study various notions of equivalence on actor expressions and configurations." } @article{MAS93, author= {S. Miriyala and G. Agha and Y. Sami}, title="Visualizing Actor Programs using Predicate Transition Nets", journal="Journal of Visual Languages and Computing, 3 (2)", year=1992 } @article{AAJCIS, author= {G. Agha and M. Astley}, title="A visualization Model for Concurrent Systems", journal="International Journal of Information Science, Elsevier", year=1996, note={To appear} } @inproceedings{Salle96, author= {J-L. Cola\c{c}o, M. Pantel, P. Sall\'e, A. Senteni}, title={Un Calcul d'Acteurs Primitifs ({\sc Cap})}, booktitle = {Proc. of JFLA'96 Conference}, address={Qu\'ebec}, year=1996 } @TechReport{Clin81a, author = "W. D. Clinger", title = "Foundations of Actor Semantics", institution = "MIT Artificial Intelligence Laboratory", number = "AI-TR-633", month = may, year = "1981", keywords = "concurrency actors", } @InProceedings{Vasc92a, author = "V. Vasconcelos and M. Tokoro", title = "Traces Semantics for Actor Systems", booktitle = "Proc. of the ECOOP '91 Workshop on Object-Based Concurrent Computing", series = "LNCS 612", pages = "141--162", year = "1992", keywords = "olit-obc obc91", } %========== Automates et reseaux de Petri @article{Tau89, author= {D. Taubner}, title="{F}inite {R}epresentations of {C}{C}{S} and {T}{C}{S}{P} {P}rograms by {A}utomata and {P}etri {N}ets", journal="LNCS, Springer-Verlag, Berlin Heidelberg", year=1989 } %========= Graphes @misc{graph, author= {A. Le Hors}, title={Graph: A Directed Graph Displaying Server, {GIPE} 2 {E}SPRIT project, 4th Review Report, Workpackage 4}, year=1992 } @InProceedings{Gang93a, author = "D. Gangopadhyay and S. Mitra", title = "ObjChart: Tangible Specification of Reactive Object Behavior", booktitle = "Proc. ECOOP '93", series = "LNCS 707", pages = "432--457", address = "Kaiserslautern, Germany", month = jul, year = "1993", keywords = "olit ecoop93", abstract = "ObjChart is a new visual formalism to specify objects and their reactive behavior. A system is specified as a collection of asynchronously communicating objects arranged in a part-of hierarchy, where the reactive behavior of each object is described by a finite state machine. Value propagation is effected using functional invariants over attributes of objects. A compositional semantics for concurrent object behavior is sketched using the equational framework of Misra. In contrast to other Object Oriented modeling notations, ObjChart uses object decomposition as the single refinement paradigm, maintains orthogonality between control flow and value propagation, introduces Sequence object which embodies structural induction, and allows tracing causality chains in time linear in the size of the system. ObjChart's minimality of notations and precise semantics make ObjChart models of systems coherent and executable.", } %========== Visualisation @article{RC93, author= {G.-C. Roman and K. C. Cox}, title="{A} {T}axonomy of {P}rogram {V}isualization {S}ystems", journal="IEEE Computer", year=1993 } @article{Pavane, author= {G.C. Roman and et al}, title="{A} {S}ystem for {D}eclarative {V}isualization of {C}oncurrent {C}omputations", journal="Journal of Visual Languages and Computing, 3 (2)", year=1992 } @article{Polka, author= {J. T. Stasko and E. Kraemer}, title={A Methodology for building application-specific visualizations of parallel programs}, journal="Journal of Parallel and Distributed Computing, 18", year=1993 } @article{overview, author= {E. Kraemer and J. T. Stasko}, title={The visualization of parallel systems: an overview}, journal="Journal of Parallel and Distributed Computing, 18", year=1993 } %========== Environnement de programmation @inproceedings{ToonTalk, author= {K. Kahn}, title={ToonTalk - an animated Programming Environment for children}, booktitle = {Proc. of the National Educational Computing Conference}, address = {Baltimore, MD}, year=1995 } @inproceedings{Zeus, author= {M. H. Brown}, title={Zeus: a system for algorithm animation and multiview editing}, booktitle = {Proc. of the IEEE Workshop on Visual Languages}, year=1991 } %========= Objets actifs @InProceedings{Nier87c, author = "O. Nierstrasz", title = "Active Objects in Hybrid", booktitle = "Proc. OOPSLA '87, ACM SIGPLAN Notices 22 (12)", pages = "243--253", year = "1987", keywords = "olit-obcl hybrid triggers osg-ftp oopsla87 oobib(obcp)", url = "ftp://iamftp.unibe.ch/pub/scg/Papers/activeObjectsInHybrid.ps.gz", abstract = "Most object-oriented languages are strong on reusability or on strong-typing, but weak on concurrency. In response to this gap, we are developing Hybrid, an object-oriented language in which objects are the active entities. Objects in Hybrid are organized into domains, and concurrent executions into activities. All object communications are based on remote procedure-calls. Unstructured sends and accepts are forbidden. To this the mechanisms of delegation and delay queues are added to enable switching and triggering of activities. Concurrent subactivities and atomic actions are provided for compactness and simplicity. We show how solutions to many important concurrent problems, such a pipelining, constraint management and ``administration'' can be compactly expressed using these mechanisms." } @InProceedings{Nier91d, author = "O. Nierstrasz and M. Papathomas", title = "Towards a Type Theory for Active Objects", booktitle = "ACM OOPS Messenger, 2 (2), Proc. OOPSLA/ECOOP 90 Workshop on Object-Based Concurrent Systems", pages = "89--93", month = apr, year = "1991", keywords = "olit-obc pcalc equivalence semantics abacus osg-ftp om90 obc90", url = "ftp://iamftp.unibe.ch/pub/scg/Papers/towardsATypeTheory.ps.gz", abstract = "Currently popular notions of types, such as signature compatibility, fail to express essential properties of concurrent active objects that are necessary for their correct use in new contexts. We propose and explore a new notion of compatibility called interaction conformance defined in terms of the possible interactions between an object and its clients. We relate interaction conformance to known equivalence relations between communicating concurrent agents, and we show that, by viewing types as certain kinds of indeterminate agents, interaction conformance gives us a subtype relationship. We briefly explore the potential for applying these ideas to concurrent object-oriented languages." } %% ISBN: 3 540 55613 3 %% CONFERENCE @InProceedings{Nier92a, author = "O. Nierstrasz", title = "Towards an Object Calculus", booktitle = "Proc. of the ECOOP '91 Workshop on Object-Based Concurrent Computing", series = "LNCS 612", pages = "1--20", publisher = "Springer-Verlag", year = "1992", keywords = "pcalc-obc mobility oc obc91 of92 osg-ftp-book", url = "ftp://iamftp.unibe.ch/pub/scg/Papers/towardsAnObjectCalculus.ps.gz", abstract = "The development of concurrent object-based programming languages has suffered from the lack of any generally accepted formal foundations for defining their semantics. Furthermore, the delicate relationship between object-oriented features supporting reuse and operational features concerning interaction and state change is poorly understood in a concurrent setting. To address this problem, we propose the development of an object calculus, borrowing heavily from relevant work in the area of process calculi. To this end, we briefly review some of this work, we pose some informal requirements for an object calculus, and we present the syntax, operational semantics and use through examples of a proposed object calculus, called OC.", } @InProceedings{Nier93d, author = "O. Nierstrasz", title = "Regular Types for Active Objects", booktitle = "Proc. OOPSLA '93, ACM SIGPLAN Notices, 28 (10)", pages = "1--15", month = oct, year = "1993", keywords = "olit-obc pcalc equivalence types osg-ftp oopsla93 vo93 rtao", url = "ftp://iamftp.unibe.ch/pub/scg/Papers/regularTypes.ps.gz", abstract = "Previous work on type-theoretic foundations for object-oriented programming languages has mostly focussed on applying or extending functional type theory to functional {"}objects.{"} This approach, while benefitting from a vast body of existing literature, has the disadvantage of dealing with state change either in a roundabout way or not at all, and completely side-stepping issues of concurrency. In particular, dynamic issues of non-uniform service availability and conformance to protocols are not addressed by functional types. We propose a new type framework that characterizes objects as regular (finite state) processes that provide guarantees of service along public channels. We also propose an original notion of subtyping for regular types that extends Wegner and Zdonik's {"}principle of substitutability{"} to non-uniform service availability, and we relate it to known process equivalences. Finally, we formalize what it means to {"}satisfy a client's expectations,{"} and we show how regular types can be used to tell when sequential or concurrent clients are satisfied. [NB: a revised version is available by ftp.]", } @Article{Fugi92a, author = "M. Fugini and O. Nierstrasz and B. Pernici", title = "Application Development Through Reuse: The {ITHACA} Tools Environment", journal = "SIGOIS Bulletin", volume = "13", number = "2", pages = "38--47", month = aug, year = "1992", keywords = "olit-ithaca recast vista oke osg-ftp oc91 ithaca-final", url = "ftp://iamftp.unibe.ch/pub/scg/Papers/appDevThroughReuse.ps.gz", abstract = "This paper presents the architecture and basic features of the Ithaca Application Development Environment based on a Software Information System for enhancing reusability of both software components and artifacts about development of these components. Object-oriented techniques are used in the Environment at all levels of the development of an application: requirement specification, scripting, implementation through class refinement and tailoring. In the Environment, it is tracked how the various products of the development phases were produced by providing tools for the Application Engineer who is responsible for abstracting application skeletons and development information and storing these as Application Frames into a Software Information Base. In particular, the paper describes the Requirement Collection And Specification Tool (RECAST) and the Visual Scripting Tool (Vista) of the Ithaca Development Environment.", } @Book{NCY95, editor = "O. Nierstrasz and P. Ciancarini and A. Yonezawa", title = "Rule-based Object Coordination", booktitle = "Object-Based Models and Languages for Concurrent Systems", publisher = "Springer-Verlag", series = "LNCS 924", year = "1995" } @InProceedings{AIKMO89, author = "I. Ichikawa and S. Aikawa and M. Kamiko and E. Ono and T. Mori", title = "Program Design Visualization Systems for Object-Oriented Programs", booktitle = "Proc. of the ACM SIGPLAN Workshop on Object-Based Concurrent Programming, ACM SIGPLAN Notices 24 (4)", pages = "181--183", month = "[4]", year = "1989", keywords = "Object-Oriented Languages Parallel Programming", abstract = "Describes a program design visualization system which provides animation using figures at a functional specification level helpful in checking the consistency between design and program behavior.", } @InProceedings{Masu92a, author = "Hidehiko Masuhara and Satoshi Matsuoka and Takuo Watanabe and Akinori Yonezawa", title = "Object-Oriented Concurrent Reflective Languages can be Implemented Efficiently", booktitle = "Proc. OOPSLA '92, ACM SIGPLAN Notices", pages = "127--144", month = oct, year = "1992", keywords = "olit-obc abcl oopsla92 binder", url = "ftp://camille.is.s.u-tokyo.ac.jp/pub/papers/oopsla92-abclr2.ps.gz", note = "Published as Proc. OOPSLA '92, ACM SIGPLAN Notices, volume 27, number 10", } @InProceedings{Wata88a, author = "T. Watanabe and A. Yonezawa", title = "Reflection in an Object-Oriented Concurrent Language", booktitle = "Proc. OOPSLA '88, ACM SIGPLAN Notices 23 (11)", pages = "306--315", month = nov, year = "1988", keywords = "olit-obcl abclr oopsla88", } @InProceedings{Mats91a, author = "Satoshi Matsuoka and Takuo Watanabe and Akinori Yonezawa", editor = "P. America", title = "Hybrid Group Reflective Architecture for Object-Oriented Concurrent Reflective Programming", booktitle = "Proc. ECOOP '91", series = "LNCS 512", pages = "231--250", address = "Geneva, Switzerland", month = jul # " 15-19", year = "1991", keywords = "olit-obc ecoop91", url = "ftp://camille.is.s.u-tokyo.ac.jp/pub/papers/ecoop91-abclr2.ps.gz", } @InProceedings{Benn87a, author = "J. K. Bennett", title = "The Design and Implementation of {D}istributed {S}malltalk", booktitle = "Proc. OOPSLA '87, ACM SIGPLAN Notices 22 (12)", pages = "318--330", month = dec, year = "1987", keywords = "olit-oopl oopsla87" } @InProceedings{Yoko86a, author = "Y. Yokote and M. Tokoro", title = "The Design and Implementation of {C}oncurrent {S}malltalk", booktitle = "Proc. OOPSLA '86, ACM SIGPLAN Notices, 21 (11)", pages = "331--340", month = nov, year = "1986", keywords = "olit-obcl concurrentsmalltalk oopsla86", } %%%%%%%%%%%%%%%%%% % denis %%%%%%%%%%%%%%%%%% @Article{Balter94, author = "R. Balter and S. Lacourte and M. Riveill", title = "The {G}uide language.", journal = "Computer Journal", volume = "37", number = "6", pages = "519--530", year = "1994", } @InProceedings{Brue93a, author = "B. Bruegge and T. Gottschalk and B. Luo", title = "A Framework for Dynamic Program Analyzers", booktitle = "Proc. OOPSLA '93, ACM SIGPLAN Notices 28 (10)", pages = "65--82", month = oct, year = "1993", } @InProceedings{Consens-icse92, author = "M. Consens and A. Mendelzon and A. Ryman", title = "Visualizing and Querying Software Structures", booktitle = "Proc. of the ~$14^{th}$~ International Conference on Software Engineering", pages = "138--156", month = may, year = "1992", } @InProceedings{icse97, author = "D. F. Jerding and J. T. Stasko and T.Ball", title = "Visualizing Interactions in Program Executions", booktitle = "Proc. of the ~$17^{th}$~ International Conference on Software Engineering", pages = "360--370", month = may, year = "1997", } @InProceedings{Consens95, author = "M. P. Consens and A. O. Mendelzon", title = "Hy+: A Hygraph-based Query and Visualization System", booktitle = "Proc. of the ACM SIGMOD International Conference on Management of Data", series = "SIGMOD Record, 22(2)", pages = "511-516", year = "1993", } @Article{Grass92, author = "J. E. Grass", title = "Object-Oriented Design Archaeology with {CIA++}", journal = "Computing Systems", year = "1992", volume = "5", number = "1", pages = "5--67", } @Book{Paepcke93, key = "Paepcke", author = "A. Paepcke", title = "Object-Oriented Programming: The {CLOS} Perspective", publisher = "The MIT Press", year = "1993", OPTeditor = "Andreas Paepcke", annote = "An edited collection of articles.", } @InProceedings{Laffra94, author = "C. Laffra and A. Malhotra", title = "HotWire -- {A} Visual Debugger for {C}++", booktitle = "USENIX Sixth C++ Technical Conference", location = "IBM T.J. Watson Labs", pages = "109--122", publisher = "USENIX", address = "Cambridge, MA", month = apr # " 11-14", year = "1994", } @InProceedings{LanNak95, author = "D. B. Lange and Y. Nakamura", title = "Interactive Visualization of Design Patterns Can Help in Framework Understanding", booktitle = "Proc. OOPSLA '95, ACM SIGPLAN Notices 30 (10)", pages = "342-357", month = oct, year = 1995, } @Book{MilCC, author = "R. Milner", title = "Communication and Concurrency", publisher = "Prentice Hall", year = "1989", } @InProceedings{Pauw94a, author = "W. De Pauw and D. Kimelman and J. Vlissides", title = "Modeling Object-Oriented Program Execution", booktitle = "Proc. ECOOP '94", series = "LNCS 821", pages = "163--182", publisher = "Springer-Verlag", address = "Bologna, Italy", month = jul, year = "1994", keywords = "olit ecoop94", } @InProceedings{Robertson94, author = "S. P. Robertson and J. M. Carroll and R. L. Mack and M. B. Rosson and S. R. Alpert and J. Koenemann-Belliveau", title = "{ODE}: {A} Self-Guided, Scenario-Based Learning Environment for Object-Oriented Design Principles", pages = "51--64", booktitle = "Proc. OOPSLA '94, ACM SIGPLAN Notices", month = oct, year = "1994", } @InProceedings{Tokoro92, author = "I. Satoh and M. Tokoro", title = "A Formalism for Real-Time Concurrent Object-Oriented Computing", booktitle = "Proc. OOPSLA '92, ACM SIGPLAN Notices, 27 (10)", pages = "315--326", month = oct, year = "1992", } @InProceedings{Vion94, author = "J.-Y. Vion-Dury and M. Santana", title = "Virtual Images: Interactive Visualization of Distributed Object-Oriented Systems", pages = "65--84", booktitle = "Proc. OOPSLA '94, ACM SIGPLAN Notices 29 (10)", month = oct, year = "1994" } @InProceedings{Kobayashi:ILPS93, author = "Naoki Kobayashi and Akinori Yonezawa", booktitle = "Logic Programming - Proc. of the 1993 International Symposium", title = "{ACL} - {A} Concurrent Linear Logic Programming Paradigm", remark = "Refereed Papers", pages = "279--294", year = "1993", editor = "Dale Miller", publisher = "The MIT Press", address = "Vancouver, Canada", ISBN = "0-262-63152-0", } @InProceedings{Kobayashi:Yonezawa:acm:oopsla:1994, author = "Naoki Kobayashi and Akinori Yonezawa", title = "Type-Theoretic Foundations for Concurrent Object-Oriented Programs", pages = "31--45", booktitle = "Ninth Annual Conference on Object-Oriented Programming Systems, Languages, and Applications", month = oct, year = "1994", note = "Also available as SIGPLAN Notices 29(10) Oct 1994.", checked = "19950124", source = "Dept. Library", } @InProceedings{KobNakYon95SAS, author = "Naoki Kobayashi and Motoki Nakade and Akinori Yonezawa", title = "Static Analysis of Communication for Asynchronous Concurrent Programming Languages", volume = "983", series = "Lecture Notes in Computer Science", pages = "225--242", booktitle ="Second International Static Analysis Symposium (SAS'95)", year = "1995", publisher = "Springer-Verlag", } @book{Java, author= "J. Gosling and B. Joy and G. Steele", title = "The Java Language Specification", publisher = "Addison-Wesley", year = "1996", } @InCollection{Cian95a, author = "P. Ciancarini and K. K. Jensen and D. Yankelevich", title = "On the Operational Semantics of a Coordination Language", booktitle = "Proc. Object-Based Models and Languages for Concurrent Systems", publisher = "Springer-Verlag", series = "LNCS 924", pages = "77--106", year = "1995", keywords = "olit OBM94-06", abstract = "Linda is a coordination language, because it has to be combined with a sequential language to give a full parallel programming formalism. Although Linda has been implemented on a variety of architectures, and in combination with several sequential languages, its formal semantics is relatively unexplored. In this paper we study and compare a number of operational semantics specifications for Linda: Plotkin's SOS, Milner's CCS, Petri Nets, and Berry and Boudol's Chemical Abstract Machine. We analyze these specifications, and show how they enlighten different abstract implementations.", } @article{Hewitt77, author= {C. Hewitt}, title="Viewing control structures as patterns of passing messages", journal="Journal of Artificial Intelligence, 8 (3)", year=1977 } @book{Prog89a, editor = "P. Wegner and G. Agha and A. Yonezawa", title = "Workshop on Object-Based Concurrent Programming", publisher= "ACM SIGPLAN Notices 24 (4)", address = "San Diego", month = apr, year = "1989", keywords = "olit-obc obcp89 oobib(obcp)", } @inproceedings{abacus, author = "O. Nierstrasz", title = "A Guide to Specifying Concurrent Behaviour with Abacus", booktitle = "Object Management", pages = "267--293", address = "Centre Universitaire d'Informatique, University of Geneva", month = jul, year = "1990", keywords = "abacus90", } @TechReport{Nier91c, author = "O. Nierstrasz", editor = "D. Tsichritzis", title = "The Next 700 Concurrent Object-Oriented Languages -- Reflections on the Future of Object-Based Concurrency", institution = "Centre Universitaire d'Informatique, University of Geneva", type = "Object Composition", pages = "165--187", month = jun, year = "1991", keywords = "olit-obc hybrid abacus scol osg oc91", abstract = "There has been a flurry of activity in recent years to extend existing languages with object-oriented features, and to extend object-oriented concepts and languages with seemingly orthogonal features, such as obc and persistence, to improve their expressive power and potential as a solution to the {"}software crisis{"}. In many cases these integration efforts have uncovered various forms of semantic interference between features. We claim that the majority of these difficulties are concerned with the very aspect of object-orientation that we seek most urgently to exploit, namely software compositionality. We shall review the problems of integrating obc and object-oriented features from this viewpoint and discuss some of the more important requirements to be met. Finally, we propose a view of objects as patterns of communicating agents that suggests the development of a class of concurrent object-oriented languages parameterized by patterns that address the needs of particular application domains.", }