$Id: bib1300.bib 2001/02/01 denker $ DAML annotation of ca. 1300 bibliography entries "D. Basin" "M. Clavel" "J. Meseguer" "Rewriting Logic as a Metalogical Framework" "url{http://www.informatik.uni-freiburg.de/{homedir}basin/pubs/pubs.html}" "D. Basin" "G. Denker" "Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis" "May 2000" "Sumitted for publication" "Klaus Havelud" "Grigore Roc{s}u" "Testing linear temporal logic formulas on finite execution traces" "NASA Ames Research Center" "" "2000" "Peter Csaba {\"O}lveczky" "Jos'e Meseguer" "Specification of real-time and hybrid systems in rewriting logic" "2000" "To appear in {em Theoretical Computer Science}, url{maude.csl.sri.com}" "Francisco Dur'an" "Jos'e Meseguer" "On Parameterized Theories and Views in {Full Maude} 2.0" "Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications" "K. Futatsugi" "2000" "{ENTCS}, Elsevier" "D. Basin" "M. Clavel" "J. Meseguer" "Rewriting Logic as a Metalogical Framework" "FST TCS 2000" "S. Kapoor" "S. Prasad" "2000" "55-80" "Springer LNCS" "Peter Csaba {\"O}lveczky" "Jos'e Meseguer" "{Real-Time} {Maude}: a tool for simulating and analyzing real-time and hybrid systems" "Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications" "K. Futatsugi" "2000" "{ENTCS}, Elsevier" "Manuel Clavel" "Francisco Dur'an" "Steven Eker" "Patrick Lincoln" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "Jos'e Quesada" "Towards {Maude} 2.0" "Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications" "K. Futatsugi" "2000" "{ENTCS}, Elsevier" "Manuel Clavel" "Francisco Dur'an" "Narciso Mart'{i}-Oliet" "Polytypic Programming in {Maude}" "Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications" "K. Futatsugi" "2000" "{ENTCS}, Elsevier" "Grit Denker" "Jos'e Meseguer" "C. Talcott" "Rewriting Semantics of Meta-Objects and Composable Distributed Services" "Proc. 3rd. Intl. Workshop on Rewriting Logic and its Applications" "K. Futatsugi" "2000" "{ENTCS}, Elsevier" "Flaviu Cristian" "Agreeing on processor group membership in timed asynchronous distributed systems" "University of California San Diego, Computer Science and Engineering Department" "CSE95-428" "1995" "S. Kasera" "S. Bhattacharyya" "M. Keaton" "D. Kiwior" "J. Kurose" "D. Towsley" "S. Zabele" "Scalable fair reliable multicast using active services" "University of Massachusetts, Amherst, CMPSCI" "TR 99-44" "1999" "Flaviu Cristian" "Synchronous and asynchronous group communication" "Proceedings IEEE Workshop on Fault-tolerant and Parallel Distributed Systems, Honolulu, Hawaii" "1995" "R. Allen" "D. Garlan" "Formalizing Architectural Connection" "Proceedings 16th International Conference on Software Engineering" "1994" "G. Denker" "J. Meseguer" "C. Talcott" "{Rewriting Semantics of Distributed Meta Objects and Composable Communication Services}" "1999" "working draft" "M. Hicks" "P. Kakkar" "J. T. Moore" "C. A. Gunter" "S. Nettles" "{PLAN: A Packet Language for Active Networks}" "Proceedings of the Third {ACM} {SIGPLAN} International Conference on Functional Programming Languages" "1998" "86-93" "ACM" "http://www.cis.upenn.edu/~switchware/papers/plan.ps" "G. Denker" "J. Millen" "{CAPSL Intermediate Language}" "{Workshop on Formal Methods and Security Protocols (FMSP'99), July 5, 1999, Trento, Italy (part of FLOC'99)}" "N. Heintze" "E. Clarke" "1999" "url{http://cm.bell-labs.com/cm/cs/who/nch/fmsp99/}" "G. Denker" "J. Meseguer" "C. Talcott" "{Protocol Specification and Analysis in Maude}" "{Proc. of Workshop on Formal Methods and Security Protocols, 25 June 1998, Indianapolis, Indiana}" "1998" "N. Heintze" "J. Wing" "" "" "" "" "" "url{http://www.cs.bell-labs.com/who/nch/fmsp/index.html}" "{Denker, G." "J. J. Garcia-Luna-Aceves" "J. Meseguer" "P. \"Olveczky" "J. Raju" "B. Smith" "C.} Talcott" "{Specification and Analysis of a Reliable Broadcasting Protocol in Maude}" "{Proc. 37th Annual Allerton Conference on Communication, Control and Computation}" "1999" "B. Hajek" "R. S. Sreenivas" "738-747" "" "University of Illinois" "" "" "url{http://www.comm.csl.uiuc.edu/allerton}" "J. Meseguer" "C. Talcott" "Semantic Interoperation of Dynamic Heterogeneous Architectures" "Technical presentations to EDCS Architecture Cluster Meeting, April and July 1997" "1997" "N. Venkatasubramanian" "C. L. Talcott" "1995" "{Principles of Distributed Computation}" "{Reasoning about Meta Level Activities in Open Distributed Systems}" "Manuel Clavel" "Jos'e Meseguer" "Internal Strategies in a Reflective Logic" "Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction (Townsville, Australia, July 1997)" "B. Gramlich" "H. Kirchner" "1997" "1-12" "Patrick Lincoln" "Jos'e Meseguer" "Strategic Reflection" "Proceedings of the CADE-15 Workshop on Strategies in Automated Deduction (Lindau, Germany, July 1998)" "B. Gramlich" "F. Pfenning" "1998" "3-9" "P. Borovansk'y" "C. Kirchner" "H. Kirchner" "Strategies and Rewriting in {ELAN}" "Proceedings of the CADE-14 Workshop on Strategies in Automated Deduction (Townsville, Australia, July 1997)" "B. Gramlich" "H. Kirchner" "1997" "P. Borovansk'y" "C. Kirchner" "H. Kirchner" "Strategies of {ELAN}: meta-interpretation and partial evaluation" "Proceedings of the International Workshop on Theory and Practice of Algebraic Specifications (Amsterdam, Holland)" "1997" "P.-E. Moreau" "H. Kirchner" "Compilation techniques for associative-commutative normalisation" "Proceedings of the International Workshop on Theory and Practice of Algebraic Specifications (Amsterdam, Holland)" "1997" "Francisco Dur'an" "Jos'e Meseguer" "An extensible module algebra for {Maude}" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "David Basin" "Sean Matthews" "Scoped Metatheorems" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "L. J. Steggles" "P. Kosiuczenko" "A timed rewriting logic semantics for {SDL}: a case study of the alternating bit protocol" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "Francisco Dur'an" "Jos'e Meseguer" "Structured Theories and Institutions" "{em Proc. Category Theory and Computer Science 1999/}, (Edinburgh, Scotland, September 1999) {ENTCS}, Vol. 29, {Elsevier}, 1999, url{http://www.elsevier.nl/locate/entcs/volume29.html}" "Bow-Yaw Wang" "Jos'e Meseguer" "Carl A. Gunter" "Specification and formal analysis of a {PLAN} algorithm in {Maude}" "To appear in Proc. DSVV 2000" "G. Carabetta" "P. Degano" "F. Gadducci" "{CCS} semantics via proved transition systems and rewriting logic" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "Jos'e Meseguer" "Carolyn Talcott" "Mapping {OMRS} to rewriting logic" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "Grit Denker" "Jos'e Meseguer" "Carolyn Talcott" "Rewriting semantics of meta-objects and composable distributed services" "Manuscript, February 1999" "Jos'e Meseguer" "A logical framework for distributed systems and communication protocols" "{em Proc. FORTE/PSTV'98/}, {Kluwer}, 1998" "Manuel Clavel" "Francisco Dur'an" "Steven Eker" "Patrick Lincoln" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "Jos'e Quesada" "{Maude}: specification and programming in rewriting logic" "SRI International, January 1999, url{http://maude.csl.sri.com}" "A. Verdejo" "N. Mart'{i}-Oliet" "Executing and verifying {CCS} in {Maude}" "Technical Report 99-00, Dto. Sistemas Inform'aticos y Programaci'on, Universidad Complutense, Madrid; also, url{http://maude.csl.sri.com}" "Manuel Clavel" "Francisco Dur'an" "Steven Eker" "Patrick Lincoln" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "Jos'e Quesada" "A Tutorial on {Maude}" "SRI International, March 2000, url{http://maude.csl.sri.com}" "Manuel Clavel" "Francisco Dur'an" "Steven Eker" "Patrick Lincoln" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "Jos'e Quesada" "{Maude} as a Metalanguage" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "Manuel Clavel" "Francisco Dur'an" "Steven Eker" "Patrick Lincoln" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "Metalevel computation in {Maude}" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "Steven Eker" "Term rewriting with operator evaluation strategy" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "Peter Borovansk'y" "Salma Jamoussi" "Pierre-Etienne Moreau" "Christophe Ringeissen" "Handling {ELAN} rewrite programs via an exchange format" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "Roberto Bruni" "Jos'e Meseguer" "Ugo Montanari" "Internal strategies in a rewriting implementation of tile systems" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "K. Futatsugi" "R. Diaconescu" "{CafeOBJ} Report" "World Scientific, AMAST Series" "1998" "T. Genet" "Proving termination of sequential reduction relation using tree automata" "Manuscript; INRIA Lorraine, 1997" "F. Gadducci" "U. Montanari" "The tile model" "In G. Plotkin, C. Stirling and M. Tofte, eds., {em Proof, Language and Interaction: Essays in Honour of Robin Milner}, MIT Press. Also, TR-96-27, C.S. Dept., Univ. of Pisa, 1996." "P. Viry" "Rewriting modulo a rewrite system" "TR-95-20, C.S. Department, University of Pisa, 1996." "R. Bruni" "J. Meseguer" "U. Montanari" "Process and term tile logic" "Technical Report SRI-CSL-98-06, SRI International, July 1998." "M.-O. Stehr" "A rewriting semantics for algebraic {Petri} nets" "Manuscript, March 1998, SRI International and C.S. Dept., Univ. of Hamburg, 1998." "J. Meseguer" "C. Talcott" "Using Rewriting Logic to Interoperate Architectural Description Languages ({I and II})" "Lectures at the Santa Fe and Seattle DARPA-EDCS Workshops, March and July 1997. url{http://www-formal.stanford.edu/clt/ArpaNsf/adl-interop.html}." "E. Contejean" "C. March'e" "The {CiME} system: tutorial and user's manual" "Manuscript, Universit'e Paris-Sud, Centre d'Orsay" "M. Clavel" "F. Dur'an" "S. Eker" "J. Meseguer" "P. Lincoln" "An introduction to {Maude} (beta version)" "Manuscript, SRI International, March 1998" "J. J. Garc'{i}a-Luna" "Reliable broadcasting in computer networks" "Manuscript; University of California at Santa Cruz, January 1998" "Grit Denker" "Jos'e Meseguer" "Carolyn Talcott" "Formal specification and analysis of active networks and communication protocols: the {Maude} experience" "Proc. DARPA Information Survivability Conference and Exposition DICEX 2000, Vol. 1, Hilton Head, South Carolina, January 2000" "2000" "251-265" "IEEE" "Jos'e Meseguer" "Rewriting Logic and {Maude}: Concepts and Applications" "Rewriting Techniques and Applications, RTA 2000" "L. Bachmair" "2000" "1-26" "1833" "Springer-Verlag" "Lecture Notes in Computer Science" "Francisco Dur'an" "Steven Eker" "Patrick Lincoln" "Jos'e Meseguer" "Principles of {Mobile} {Maude}" "Agent Systems, Mobile Agents, and Applications, ASA/MA 2000" "D. Kotz" "F. Mattern" "2000" "73-85" "1882" "Springer-Verlag" "Lecture Notes in Computer Science" "C. L. Talcott" "Composable Semantic Models for Actor Theories" "Theoretical Aspects of Computer Science" "Lecture Notes in Computer Science" "T. Ito M. Abadi" "1997" "" "Springer-Verlag" "An Actor Rewriting Theory" "C. L. Talcott" "Proc. 1st Intl. Workshop on Rewriting Logic and its Applications" "J. Meseguer" "1996" "Electronic Notes in Theoretical Computer Science" "4" "North Holland" "J. Meseguer" "C. Talcott" "" "Technical presentations to EDCS Architecture Cluster Meeting, April and July 1997" "1997" "J. Ad'amek" "J. Rosick'y" "Locally Presentable and Accessible Categories" "Cambridge University Press" "1994" "P. D. Mosses" "Action Semantics" "Cambridge University Press" "1992" "P. Burmeister" "Partial Algebras---{S}urvey of a Unifying Approach Towards a Two-Valued Model Theory for Partial Algebras" "Algebra Universalis" "1982" "15" "306-358" "Doron Peled" "Combining partial order reductions with on-the-fly model-checking" "Formal Methods in System Design" "1996" "8" "39-64" "C. Strachey" "Fundamental concepts in programming languages" "Higher-Order and Symbolic Computation" "2000" "13" "11-49" "T. Mossakowski" "Representations, Hierarchies, and Graphs of Institutions" "Fachbereich Mathematik und Informatik der Universit{\"a}t Bremen" "1996" "A. Knapp" "A formal approach to object-oriented software engineering" "Institut f{\"u}r Informatik, Universit{\"a}t M{\"u}nchen" "2000" "To appear" "J. F. Quesada" "{The {SCP} parsing algorithm based on syntactic constraint propagation}" "University of Seville" "{Doctoral Dissertation}" "1997" "A. van Deursen" "Executable Language Definitions" "University of Amsterdam" "1994" "U. Lechner" "Object-oriented specification of distributed systems" "University of Passau" "1997" "Grit Denker" "Jos'e Meseguer" "Carolyn Talcott" "Formal Specification and Analysis of Active Networks and Communication Protocols: The {Maude} Experience" "Manuscript, SRI International, October 1999" "David Basin" "Manuel Clavel" "Jos'e Meseguer" "Reflective metalogical frameworks" "In Proc. LFM'99, (Paris, France, September 1999) url{http://www.cs.bell-labs.com/~felty/LFM99/}" "Manuel Clavel" "Francisco Dur'an" "Steven Eker" "Jos'e Meseguer" "Mark-Oliver Stehr" "{Maude} as a formal meta-tool" "FM'99 --- Formal Methods" "1999" "J. Wing" "J. Woodcock" "1684-1703" "Springer-Verlag" "1709" "Lecture Notes in Computer Science" "Isabel Pita" "Narciso Mart'{i}-Oliet" "Using reflection to specify transaction sequences in rewriting logic" "Recent Trends in Algebraic Development Techniques" "1999" "J. L. Fiadeiro" "261-276" "Springer-Verlag" "1589" "Lecture Notes in Computer Science" "J. Fiadeiro" "N. Mart'{i}-Oliet" "T. Maibaum" "J. Meseguer" "I. Pita" "Towards a Verification Logic for Rewriting Logic" "Recent Trends in Algebraic Development Techniques, WADT'99" "2000" "D. Bert" "C. Choppy" "P. Mosses" "438-458" "Springer-Verlag" "1827" "Lecture Notes in Computer Science" "T. Mossakowski" "Equivalences among Various Logical Frameworks of Partial Algebras" "Computer Science Logic, Paderborn, Germany, September 1995, Selected Papers" "1996" "H. Kleine B{\"u}ning" "403-433" "Springer-Verlag" "1092" "Lecture Notes in Computer Science" "Jos'e Meseguer" "Formal Interoperability" "Proceedings of the 1998 Conference on Mathematics in Artificial Intelligence, Fort Laurerdale, Florida, January 1998" "url{http://rutcor.rutgers.edu/~amai/Proceedings.html}" "1998" "M. Coste" "Localisation, Spectra and Sheaf Representation" "Applications of Sheaves" "1979" "M. P. Fourman" "C. J. Mulvey" "D. S. Scott" "212-238" "Springer-Verlag" "753" "Lecture Notes in Mathematics" "V. Manca" "A. Salibra" "G. Scollo" "Equational Type Logic" "Theoretical Computer Science" "1990" "77" "131-159" "S. Morasca" "M. Pezz`e" "M. Trubian" "Timed high-level nets" "J. of Real-Time Systems" "1991" "3" "165-189" "P. D. Mosses" "Unified Algebras and Institutions" "Proc. Fourth Annual IEEE Symp. on Logic in Computer Science" "1989" "304-312" "Asilomar, California" "June" "W. W. Wadge" "Classified Algebras" "1982" "University of Warwick" "Manuel Clavel" "Francisco Dur'an" "Steven Eker" "Jos'e Meseguer" "Design and Implementation of the {Cafe} Prover and {Church-Rosser} Checker Tools" "1997" "December" "SRI International" "G. F. Stuart" "W. W. Wadge" "Classified Model Abstract Data Type Specification" "1991" "Manuscript, University of Victoria" "Manuel Clavel" "Reflection in General Logics and in Rewriting Logic, with Applications to the {Maude} Language" "1998" "Ph.D. Thesis, University of Navarre" "Manuel Clavel" "Reflection in Rewriting Logic: Metalogical Foundations and Metaprogramming Applications" "2000" "CSLI Publications" "Francisco Dur'an" "A Reflective Module Algebra with Applications to the {Maude} Language" "1999" "Ph.D. Thesis, University of M'alaga" "Jos'e Meseguer" "Membership algebra as a logical framework for equational specification" "1998" "In F. Parisi-Presicce, ed., {it Proc. WADT'97}, 18--61, Springer LNCS 1376" "Jos'e Meseguer" "Ugo Montanari" "Mapping Tile Logic into Rewriting Logic" "1998" "in F. Parisi-Presicce, ed., Proc. WADT'97, Springer LNCS 1376" "{CoFI Task Group on Semantics}" "{CASL}---{T}he {CoFI} Algebraic Specification Language, Version 0.97, {S}emantics" "July" "1997" "url{http://www.brics.dk/Projects/CoFI}" "A. Poign'e" "Algebra Categoricaly" "Category Theory and Computer Programming" "1985" "D. Pitt et al." "76-102" "Springer-Verlag" "240" "Lecture Notes in Computer Science" "Manuel Clavel" "Francisco Dur'an" "Steven Eker" "Jos'e Meseguer" "Building equational proving tools by reflection in rewriting logic" "1998" "April" "Proc. of the CafeOBJ Symposium '98, Numazu, Japan" "CafeOBJ Project" "url{http://maude.csl.sri.com}" "Manuel Clavel" "Francisco Dur'an" "Steven Eker" "Jos'e Meseguer" "Building equational proving tools by reflection in rewriting logic" "2000" "CAFE: An Industrial-Strength Algebraic Formal Method" "Elsevier" "url{http://maude.csl.sri.com}" "M. Ishisone" "T. Sawada" "Brute: brute force rewriting engine" "1998" "April" "Proc. of the CafeOBJ Symposium '98, Numazu, Japan" "CafeOBJ Project" "S. Nakajima" "Encoding mobility in {CafeOBJ}: an exercise of describing mobile code-based software architecture" "1998" "April" "Proc. of the CafeOBJ Symposium '98, Numazu, Japan" "CafeOBJ Project" "A. Knapp" "Case Studies with {CafeOBJ}" "1998" "April" "Proc. of the CafeOBJ Symposium '98, Numazu, Japan" "CafeOBJ Project" "P. Freyd" "Algebra valued functors in general and tensor products in particular" "Coll. Math." "14" "89-106" "1966" "F. W. Lawvere" "Some algebraic problems in the context of functorial semantics of algebraic theories" "Proc. Midwest Category Seminar II" "1968" "41-61" "Springer Lecture Notes in Mathematics No. 61" "Digital Signature Schemes" "B. Pfitzmann" "1996" "Springer-Verlag" "LNCS, Volume 1100" "C. Kirchner" "P. Viry" "Implementing Parallel Rewriting" "Parallelization in Inference Systems" "1992" "B. Fronh{\"o}fer" "G. Wrightson" "123-138" "Springer LNAI 590" "Adel Bouhoula" "Jean-Pierre Jouannaud" "Jos'e Meseguer" "Specification and Proof in Membership Equational Logic" "Proceedings TAPSOFT'97" "1997" "M. Bidoit" "M. Dauchet" "Springer-Verlag" "1214" "67-92" "Lecture Notes in Computer Science" "T. Genet" "Termination proofs using gpo ordering constraints" "Proceedings 22nd International Colloquium on Trees in Algebra and Programming" "1997" "M. Bidoit" "M. Dauchet" "Springer-Verlag" "1214" "249-260" "Lecture Notes in Computer Science" "mbox{Franc{c}ois-Nicola Demers" "Jacques Malenfant}" "Reflection in logic, functional and object-oriented programming: a Short Comparative Study" "IJCAI '95 Workshop on Reflection and Metalevel Architectures and their Applications in AI" "1995" "August" "29-38" "C. Dony J. Malenfant" "P. Cointe" "A Semantics of Introspection in a Reflective Prototype-Based Language" "To appear in emph{Lisp and Symbolic Computation}" "Jos'e Meseguer" "Membership Algebra" "Lecture and abstract at the Dagstuhl Seminar on ``Specification and Semantics,'' July 9, 1996" "Jos'e Meseguer" "Carolynn Talcott" "Rewriting Logic and Secure Mobility" "To appear in {em Proc. Workshop on Foundations for Secure Mobile Code}, Monterey, California, March 1997" "M. Walicki" "S. Meldal" "Algebraic approaches to nondeterminism---an overview" "To appear in emph{Computing Surveys}" "Vijay Saraswat" "Jos'{e} Meseguer" "Carolyn Talcott" "Radha Jagadeesan" "Formal Foundations for {\bf tic-toc}" "February" "1996" "Chris Hankin" "Gamma" "In C. Hankin and H.R. Nielson (editors) {em New Trends in the Integration of Paradigms}, Dagstuhl Seminar Report 125, (9538), 1995" "Peter Aczel" "A general {Church-Rosser} theorem" "Manuscript, University of Manchester, 1978" "Jos'e Meseguer" "Rewriting Logic and {Maude}: a wide-spectrum semantic framework for object-based distributed systems" "Formal Methods for Open Object-based Distributed Systems, FMOODS 2000" "S. Smith" "C. L. Talcott" "2000" "89-117" "Kluwer" "Jos'e Meseguer" "Specifying, analyzing, and programming communication systems in {Maude}" "Communication-Based Systems" "G. Hommel" "2000" "93-101" "Kluwer" "C. L. Talcott" "Interaction Semantics for Components of Distributed Systems" "Formal Methods for Open Object-based Distributed Systems" "E. Najm" "J-B. Stefani" "1997" "154-169" "Chapman & Hall" "E. Najm" "J-B. Stefani" "Computational models for open distributed systems" "Formal Methods for Open Object-based Distributed Systems, Vol. 2" "H. Bowman" "J. Derrick" "1997" "157-176" "Chapman & Hall" "G. Agha" "I. A. Mason" "S. F. Smith" "C. L. Talcott" "A Foundation for Actor Computation" "Journal of Functional Programming" "1996" "to appear" "Vineet Gupta" "Radha Jagadeesan" "Vijay A. Saraswat" "Danny G. Bobrow" "Computing with Continuous Change" "Submitted for publication, October 1995" "Vijay A. Saraswat" "Radha Jagadeesan" "Vineet Gupta" "Timed Default Concurrent Constraint Programming" "Submitted for publication. Extended abstract published in Proc. of the 22nd Ann. ACM SIGPLAN SIGACT Sym. on the Principles of Prog. Lang., San Francisco, January 1995" "Vijay A. Saraswat" "Vineet Gupta" "The {\bf tic-toc} computation model" "Pueblo Working Document #1, July 1996" "William E. Aitken" "Robert L. Constable" "Judith L. Underwood" "Metalogical Frameworks {II}: Using Reflected Decision Procedures" "Technical Report, Computer Sci. Dept., Cornell University, 1993; also, lecture at the Max Planck Institut f{\"u}r Informatik, Saarbr{\"u}cken, Germany, July 1993" "C. Kirchner" "H. Kirchner" "Personal communication" "July 1995" "John Harrison" "Metatheory and reflection in theorem proving: a survey and critique" "University of Cambridge Computer Laboratory" "1995" "Jos'e Meseguer" "Formal Interoperability" "Paper presented at the 14th IMACS World Congress, Atlanta, Georgia, July" "1994" "M. Vittek" "{ELAN}: Un cadre logique pour le prototypage de langages de programmation avec contraintes" "Universit'e Henry Poincar'e --- Nancy I" "1994" "J. Levy" "The calculus of refinements: a formal specification model based on inclusions" "Universitat Polit`ecnica de Catalunya" "1994" "A. Corradini" "F. Gadducci" "U. Montanari" "Relating two categorical models of term rewriting" "Proc. Rewriting Techniques and Applications, Kaiserslautern" "J. Hsiang" "225-240" "1995" "F. Gadducci" "U. Montanari" "Enriched categories as models of computation" "Proc. $5^{th}$ Italian Conference on Theoretical Computer Science, Ravello" "1995" "H. Kirchner" "P.-E. Moreau" "Prototyping completion with constraints using computational systems" "Proc. Rewriting Techniques and Applications, Kaiserslautern" "J. Hsiang" "1995" "E. Battiston" "V. Crespi" "F. De Cindio" "G. Mauri" "Semantic frameworks for a class of modular algebraic nets" "Proc. of the 3rd International AMAST Conference" "1994" "M. Nivat" "C. Rattray" "T. Russ" "G. Scollo" "Springer-Verlag" "Workshops in Computing" "Manuel Clavel" "Jos'e Meseguer" "Axiomatizing reflective logics and languages" "Proceedings of Reflection'96, San Francisco, California, April 1996" "Gregor Kiczales" "263-288" "url{http://jerry.cs.uiuc.edu/reflection/}" "1996" "Proceedings of Reflection'96, San Francisco, California, April 1996" "Gregor Kiczales" "Xerox PARC" "1996" "Proceedings of the Partial Evaluation Dagstuhl Meeting, 1996" "O. Danvy" "R. Gl{\"u}ck" "P. Thiemann" "Springer LNCS 1110" "1996" "Meta-Level Architectures and Reflection" "P. Cointe" "Springer LNCS 1616" "1999" "U. Lechner" "C. Lengauer" "M. Wirsing" "An Object-Oriented Airport" "Recent Trends in Data Type Specification, Santa Margherita, Italy, May/June 1994" "1995" "E. Astesiano" "G. Reggio" "A. Tarlecki" "351-367" "Springer LNCS 906" "T. Mossakowski" "Equivalences among various logical frameworks of partial algebras" "9th Workshop on Computer Science Logic, CSL'95, Paderborn, September 1995" "1996" "H. Kleine B{\"u}ning" "403-433" "Springer LNCS 1092" "A. Corradini" "F. Gadducci" "{CPO} models for infinite term rewriting" "Proc. AMAST'95" "1995" "368-384" "Springer LNCS 936" "P. Borovansk'y" "Implementation of higher-order unification based on calculus of explicit substitutions" "Proc. SOFTSEM'95" "1995" "M. Bartosek" "J. Staudek" "J. Wiedermann" "363-368" "Springer LNCS 1012" "R. Alur" "C. Courcoubetis" "T. A. Henzinger" "P.-H. Ho" "Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems" "Workshop on Theory of Hybrid Systems" "1993" "R. L. Grossman" "A. Nerode" "A. P. Ravn" "H. Rischel" "209-229" "Springer LNCS 739" "Jos'e Meseguer" "Narciso Mart'{i}-Oliet" "From abstract data types to logical frameworks" "Recent Trends in Data Type Specification, Santa Margherita, Italy, May/June 1994" "1995" "E. Astesiano" "G. Reggio" "A. Tarlecki" "48-80" "Springer LNCS 906" "M. Bettaz" "M. Maouche" "How to specify nondeterminism and true concurrency with algebraic term nets" "Recent Trends in Data Type Specification" "1993" "M. Bidoit" "C. Choppy" "164-180" "Springer LNCS 655" "M. Bettaz" "M. Maouche" "Modeling of object based systems with hidden sorted {ECATNets}" "Proc. of MASCOTS'95, Durham, North Carolina" "1995" "307-311" "IEEE" "K. Futatsugi" "T. Sawada" "Cafe as an extensible specification environment" "In {it Proc. of the Kunming International CASE Symposium, Kunming, China, November}" "1994" "H. Reichel" "An Approach to Object Semantics Based on Terminal Co-algebras" "To appear in {it Mathematical Structures in Computer Science/}, 1995. Presented at {em Dagstuhl Seminar on Specification and Semantics}, Schloss Dagstuhl, Germany, May 1993" "C. Landauer" "K. Bellman" "A. Gillam" "Software Infrastructure for System Engineering Support" "{AAAI}'93 Workshop on Artificial Intelligence for System Engineering" "1993" "Common Object Request Borker Architecture and Specification" "OMG" "Hewlett-Packard Company and SunSoft, Inc." "{OMG Document Number 91.12.1}" "1991" "J. G. Stell" "Modelling term rewriting systems by sesqui-categories" "Keele University" "{TR94-02}" "1994" "Also in shorter form in Proc. C.A.E.N., 1994, pp. 121--127" "J. M. Purtilo" "A Software Interconnection Technology" "University of Maryland" "{UMIACS-TR-88-83, CS-TR-2139}" "1988" "J. Lee" "T. W. Malone" "Partially shared views: {A} {SC}heme for Communicating among Groups that Use Different Type Hierarchies" "{ACM} Transactions on Information Systems" "8" "1" "1-26" "1990" "Adel Bouhoula" "Jean-Pierre Jouannaud" "Jos'e Meseguer" "Specification and Proof in Membership Equational Logic" "Theoretical Computer Science" "236" "35-132" "2000" "R. P. Lippmann" "An introduction to computing with neural nets" "{IEEE} {ASSP} Magazine" "April" "4-22" "1987" "M. R. Genesereth" "An Agent-Based Framework for Software Interoperation" "Proceedings {DARPA} Software Technology Conference" "1992" "359-366" "J. W. Lewis" "the {DICE} Team" "Wrappers: Integration Utilities and Services for the {DICE} Architecture" "Proceedings {CALS & CE}: Computer Aided Logistic Systems and Concurrent Engineering" "1991" "445-457" "Connecting Tools Using Message Passing in the Field Environment" "{IEEE} Software" "July" "1990" "57-66" "K. Bellman" "An Approach to Integrating and Creating Flexible Software Environments Supporting the Design of Complex Systems" "Proceedins of {SOAR}'91: The 1991 Symposium on Space Operations, Automation and Research, 9-11 July 1991, Houston, Texas" "1991" "Computer Science and Technology SubDivision, The Aeorspace Corporation, Los Angeles CA, 90009-2957" "C. Landauer" "K. Bellman" "Integrated Simulation Environments" "Proceedins of {DARPA} Variable-Resolution Modeling Conference, 5-6 May 1992, Herndon, Virginia" "1993" "CF-103-DARPA, published by RAND" "C. Landauer" "K. Bellman" "The Role of Self-Referential Logics in a Software Architecture Using Wrappings" "1993" "3rd Irvine Software Symposium" "D. Walter" "K. Bellman" "Some issues in model integration" "1990" "1990 Eastern Simulation Conference" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "General Logics and Logical Frameworks" "D. Gabbay" "What is a Logical System?" "1994" "355-392" "Oxford University Press" "Shmuel Katz" "Refinement with global equivalence proofs in temporal logic" "DIMACS Series in Discrete Mathematics, Vol. 29" "19997" "59-78" "American Mathematical Society" "R. Jagannathan" "Dataflow Models" "E. Y. Zoyama" "Parallel and Distributed Computing Handbook" "1996" "223-238" "McGraw Hill" "Patrick Lincoln" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "Specification, transformation, and programming of concurrent systems in rewriting logic" "G. E. Blelloch" "K. M. Chandy" "S. Jagannathan" "Specification of Parallel Algorithms" "309-339" "DIMACS Series, Vol. 18, American Mathematical Society" "1994" "R. Harper" "D. Sanella" "A. Tarlecki" "Logic representation in {LF}" "D. H. Pitt et al." "Category Theory and Computer Science" "1989" "250-272" "Springer LNCS 389" "Andrea Corradini" "Ugo Montanari" "An algebra of graphs and graph rewriting" "D. H. Pitt et al." "Category Theory and Computer Science" "1991" "236-260" "Springer LNCS 530" "Christophe Ringeissen" "Combination of matching algorithms" "P. Enjalbert et al." "Proceedings of the 11th TACS Symposium" "1994" "187-198" "Springer LNCS 775" "Christophe Ringeissen" "Prototyping combination of unification algorithms with the {ELAN} rule-based programming language" "H. Comon" "Proceedings of the 8th Conference on Rewriting Techniques and Applications" "1997" "Springer LNCS 1232" "K. Ogata" "K. Futatsugi" "An abstract machine for order-sorted conditional term rewriting systems" "H. Comon" "Proceedings of the 8th Conference on Rewriting Techniques and Applications" "1997" "Springer LNCS 1232" "Jos'e Meseguer" "Completions, factorizations and colimits for $omega$-posets" "Mathematical Logic in Computer Science, Salgotarjan, 1978, Colloquia Mathematica Societatis Janos Bolyai" "26" "1981" "509-545" "North Holland" "Maura Cerioli" "Jos'e Meseguer" "May {I} borrow your logic?" "Proceedings of MFCS'93, 18th International Symposium on Mathematical Foundations of Computer Science" "1993" "342-351" "Springer LNCS 711" "Peter Mosses" "Foundations of Modular {SOS}" "Proceedings of MFCS'99, 24th International Symposium on Mathematical Foundations of Computer Science" "1999" "70-80" "Springer LNCS 1672" "C. Braga" "H. Haeusler" "J. Meseguer" "P. Mosses" "Maude {Action} {Tool}: using reflection to map action semantics to rewriting logic" "Proceedings of AMAST'2000" "2000" "Springer LNCS" "To appear" "F. Parisi-Presicce" "S. Veglioni" "Heterogeneous unified algebras" "Proceedings of MFCS'93, 18th International Symposium on Mathematical Foundations of Computer Science" "1993" "618-628" "Springer LNCS 711" "Jos'e Meseguer" "Ugo Montanari" "Vladimiro Sassone" "On the model of computation of {Place/Transition} {Petri} nets" "Proceedings 15th International Conference on Application and Theory of Petri Nets" "1994" "16-38" "Springer LNCS 815" "Jos'e Meseguer" "Ugo Montanari" "Vladimiro Sassone" "Representation Theorems for {Petri} nets" "Foundations of Computer Science: Potential, Theory, Cognition" "C. Freska" "M. Jantzen" "R. Valk" "1997" "239-249" "Springer LNCS 1337" "Patrick Lincoln" "Narciso Mart'{i}-Oliet" "Jos'{e} Meseguer" "Livio Ricciulli" "Compiling rewriting onto {SIMD} and {MIMD/SIMD} machines" "Proceedings of PARLE'94, 6th International Conference on Parallel Architectures and Languages Europe" "1994" "37-48" "Springer LNCS 817" "Patrick Lincoln" "Jos'{e} Meseguer" "Livio Ricciulli" "The {Rewrite Rule Machine Node Architecture and its Performance}" "Proceedings of CONPAR'94, Linz, Austria, September 1994" "1994" "509-520" "Springer LNCS 854" "Jeffrey Arnold" "Duncan Buel" "Elaine Davis" "{SPLASH} 2" "Proceedings of the 1992 Symposium on Parallel Algorithms and Architectures" "1992" "ACM" "J. L. Fiadeiro" "T. Maibaum" "Interconnecting formalisms: supporting modularity, reuse and incrementality" "Proceedings of the 1995 SIGSOFT Conference, Washington DC, USA" "1995" "72-80" "ACM" "Timothy Winkler" "Programming in {OBJ} and {Maude}" "Peter Lauer" "Functional Programming, Concurrency, Simulation and Automated Reasoning" "1993" "229-277" "Springer LNCS 693" "Kokichi Futatsugi" "Joseph Goguen" "Jean-Pierre Jouannaud" "Jos'{e} Meseguer" "Principles of {OBJ}2" "1985" "Proceedings of 12th ACM Symposium on Principles of Programming Languages" "Brian Reid" "ACM" "52-66" "P. M. Hill" "J. W. Lloyd" "The {G\"odel} Language" "University of Bristol, Computer Science Department" "CSTR-92-27" "1992" "Wolfgang Schreiner" "Parallel functional programming: an annotated bibliography" "Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria" "1993" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "Rewriting Logic as a Logical and Semantic Framework" "SRI International, Computer Science Laboratory" "SRI-CSL-93-05" "1993" "August" "To appear in D. Gabbay, ed., {em Handbook of Philosophical Logic/}, Kluwer Academic Publishers" "Unifying Functional, Object-Oriented and Relational Programming with Logical Semantics" "Joseph Goguen" "Jos'{e} Meseguer" "Research Directions in Object-Oriented Programming" "Bruce Shriver" "Peter Wegner" "1987" "417-477" "MIT Press" "Jos'e Meseguer" "A Logical Theory of Concurrent Objects and its realization in the {Maude} Language" "Research Directions in Concurrent Object-Oriented Programming" "Gul Agha" "Peter Wegner" "Akinori Yonezawa" "1993" "314-390" "MIT Press" "Joseph Goguen" "Timothy Winkler" "Jos'e Meseguer" "Kokichi Futatsugi" "Jean-Pierre Jouannaud" "Introducing {OBJ}" "Software Engineering with OBJ: Algebraic Specification in Action" "3-167" "Kluwer" "J.A. Goguen" "G. Malcolm" "2000" "Satoshi Matsuoka" "Akinori Yonezawa" "Analysis of inheritance anomaly in object-oriented concurrent programming languages" "Research Directions in Concurrent Object-Oriented Programming" "Gul Agha" "Peter Wegner" "Akinori Yonezawa" "1993" "107-150" "MIT Press" "Peter Csaba {\"O}lveczky" "Jos'e Meseguer" "Specifying real-time systems in rewriting logic" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "C. L. Talcott" "An actor rewrite theory" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "C. L. Talcott" "An actor rewrite theory" "This volume" "R. Diaconescu" "Hidden sorted rewriting logic" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "M. Schorlemmer" "Bi-rewriting rewriting logic" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "C. Castro" "An approach to solving binary {CSP} using computational systems" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "A. Ciampolini" "E. Lamma" "P. Mello" "C. Stefanelli" "Distributed logic objects: a fragment of rewriting logic and its implementation" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "M. Wirsing" "A. Knapp" "A formal approach to object-oriented software engineering" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "Steven Eker" "Fast matching in combination of regular equational theories" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "Manuel Clavel" "Steven Eker" "Patrick Lincoln" "Jos'e Meseguer" "Principles of {Maude}" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "Manuel Clavel" "Jos'e Meseguer" "Reflection and strategies in rewriting logic" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "Manuel Clavel" "Jos'e Meseguer" "Reflection in conditional rewriting logic" "2000" "Submitted for publication" "P. Borovansk'y" "C. Kirchner" "H. Kirchner" "P.-E. Moreau" "M. Vittek" "{ELAN}: {A} logical framework based on computational systems" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "P. Borovansk'y" "C. Kirchner" "H. Kirchner" "Controlling rewriting by rewriting" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "H. Kirchner" "P.-E. Moreau" "Computational reflection and extension in {ELAN}" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "P. Viry" "Input/Output for {ELAN}" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "C. Landauer" "Discrete event systems in rewriting logic" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "U. Lechner" "Object-oriented specification of distributed systems in the $mu$-calculus and {Maude}" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "U. Lechner" "C. Lengauer" "Modal $mu$-{Maude}" "In {it Object Orientation with Parallelism and Persistence/}, B. Freitag, C.B. Jones, C. Lengauer and H.-J. Schek, editors, Kluwer, 1996" "Isabel Pita" "Narciso Mart'{i}-Oliet" "A {Maude} specification of an object oriented database model for telecommunication networks" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "Rewriting logic as a logical and semantic framework" "Proc. First Intl. Workshop on Rewriting Logic and its Applications" "1996" "J. Meseguer" "Elsevier" "4" "Electronic Notes in Theoretical Computer Science" "url{http://www.elsevier.nl/cas/tree/store/tcs/free/noncas/pc/volume4.htm}" "Jos'e Meseguer (ed.)" "{em Proc. First Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1996" "C. Kirchner" "H. Kirchner (eds.)" "{em Proc. 2nd Intl. Workshop on Rewriting Logic and its Applications/}, {ENTCS}, {North Holland}, 1998" "U. Lechner" "C. Lengauer" "F. Nickl" "M. Wirsing" "How to overcome the inheritance anomaly" "in {it Proc.ECOOP'96/}, Springer LNCS, 1996" "Charles Leiserson" "{FAT-TREES}: Universal Networks for Hardware-Efficient Supercomputing" "MIT, Laboratory for Computer Science, November 1984" "C. Talcott" "Semantics of Component Based Distributed, Open, Heterogeneous Systems" "Manuscript, Stanford University, February 1995" "C. Talcott" "Concurrent Rewriting Interaction Semantics for Abstract Actor Systems" "Manuscript, Stanford University, September 1995" "Jos'e Meseguer" "Carolyn Talcott" "Reasoning theories and rewriting logic" "Manuscript, Stanford University, June 1996" "Dale Miller" "The $pi$-calculus as a theory in linear logic: preliminary results" "Computer Science Department, University of Pennsylvania, February 1992" "Bart Jacobs" "Categorical logic and type theory" "To be published by North-Holland" "Patrick Lincoln" "Jos'e Meseguer" "Babak Taheri" "Timothy Winkler" "Preliminary Estimates for the Use of the Splash {II} System in the Emulation of the Rewrite Rule Machine" "Manuscript, August 1992" "Joseph Goguen" "Jos'e Meseguer" "Software Componet Search" "September 1994. Submitted for publication" "C. Talcott" "Mathematical Foundations for Survivable Systems" "Proceedings of the $14^{\rm th}$ {IMACS} Congress, Atlanta, Georgia, July 1994" "Livio Ricciulli" "Patrick Lincoln" "Jos'e Meseguer" "Distributed simulation of parallel executions" "In {it Proc. 29th Ann. Simulation Symp.}, New Orleans, Louisiana, April 8--11 1996, IEEE" "Livio Ricciulli" "Patrick Lincoln" "Jos'e Meseguer" "Decoupled simulation of parallel computer systems" "SRI International, Computer Science Laboratory, March 1996" "Vladimiro Sassone" "Jos'e Meseguer" "Ugo Montanari" "Inductive Completion of Monoidal Categories and Infinite Net Computations" "Submitted for publication" "Adel Bouhoula" "Micha{\"e}l Rusinowitch" "Implicit Induction in Conditional Theories" "J. of Automated Reasoning" "14" "189-235" "1995" "Joseph Goguen" "Doan Nguyen" "Jos'e Meseguer" "Luqi" "Du Zhang" "Valdis Berzins" "Software Componet Search" "J. of Systems Integration" "6" "93-134" "1996" "P. Degano" "J. Meseguer" "U. Montanari" "Axiomatizing the Algebra of Net Computations and Processes" "1996" "Acta Informatica" "33" "641-667" "C. Beeri" "Theoretical Foundations for {OODB}'s -- {A} Personal Perspective" "IEEE Data Engineering Bulletin" "1991" "14" "2" "8-12" "Luca Cardelli" "A language with distributed scope" "Computing Systems" "1995" "8" "1" "27-59" "Akinori Yonezawa" "Satoshi Matsuoka" "Masahiro Yagusi" "Kenjiro Taura" "Implementing concurrent object-oriented languages on multicomputers" "IEEE Parallel and Distributed Technology Journal" "1993" "1" "2" "49-61" "M. Kifer" "G. Lausen" "{F}-Logic: {A} Higher-Order Language for Reasoning about Objects, Inheritance, and Scheme" "Proc. ACM SIGMOD" "1989" "134-146" "Jos'e Meseguer" "Xiaolei Qian" "A Logical Semantics for Object-Oriented Databases" "Proc. International SIGMOD Conference on Management of Data" "1993" "ACM" "89-98" "S. Abiteboul" "P. Kanellakis" "The Two Facets of Object-Oriented Data Models" "IEEE Data Engineering Bulletin" "1991" "14" "2" "3-7" "S. Abiteboul" "P. Kanellakis" "Object Identity as a Query Language Primitive" "Proc. ACM SIGMOD" "1989" "159-173" "S. Abiteboul" "A. Bonner" "Objects and Views" "Proc. ACM SIGMOD" "1991" "238-247" "S. Abiteboul" "P. Kanellakis" "E. Waller" "Method Schemas" "Proc. 9th PODS" "1990" "ACM" "16-27" "E. Bertino" "A View Mechanism for Object-Oriented Databases" "Proc. EDBT" "1992" "136-151" "Springer LNCS 580" "W. Chen" "M. Kifer" "D. S. Warren" "HiLog as a Platform for Database Languages (or Why Predicate Calculus is not Enough)" "Proc. 2nd Int'l Workshop on Database Programming Languages" "1989" "315-329" "Kokichi Futatsugi" "Trends in Formal Specification Methods based on Algebraic Specification Techniques -- from Abstract Data Types to Software Processes: {A} Personal Perspective --" "Proceedings of the International Conference of Information Technology Commemorating the 30th Anniversary of the Information Processing Society of Japan (InfoJapan'90)" "IPSJ" "1990" "October" "59-66" "ISO" "{IS8807} : Information Processing Systems - Open System Interconnection - {LOTOS} - {A} formal description technique based on the temporal ordering of observational behavior" "1989" "February" "ISO" "CafeOBJ-Project" "Proceedings of the {CafeOBJ} Symposium'98, Numazu, Japan" "1998" "April" "ITU-T" "Recommendation {X}.903 | {ISO}/{IEC} International Standard 10746--3: ``{ODP} Reference Model: Prescriptive Model''" "1995" "ISO" "K. Ohmaki" "K. Futatsugi" "K. Takahashi" "A Basic {LOTOS} Simulator in {OBJ}" "Proceedings of the International Conference of Information Technology Commemorating the 30th Anniversary of the Information Processing Society of Japan (InfoJapan'90)" "IPSJ" "1990" "October" "497-504" "Stanley Peters" "An architecture and a language for software agents communicating to solve problems cooperatively" "1992" "In preparation" "Wesley Phoa" "Using fibrations to understand subtypes" "1992" "To appear in M. Fourman, P. Johnstone, and A. Pitts (eds.) {it Proc. Symp. on Applications of Categories in Computer Science, Durham, 1991}, Cambridge University Press" "J. R. B. Cockett" "R. A. G. Seely" "Weakly distributive categories" "1992" "M. Fourman" "P. Johnstone" "A. Pitts" "Proc. Symp. on Applications of Categories in Computer Science, Durham, 1991" "Cambridge University Press" "45-65" "Pierre-Louis Curien" "Giorgio Ghelli" "Coherence and Subsumption" "1991" "To appear in {it Mathematical Structures in Computer Science}" "Egidio Astesiano" "Gianna Reggio" "Algebraic Specification of Concurrency" "1992" "To appear in {it Proceedings of the ADT'91 Workshop}, Springer LNCS" "Jonathan Ginzburg" "Embedding questions: {Facts} and questions" "1992" "In preparation" "R. Burstall" "R. Diaconescu" "Hiding and Behaviour: An Institutional Approach" "Laboratory for Foundations of Computer Science, University of Edinburgh" "1992" "ECS-LFCS-92-253" "December" "M. Wirsing" "F. Nickl" "U. Lechner" "Concurrent object-oriented design specification in {SPECTRUM}" "Institut f{\"u}r Informatik, Universit{\"a}t M{\"u}nchen" "1995" "P. Kosiuczenko" "M. Wirsing" "Timed rewriting logic with application to object-oriented specification" "Institut f{\"u}r Informatik, Universit{\"a}t M{\"u}nchen" "1995" "Johan Lilius" "Sheaf semantics for {P}etri nets" "1992" "To appear as Technical report, Helsinki University of Technology" "William Tracz" "Formal specification of parameterized programs in {LILEANNA}" "1993" "Manuscript, Version 7.0" "Kristen Nygaard" "Basic concepts in object-oriented programming" "1986" "Lecture and paper delivered at the Object-Oriented Programming Workshop held at Yorktwon Heights, New Yor, June 9-13, 1986; abstract in {it Sigplan Notices}, 21, No. 10, page 187, October 1986" "Lincoln Wallen" "A constructive interpretation of proof search" "1992" "To appear" "Han Yan" "Joseph Goguen" "Tom Kemp" "Proving properties of partial functions with sort constraints" "1992" "To appear" "Joseph Goguen" "Algebraic semantics for the object paradigm" "1992" "To appear" "Ru{a}zvan Diaconescu" "Joseph Goguen" "Petros Stefaneas" "Logical support for modularisation" "1992" "To appear, {em Proceedings/} of Workshop on Logical Frameworks (Edinburgh, Scotland, May 1991)" "J. Hardy" "B. Hasslacher" "Y. Pomeau" "Lattice Gas Automata for the {Navier-Stokes} Equation" "Physical Review Letters" "56" "1986" "1505" "{HOT} Chips {III}" "HOT Chips" "Record of Symposium held at Stanford University August 26--27, 1991" "1991" "IEEE" "Ulrich Schmidt" "Knut Caesar" "Datawave: {A} Single-Chip Multiprocessor for Video Applications" "IEEE Micro" "{IEEE} Computer Society" "11" "3" "22-25" "June" "1991" "Patrick Hayes" "The second naive physics manifesto" "Readings in Knowledge Representation" "Ronald Brachman" "Hector Levesque" "467-485" "1985" "Morgan Kaufmann" "Nancy Lynch" "Distributed Algorithms" "1996" "Morgan Kaufmann" "S. Borkar" "R. Cohn" "G. Cox" "H. T. Kung" "M. Lam" "B. Moore" "C. Peterson" "J. Pieper" "L. Rankin" "P. S. Tseng" "J. Sutton" "J. Urbanski" "J. Webb" "{iWARP}: an integrated solution to high-speed parallel computing" "Proceedings of Supercomputing '88" "IEEE Press" "330-339" "1988" "H. Aida" "J. Goguen" "S. Leinwand" "P. Lincoln" "J. Meseguer" "B. Taheri" "T. Winkler" "Simulation and Performance Estimation for the Rewrite Rule Machine" "Proceedings of the Fourth Symposium on the Frontiers of Massively Parallel Computation" "336-344" "1992" "IEEE" "G. Bracha" "G. Lindstrom" "Modularity meets inheritance" "Proceedings of the International Conference on Computer Languages" "282-290" "1992" "IEEE" "D. Decouchant" "P. Le Dot" "M. Riveill" "C. Roisin" "X. Rousett de Pina" "A synchronization mechanism for an object-oriented distributed system" "Proceedings of the Eleventh International Conference on Distributed Computing Systems" "152-159" "1991" "IEEE" "Joseph Goguen" "Jos'e Meseguer" "Security policies and security models" "Proceedings of the 1982 Symposium on Security and Privacy" "11-20" "1982" "IEEE" "Joseph Goguen" "Jos'e Meseguer" "Unwinding and inference control" "Proceedings of the 1984 Symposium on Security and Privacy" "75-86" "1984" "IEEE" "Denis Caromel" "Concurrency and reusability: from sequential to parallel" "Journal of Object-Oriented Programming" "1990" "September/October" "34-42" "C. Weems" "E. Riseman" "A. Hamson" "The {DARPA} Image Understanding Benchmark for Parallel Computers" "Journal of Parallel and Distributed Computing" "1991" "11" "1" "1-24" "R. Davis" "R. G. Smith" "Negotiation as a metaphor for distributed problem solving" "Artificial Intelligence" "1983" "20" "1" "63-109" "M. Wand" "D. P. Friedman" "The mystery of the tower revealed: a non-reflective description of the reflective tower" "Lisp and Symbolic Computation" "1988" "1" "1" "11-38" "Christoph Walther" "A mechanical solution to {Schubert's} steamroller by many-sorted resolution" "Artificial Intelligence" "1985" "26" "2" "217-224" "John Hayes" "Trevor Mudge" "Hypercube supercomputers" "Proceedings of the IEEE" "1989" "77" "12" "1829-1841" "Nils Nilsson" "Logic and artificial intelligence" "Artificial Intelligence" "1991" "47" "31-56" "Jos'{e} Meseguer" "Ugo Montanari" "Petri Nets Are Monoids" "Information and Computation" "1990" "88" "105-155" "Andrea Asperti" "Simone Martini" "Categorical models of polymorphism" "Information and Computation" "1992" "99" "1-79" "David Mac{Queen}" "Modules for Standard {ML}" "Polymorphism" "1985" "2" "2" "October" "Earlier version appeared in Proc. 1984 ACM Symp. on Lisp and Functional Programming" "L. Moss" "J. Meseguer" "J. A. Goguen" "Final Algebras, Cosemicomputable Algebras, and Degrees of Unsolvability" "Theoretical Computer Science" "1992" "100" "267-302" "Ehud Shapiro" "Akikazu Takeuchi" "Object oriented programming in concurrent {Prolog}" "New Generation Computing" "1983" "1" "25-48" "M. Nigam" "S. Sahni" "D. Shetti" "J. R. Slagle" "Allocation of Weapons to Targets" "Computer Science Department, University of Minnesota" "Joseph Goguen" "Hyperprogramming: a formal approach to software environments" "In Proc. 1990 Symp. on Formal Methods in Software Development, Tokyo, Japan" "Fernand Bedard" "Private communication" "1990" "December" "Sansom Abramsky" "Computational Interpretations of Linear Logic" "Imperial College, October 1990" "Zohar Manna" "Amir Pnueli" "The {Temporal} {Logic} of {Reactive} {Systems}" "To be published by Springer-Verlag" "Egidio Astesiano" "Alessandro Giovini" "Gianna Reggio" "Observational structures and their logics" "To appear in {it Theoretical Computer Science}" "Steven Bloom" "Varieties of Ordered Algebras" "Journal of Computer and System Sciences" "13" "200-212" "1976" "Joseph Goguen" "Jos'{e} Meseguer" "Correctness of recursive parallel nondeterministic flow programs" "Journal of Computer and System Sciences" "27" "268-290" "1983" "Peter Wegner" "Concepts and Paradigms of Object-Oriented Programming" "OOPS Messenger" "1" "7-87" "1990" "Bruno Courcelle" "Infinite trees in normal form and recursive equations having a unique solution" "Mathematical Systems Theory" "13" "131-180" "1979" "Varieties of Chain-Complete Algebras" "Jos'e Meseguer" "1980" "Journal of Pure and Applied Algebra" "19" "347-383" "A mathematical approach to nondeterminism in data types" "W. H. Hesselink" "1988" "ACM Trans. Prog. Lang. and Sys." "10" "87-117" "A formal basis for architectural connection" "R. Allen" "D. Garlan" "1997" "July" "ACM Trans. Soft. Eng. and Meth." "A {Birkhoff}-like Theorem for Algebraic Classes of Interpretations of Program Schemes" "Jos'e Meseguer" "1981" "Formalization of Programming Concepts" "Springer-Verlag" "152-168" "J. Diaz" "I. Ramos" "LNCS, Volume 107" "Parallel Programming in {Maude}" "Jos'{e} Meseguer" "Timothy Winkler" "1992" "Research Directions in High-level Parallel Programming Languages" "Springer LNCS 574" "253-293" "J.-P. Ban^{a}tre" "D. Le M`{e}tayer" "Also Technical Report SRI-CSL-91-08, SRI International, Computer Science Laboratory, November 1991" "A logic programming language with lambda-abstraction, function variables, and simple unification" "Dale Miller" "1990" "Extensions of Logic Programming" "Springer-Verlag" "253-281" "P. Schroeder-Heister" "LNCS, Volume 475" "Temporal Logic" "Johan van Benthem" "Handbook of Logic in Artificial Intelligence and Logic Programming" "Oxford University Press" "D. Gabbay" "C. Hogger" "J. Robinson" "To appear" "Modal and Temporal Logics" "Colin Stirling" "Handbook of Logic in Computer Science" "Oxford University Press" "S. Abramsky" "D. Gabbay" "T. Maibaum" "To appear" "Concurrent Architectures" "Charles L. Seitz" "1990" "{VLSI} and Parallel Computation" "Morgan Kaufmann" "1-84" "R. Suaya" "G. Birtwistle" "Network and processor architecture for message-driven computers" "William Dally" "1990" "{VLSI} and Parallel Computation" "Morgan Kaufmann" "140-222" "R. Suaya" "G. Birtwistle" "On undecidable propositions of formal mathematical systems" "K. {G\"odel}" "1965" "The Undecidable" "Raven Press" "39-74" "Martin Davis" "Algebraic Semantics" "Irene Guessarian" "1981" "Springer-Verlag" "LNCS, Volume 99" "Past, Present, Parallel: {A} survey of Available Computing Systems" "Arthur Trew" "Greg Wilson" "1991" "Springer-Verlag" "Fundamentals of Algebraic Specification 1" "Hartmut Ehrig" "Bernd Mahr" "1985" "Springer-Verlag" "Readings in Knowledge Representation" "Ronald Brachman" "Hector Levesque" "1985" "Morgan Kaufmann" "Formal Structures for Computation and Deduction" "G. Huet" "1986" "INRIA" "Combinatory reduction systems" "J. W. Klop" "1980" "Mathematisch Centrum, Amsterdam" "The Algebraic Semantics of Recursive Program Schemes" "Bruno Courcelle" "Maurice Nivat" "1978" "16-30" "Proceedings, Mathematical Foundations of Computer Science" "LNCS, Volume 64" "Springer-Verlag" "On order-complete universal algebra and enriched functorial semantics" "Jos'e Meseguer" "1977" "Proceedings, Foundations of Computation Theory" "Marek Karpi'nski" "LNCS, Volume 56" "294-301" "Springer-Verlag" "R. Jagannathan" "A. A. Faustini" "The {GLU} Programming Language" "1990" "November" "SRI-CSL-90-11" "SRI International, Computer Science Laboratory" "Gert Smolka" "Martin Henz" "J{\"{o}}rg W{\"{u}}rtz" "Object-oriented concurrent constraint programming in {Oz}" "1993" "April" "RR-93-16" "DFKI, Saarbr{\"{u}}cken" "Kim Bruce" "A paradigmatic object-oriented programming language: design, static typing and semantics" "1992" "January" "CS-92-01" "Williams College" "Joseph Goguen" "Order Sorted Algebra" "1978" "Semantics and Theory of Computation Report 14" "UCLA" "Douglas R. Smith" "Constructing Specification Morphisms" "1992" "January" "KES.U.92.1" "Kestrel Institute" "Paul Hudak" "Report on the Programming Language {Haskell}" "1990" "April" "Computing Science Department, University of Glasgow" "C. Talcott" "A theory of binding structures and applications to rewriting" "1991" "October" "Computer Science Department, Stanford University" "G. Wiederhold" "P. Wegner" "S. Ceri" "Towards {Megaprogramming}" "1990" "October" "STAN-CS-90-1341" "Computer Science Department, Stanford University" "F. Giunchiglia" "C. L. Pecchiari" "C. Talcott" "Reasonig theories: towards an architecture for open mechanized reasoning systems" "1994" "November" "9409-15" "IRST, University of Trento" "Also in {em Workshop on Frontiers of Combining Systems, FROCOS'96, 1996}" "Jos'{e} Meseguer" "Rewriting as a Unified Model of Concurrency" "1990" "February" "SRI-CSL-90-02" "SRI International, Computer Science Laboratory" "Revised June 1990" "Thinking Machines Corporation" "Connection Machine Technical Summary" "1990" "Shigeru Watari" "Shinji Kono" "Ei-ichi Osawa" "Rik Smoody" "Mario Tokoro" "Extending object-oriented systems to support dialectic worldviews" "1989" "Sony Computer Science Laboratory, Tokyo" "Presented at the Advanced Database System Symposium, Kyoto, December 1989" "S. Matsuoka" "K. Wakita" "A. Yonezawa" "Inheritance anomaly in object-oriented concurrent programming languages" "1991" "January" "University of Tokyo, Dept. of Information Science" "Jos'e Meseguer" "Ugo Montanari" "Vladimiro Sassone" "Process versus unfolding semantics for {Place/Transition} {Petri} nets" "Theoretical Computer Science" "153" "1--2" "171-210" "1996" "R. Alur" "C. Courcoubetis" "N. Halbwachs" "T. A. Henzinger" "P.-H. Ho" "X. Nicollin" "A. Olivero" "J. Sifakis" "S. Yovine" "The algorithmic analysis of hybrid systems" "Theoretical Computer Science" "138" "3-34" "1995" "The Chemical Abstract Machine" "{G'{e}rard Berry" "G'{e}rard Boudol}" "Proc. POPL'90" "ACM" "81-94" "1990" "G'{e}rard Berry" "G'{e}rard Boudol" "The Chemical Abstract Machine" "Theoretical Computer Science" "96" "1" "217-248" "1992" "Jos'{e} Meseguer" "Conditional Rewriting Logic as a Unified Model of Concurrency" "Theoretical Computer Science" "96" "1" "73-155" "1992" "Maura Cerioli" "Jos'e Meseguer" "May {I} borrow your logic? ({Transporting} logical structure along maps)" "Theoretical Computer Science" "173" "311-347" "1997" "E. Best" "R. Devillers" "Sequential and concurrent behavior in {Petri} net theory" "Theoretical Computer Science" "55" "87-136" "1989" "Gerard Huet" "A unification algorithm for typed lambda calculus" "Theoretical Computer Science" "1" "1" "27-57" "1973" "Eric Badouel" "Conditional rewrite rules as an algebraic semantics of processes" "1990" "May" "1226" "INRIA" "Gilles Dowek" "Amy Felty" "Hugo Herberlin" "G'erard Huet" "Christine Paulin-Mohring" "Benjamin Werner" "The {Coq} proof assistant user's guide" "1991" "December" "Rapport Technique 134" "INRIA" "P. Degano" "J. Meseguer" "U. Montanari" "Axiomatizing the Algebra of Net Computations and Processes" "1990" "November" "SRI-CSL-90-12" "SRI International, Computer Science Laboratory" "To appear in {em Acta Informatica}" "C. L. Seitz" "J. Seizovic" "W.-K. Su" "The {C} Programmer's Abbreviated Guide to Multicomputer Programming" "1988" "January" "CS-TR-88-1" "California Institute of Technology" "Revised April 1989" "Jos'{e} Meseguer" "Conditional rewriting logic: deduction, models and concurrency" "In S. Kaplan and M. Okada (eds.) {it Proc. CTRS'90}, Montreal, Canada, 1990, Springer LNCS 516, pp. 64-91, 1991" "Patrick Lincoln" "Narciso Mart'{i}-Oliet" "Jos'{e} Meseguer" "Maude: Making parallel programming machine-independent" "Submitted for publication" "Jos'{e} Meseguer" "Conditional rewriting logic: deduction, models and concurrency" "This volume" "P. M. Sewell" "Cell machine correctness via parallel jungle rewriting" "1990" "MSc Thesis, Programming Research Group, University of Oxford" "K. Ohmaki" "K. Futatsugi" "K. Takahashi" "A Basic {LOTOS} simulator in {OBJ}" "1990" "March" "TR-90-11" "ETL" "H. Hussmann" "Nondeterministic algebraic specifications and nonconfluent term rewriting" "Computer Science Dept., TU Munich" "Keith Devlin" "Logic and Information" "Book to appear" "J. Engelfriet" "G. Leih" "G. Rozenberg" "Parallel Object-Based Systems and {Petri} Nets, {I} and {II}" "1990" "February" "90-04,90-05" "Dept. of Computer Science, University of Leiden" "J. Engelfriet" "G. Leih" "G. Rozenberg" "Net-based description of parallel object-based systems, or {POT}s and {POP}s" "Foundations of Object-Oriented Languages, Noordwijkerhout, The Netherlands, May/June 1990" "J. W. de Bakker" "W. P. de Roever" "G. Rozenberg" "1991" "Springer LNCS 489" "229-273" "Sverker Janson" "Seif Haridi" "Programming paradigms of the {Andorra} kernel language" "1991" "Proc. 1991 Intl. Symp. on Logic Programming" "V. Saraswat" "K. Ueda" "MIT Press" "167-186" "Jos'e Meseguer" "Multiparadigm Logic Programming" "Proc. 3rd Intl. Conf. on Algebraic and Logic Programming" "H. Kirchner" "G. Levi" "1992" "Springer LNCS 632" "158-200" "Jos'e Meseguer" "Kokichi Futatsugi" "Timothy Winkler" "Using Rewriting Logic to Specify, Program, Integrate, and Reuse Open Concurrent Systems of Cooperating Agents" "1992" "Proceedings of the 1992 International Symposium on New Models for Software Architecture, Tokyo, Japan, November 1992" "Research Institute of Software Engineering" "61-106" "Sven Frolund" "Inheritance of Synchronization Constraints in Concurrent Object-Oriented Programming Languages" "Proc. ECOOP'92" "O. Lehrmann Madsen" "1992" "Springer LNCS 615" "185-196" "Jos'e Meseguer" "Solving the Inheritance Anomaly in Concurrent Object-Oriented Programming" "Proc. ECOOP'93" "Oscar M. Nierstrasz" "1993" "Springer LNCS 707" "220-246" "Christian Neusius" "Synchronizing Actions" "Proc. ECOOP'91" "Pierre America" "1991" "Springer LNCS 512" "118-132" "Pierre America" "Synchronizing Actions" "Proc. ECOOP'87" "1987" "Springer LNCS 276" "234-242" "Dennis Kafura" "Keung Lee" "Inheritance in actor based concurrent object oriented languages" "Proc. ECOOP'89" "1989" "Cambridge University Press" "131-145" "David Maier" "A Logic for Objects" "Proc. Workshop on Foundations of Deductive Databases and Logic Programming, Washington, D.C." "1986" "6-26" "Joseph Goguen" "Merged Views, Closed Worlds, and Ordered Sorts: Some Novel Database Features in {OBJ}" "Proc. 1982 Workshop on Database Interfaces" "Alex Borgida" "Peter Buneman" "1985" "University of Pennsylvania, Computer Science Department" "38-47" "M. Atkinson" "P. Richard" "P. Trinder" "Bulk types for large scale programming" "Proc. Next Generation Information System Technology" "1991" "Springer LNCS 504" "228-250" "V. Breazu-Tannen" "R. Subrahmanyam" "Logical and computational aspects of programming with sets/bags/lists" "Proc. ICALP'91" "1991" "Springer LNCS 510" "60-75" "P. Degano" "C. Priami" "Proved trees" "Proc. ICALP'92" "1992" "Springer LNCS 623" "629-640" "I. Mason" "C. Talcott" "A semantics preserving actor translation" "Proc. ICALP'97" "1997" "Springer LNCS 1256" "369-378" "I. Mason" "C. Talcott" "Simple Network Protocol Simulation within {Maude}" "May 2000" "Submitted for publication" "C. Hintermeier" "C. Kirchner" "H. Kirchner" "Dynamically-typed computations for order-sorted equational presentations" "Proc. ICALP'94" "1994" "Springer LNCS 510" "60-75" "Hans-Dieter Ehrich" "Joseph Goguen" "Am'{i}lcar Sernadas" "A categorical theory of objects a observed processes" "Foundations of Object-Oriented Languages, Noordwijkerhout, The Netherlands, May/June 1990" "J. W. de Bakker" "W. P. de Roever" "G. Rozenberg" "1991" "Springer LNCS 489" "203-228" "J. Fiadeiro" "A. Sernadas" "Structuring Theories on Consequence" "D. Sannella" "A. Tarlecki" "Recent Trends in Data Type Specification" "1988" "Springer LNCS 332" "44-72" "J. R. Slagle" "R. R. Cantone" "E. J. Halpern" "Battle, an expert decision aid for fire support command and control" "Proceedings 49th MORS" "1982" "35-38" "J. Engelfriet" "G. Leih" "G. Rozenberg" "Parallel Object-Based Systems and {Petri} Nets. {Part} {I}: Basic Notions, Reference Passing and Handshaking" "1990" "February" "90-04" "Dept. of Computer Science, University of Leiden" "C. Hintermeier" "C. Kirchner" "H. Kirchner" "Dynamically-typed computations for order-sorted equational presentations" "1994" "March" "2208" "INRIA" "J. Engelfriet" "G. Leih" "G. Rozenberg" "Parallel Object-Based Systems and {Petri} Nets. {Part} {II}: Actor Systems, Dangling References and Semantics" "1990" "February" "90-05" "Dept. of Computer Science, University of Leiden" "Peter Mosses" "Unified Algebras and Institutions" "1989" "Computer Science Department, Aarhus University" "DAIMI PB-274" "Peter Mosses" "Unified Algebras and Institutions" "1989" "Computer Science Department, Aarhus University" "DAIMI PB-274" "J. A. Goguen" "S. Leinwand" "J. Meseguer" "T. Winkler" "The Rewrite Rule Machine, 1988" "1989" "Oxford University, Programming Research Group" "PRG-76" "Categorical Foundations for General Systems Theory" "Joseph Goguen" "Advances in Cybernetics and Systems Research" "F. Pichler" "R. Trappl" "1973" "Transcripta Books" "121-130" "Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems" "Gerard Huet" "Journal of the Association for Computing Machinery" "27" "797-821" "1980" "Preliminary version in {it 18th Symposium on Mathematical Foundations of Computer Science}, 1977" "The Family of Concurrent Logic Programming Languages" "E. Shapiro" "ACM Computing Surveys" "21" "413-510" "1989" "Programming Languages for Distributed Computing Systems" "H. Bal" "J. Steiner" "A. Tanenbaum" "ACM Computing Surveys" "21" "261-322" "1989" "Subequalizers" "J. Lambek" "Canadian Math. Bull." "13" "337-349" "1970" "Rewrite Systems" "N. Dershowitz" "J.-P. Jouannaud" "Handbook of Theoretical Computer Science, Vol. B" "1990" "J. van Leeuwen" "243-320" "North-Holland" "Graph rewriting: an algebraic and logic approach" "B. Courcelle" "Handbook of Theoretical Computer Science, Vol. B" "1990" "J. van Leeuwen" "193-242" "North-Holland" "The incompleteness theorems" "C. Smorynski" "Handbook of Mathematical Logic" "1977" "J. Barwise" "821-865" "North-Holland" "{OBJ} as a Theorem Prover with Application to Hardware Verification" "Joseph Goguen" "Current Trends in Hardware Verification and Automated Theorem Proving" "P. S. Subramanyam" "G. Birtwistle" "1989" "Springer-Verlag" "218-267" "Objects" "Joseph Goguen" "International Journal of General Systems" "1" "4" "1975" "237-243" "General Recursive Functions of Natural Numbers" "Stephen C. Kleene" "Mathematische Annalen" "112" "5" "1936" "727-742" "$lambda$-definability and recursiveness" "Stephen C. Kleene" "Duke Math. J." "2" "1936" "340-353" "Principles of Parameterized Programming" "Joseph Goguen" "Software Reusability, Volume {I}: Concepts and Models" "Ted Biggerstaff" "Alan Perlis" "Addison-Wesley" "1989" "159-225" "Applications of Algebraic Specification Using {OBJ}" "Joseph Goguen" "Cambridge University Press" "1993" "Graph Grammars and their Application to Computer Science" "H. Ehrig" "H.-J. Kreowski" "G. Rozenberg" "Springer LNCS 532" "1991" "J.-C. Raoult" "F. Voisin" "Set-theoretic graph rewriting" "Graph Transformations in Computer Science" "H.-J. Schneider" "H. Ehrig" "312-325" "Springer LNCS 776" "1994" "Graph Transformations in Computer Science" "H.-J. Schneider" "H. Ehrig" "Springer LNCS 776" "1994" "Term Graph Rewriting" "M. R. Sleep" "M. J. Plasmeijer" "M. C. J. D. van Eekelen" "Wiley" "1993" "The Logic of Typed Feature Structures" "Bob Carpenter" "Cambridge University Press" "1992" "A. Yonezawa" "M. Tokoro" "Object-Oriented Concurrent Programming" "MIT Press" "1988" "Valentin F. Turchin" "Refal-5: programming guide and reference manual" "New England Publishing Co." "1989" "Brian Smith" "Akinori Yonezawa" "Proc. of the {IMSA}'92 International Workshop on Reflection and Meta-Level Architecture, Tokyo, November 1992" "Research Institute of Software Engineering" "1992" "M. Tokoro" "O. Nierstrasz" "P. Wegner" "Object-Based Concurrent Computing" "Springer LNCS 612" "1992" "A. Bond" "L. Gasser" "Readings in Distributed Artificial Intelligence" "Morgan Kaufmann" "1988" "G. Saake" "A. Sernadas" "Information Systems---Correctness and Reusability" "Technische Universit{\"{a}}t Braunschweig, Information-Berichte 91-03" "1991" "R. Junglclaus" "G. Saake" "T. Hartmann" "C. Sernadas" "Object-oriented specification of information systems: the {TROLL} language" "Technische Universit{\"{a}}t Braunschweig, Information-Berichte 91-04" "1991" "W. Hillis" "The Connection Machine" "MIT Press" "1985" "P. M. Hill" "J. W. Lloyd" "The {G\"odel} Programming Language" "MIT Press" "1994" "Gregor Kiczales" "Jim des Rivieres" "Daniel G. Bobrow" "The Art of the Metaobject Protocol" "MIT Press" "1991" "V. Madisetti" "D. Nicol" "R. Fujimoto" "Advances in Parallel and Distributed Simulation" "Society for Computer Simulation" "1990" "R. K. Ege" "Object-oriented Simulation" "Society for Computer Simulation" "1990" "Proc. Workshop on graph reduction, Santa Fe, New Mexico" "1987" "R. Keller" "J. Fasel" "Springer LNCS 279" "Proceedings, Conference on Conditional Term Rewriting, Orsay, France, July 8-10, 1987" "Jean-Pierre Jouannaud" "Stephane Kaplan" "Springer-Verlag, LNCS No. 308" "1988" "The Situation in Logic" "The situation in logic" "Center for the Study of Language and Information" "CSLI Lecture Notes No. 17" "1989" "Concurrent Programming Using Actors" "G. Agha" "C. Hewitt" "Object-Oriented Concurrent Programming" "A. Yonezawa" "M. Tokoro" "MIT Press" "37-53" "1988" "Concurrent object-oriented programming in {Act 1}" "Henry Lieberman" "Object-Oriented Concurrent Programming" "A. Yonezawa" "M. Tokoro" "MIT Press" "9-36" "1988" "{POOL-T}: {A} parallel object-oriented language" "Pierre America" "Object-Oriented Concurrent Programming" "A. Yonezawa" "M. Tokoro" "MIT Press" "199-220" "1988" "Semantic Specifications for the Rewrite Rule Machine" "J. A. Goguen" "Concurrency: Theory, Language and Architecture" "A. Yonezawa" "W. {Mc}{Coll}" "T. Ito" "216-234" "Springer LNCS, Vol. 491" "1990" "G. Agha" "Actors" "MIT Press" "1986" "A. Chien" "Concurrent Aggregates" "MIT Press" "1993" "K. Mani Chandy" "Jayadev Misra" "Parallel Program Design: {A} Foundation" "Addison-Wesley" "1988" "I. Jacobson" "M. Christerson" "P. Jonsson" "G. {\"O}vergaard" "Object-Oriented Software Engineering" "Addison-Wesley" "1993" "M. Fowler" "K. Scott" "{UML} Distilled" "Addison-Wesley" "1997" "M. Shaw" "D. Garlan" "Software Architecture" "Prentice Hall" "1996" "K. Mani Chandy" "Stephen Taylor" "An Introduction to Parallel Programming" "Jones and Bartlett Publishers" "1992" "H. P. Barendregt" "{The} {Lambda} {Calculus}, its {Syntax} and {Semantics}" "North-Holland" "1984" "H. B. Curry" "R. Feys" "Combinatory Logic" "North-Holland" "1968" "A. D. Goldberg" "D. Robson" "Smalltalk80: The Language and its Implementation" "Addison-Wesley" "1983" "Jos'{e} Meseguer" "General Logics" "Logic Colloquium'87" "1989" "H.-D. Ebbinghaus et al." "North-Holland" "275-329" "S. Holmstrom" "A Linear Functional Language" "Workshop on Implementation of Lazy Functional Languages" "1988" "T. Johnsson" "S. Peyton-Jones" "K. Karlsson" "Univ. of G{\"{o}}teborg and Chalmers University of Technology" "13-32" "Philip Wadler" "Is there a use for linear logic?" "ACM/IFIP Symposium on Partial Evaluation and Semantic Based Program Manipulation" "1991" "ACM" "Catriel Beeri" "New Data Models and Languages---the Challenge" "Proc. 11th Symposium on Principles of Database Systems" "1992" "1-15" "ACM" "Catriel Beeri" "Tova Milo" "Functional and Predicative Programming in {OODB}'s" "Proc. 11th Symposium on Principles of Database Systems" "1992" "176-190" "ACM" "Andrea Corradini" "Ugo Montanari" "An algebraic semantics of logic programs as structured transition systems" "S. Debray" "M. Hermenegildo" "North American Conference on Logic Programming" "788-812" "1990" "MIT Press" "H. Hussmann" "Unification in conditional equational theories" "Proc. {EUROCAL} 2" "B. F. Caviness" "Springer LNCS, Vol. 204" "1985" "543-553" "Michael J. O'Donnell" "Survey of the Equational Logic Programming Project" "Resolution of Equations in Algebraic Structures" "1987" "Maurice Nivat" "Hassan A{\"{}i}t-Kaci" "MCC Corporation" "Preliminary Proceedings" "J. Darlington" "M. J. Reeve" "Alice: {A} Multiprocessor Reduction Machine for the Parallel Evaluation of Applicative Languages" "ACM Conference on Functional Programming Languages and Computer Architecture" "1981" "ACM" "John Hughes" "Super-combinators: a new implementation method for applicative languages" "1-10" "ACM Symposium on Lisp and Functional Programming" "1982" "ACM" "Jos'{e} Meseguer" "A Logical Theory of Concurrent Objects" "{ECOOP-OOPSLA'90} Conference on Object-Oriented Programming, Ottawa, Canada, October 1990" "101-115" "1990" "ACM" "Jean-Marc Andreoli" "Remo Pareschi" "{LO} and behold! {Concurrent} structured processes" "{ECOOP-OOPSLA'90} Conference on Object-Oriented Programming, Ottawa, Canada, October 1990" "44-56" "1990" "ACM" "Jean-Marc Andreoli" "Remo Pareschi" "Communication as fair distribution of knowledge" "{OOPSLA'91} Conference on Object-Oriented Programming, Phoenix, Arizona, October 1991" "212-229" "1991" "ACM" "Yutaka Ishikawa" "Communication Mechanism on Autonomous Objects" "{OOPSLA'92} Conference on Object-Oriented Programming" "303-314" "1992" "ACM" "Chris Tomlinson" "Vineet Singh" "Inheritance and Synchronization with Enabled Sets" "{OOPSLA'89} Conference on Object-Oriented Programming" "103-112" "1989" "ACM" "Ken Wakita" "Akinori Yonezawa" "Linguistic Support for Development of Distributed Organizational Information Systems" "Proc. {ACM COCS}" "1991" "ACM" "Etsuya Shibayama" "Reuse of concurrent object descriptions" "Proc. {TOOLS 3}, Sydney" "254-266" "1990" "Denis Caromel" "Programming abstractions for concurrent programming---a solution to the explicit/implicit control dilemma" "Proc. {TOOLS 3}, Sydney" "245-253" "1990" "Paul Bergstein" "Object-preserving class transformations" "{OOPSLA'91} Conference on Object-Oriented Programming, Phoenix, Arizona, October 1991" "299-313" "1991" "ACM" "Oscar Nierstrasz" "Michael Papathomas" "Viewing objects as patterns of communicating agents" "{ECOOP-OOPSLA'90} Conference on Object-Oriented Programming, Ottawa, Canada, October 1990" "38-43" "1990" "ACM" "S. Watari" "S. Kono" "E. Osawa" "R. Smoody" "M. Tokoro" "Extending object-oriented systems to support dialectic worldviews" "Symposium on Advanced Database Systems, Kyoto, Japan, December 1989" "1989" "A. Yonezawa" "J.-P. Briot" "Etsuya Shibayama" "Object-oriented Concurrent Programming in {ABCL/1}" "{OOPSLA'86} Conference on Object-Oriented Programming, Portland, Oregon, September-October 1986" "1986" "258-268" "ACM" "N. Kobayashi" "A. Yonezawa" "Type-theoretic foundations for concurrent object-oriented programming" "{OOPSLA'94} Conference on Object-Oriented Programming, Portland, Oregon, October 1994" "1994" "31-45" "ACM" "Oscar Nierstrasz" "Active Objects in {Hybrid}" "{OOPSLA'87} Conference on Object-Oriented Programming" "1987" "243-253" "ACM" "Bertrand Meyer" "Genericity versus inheritance" "{OOPSLA'86} Conference on Object-Oriented Programming, Portland, Oregon, September-October 1986" "1986" "391-405" "ACM" "T. Watanabe" "A. Yonezawa" "Reflection in an Object-Oriented Concurrent Language" "{OOPSLA'88} Conference on Object-Oriented Programming, San Diego, California, September 1988" "1986" "306-315" "ACM" "G. Agha" "P. Wegner" "A. Yonezawa" "Proceedings of the {ACM}-{SIGPLAN} Workshop on Object-Based Concurrent Programming" "ACM Sigplan Notices, April 1989" "B. Kramer" "Specifying Concurrent Objects" "G. Agha" "P. Wegner" "A. Yonezawa" "Proceedings of the ACM-SIGPLAN Workshop on Object-Based Concurrent Programming" "1989" "162-164" "ACM" "Sigplan Notices, April 1989" "O. Nierstrasz" "Two Models of Concurrent Objects" "G. Agha" "P. Wegner" "A. Yonezawa" "Proceedings of the ACM-SIGPLAN Workshop on Object-Based Concurrent Programming" "1989" "174-176" "ACM" "Sigplan Notices, April 1989" "R. A. G. Seely" "Linear Logic, $\ast$-Autonomous Categories and Cofree Coalgebras" "Proc. AMS Summer Research Conference on Categories in Computer Science and Logic, Boulder, Colorado, June 1987" "J. W. Gray" "A. Scedrov" "371-382" "AMS" "1989" "Nachum Dershowitz" "David A. Plaisted" "Equational Programming" "Machine Intelligence 11: The logic and acquisition of knowledge" "J. Richards" "21-56" "Oxford University Press" "1988" "H. Reichel" "Initial Computability, Algebraic Specifications, and Partial Algebras" "Oxford University Press" "1987" "Bengt Nordstr{\"o}m" "Kent Petersson" "Jan Smith" "Programming in {Martin-L\"of} Type Theory" "Oxford University Press" "1990" "A small complete category" "J. M. E. Hyland" "Proc. Conf. on Church's Thesis: Fifty Years Later" "1987" "A. Grothendieck" "J. L. Verdier" "Pr'{e}fascieaux" "Th'{e}orie de Topos et Cohomologie Etale des Sch'{e}mas, SGA4" "1972" "J. L. Verdier {M. Artin, A Grothendieck}" "Springer Lecture Notes in Mathematics No. 269" "P. Gabriel" "F. Ulmer" "{Lokal} pr{\"{a}}sentierbare {Kategorien}" "1971" "Springer Lecture Notes in Mathematics No. 221" "G. M. Kelly" "R. Street" "Review of the elements of 2-categories" "{Category} {Seminar}, {Sydney} 1972/73" "1974" "75-103" "G. M. Kelly" "Springer Lecture Notes in Mathematics No. 420" "H. Volger" "Completeness Theorem for Logical Categories" "Model Theory and Topoi" "1975" "F. W. Lawvere" "C. Maurer" "G. C. Wraith" "Springer Lecture Notes in Mathematics No. 445" "Orville Keane" "Abstract {Horn} theories" "Model Theory and Topoi" "1975" "15-50" "F. W. Lawvere" "C. Maurer" "G. C. Wraith" "Springer Lecture Notes in Mathematics No. 445" "Joachim Lambek" "Deductive Systems and Categories {II}" "Category Theory, Homology Theory and their Applications I" "1969" "76-122" "Springer Lecture Notes in Mathematics No. 86" "J. W. Gray" "Fibred and Cofibred Categories" "Proc. Conf. Categorical Algebra, La Jolla 1965" "1966" "S. Eilenberg" "D. K. Harrison" "S. MacLane" "H. R{\"{o}}hrl" "Springer-Verlag" "A. Grothendieck" "Cat'{e}gories fibr'{e}es et descente" "Seminaire de g'{e}om'{e}trie alg'{e}brique" "1961" "Institut des Hautes '{E}tudes Scientifiques" "H.-D. Ebbinghaus" "Extended Logics: The General Framework" "Model-Theoretic Logics" "1985" "J. Barwise" "S. Feferman" "25-76" "Springer Verlag" "Joseph Goguen" "Higher-order functions considered unnecessary for higher-order programming" "Proc., University of Texas Year of Programming, Institute on Declarative Programming" "1988" "David Turner" "Preliminary version as SRI Tech. Rep. SRI-CSL-88-1, January 1988" "Addison-Wesley" "J. Reynolds" "G. Plotkin" "On functors expressible in the polymorphic typed lambda calculus" "Logical Foundations of Functional Programming" "1988" "G. Huet" "To appear" "Addison-Wesley" "G. Plotkin" "Complete Partial Orders, a Tool for Making Meanings" "Pisa Summer School Lecture Notes" "1978" "E. S. Bainbridge" "P. J. Freyd" "A. Scedrov" "P. J Scott" "Functorial Polymorphism" "Logical Foundations of Functional Programming" "1988" "G. Huet" "To appear" "Addison-Wesley" "G. Longo" "E. Moggi" "Constructive natural deduction and its ``modest'' interpretation" "Semantics of Natural and Computer Languages" "1988" "M. Gawron" "D. Israel" "J. Meseguer" "S. Peters" "To appear" "MIT Press" "J. A. Goguen" "J. Meseguer" "Logic Programming and Situation Semantics" "Semantics of Natural and Computer Languages" "1988" "M. Gawron" "D. Israel" "J. Meseguer" "S. Peters" "To appear" "MIT Press" "J. M. E. Hyland" "The Effective Topos" "The L.E.J. Brouwer Centenary Symposium" "1982" "A. S. Toelstra" "D. van Dalen" "165-216" "North-Holland" "A. M. Pitts" "Polymorphism is set theoretic, constructively" "Proceedings of the Summer Conference on Category Theory and Computer Science, Edinburgh, Sept. 1987" "1987" "Springer LNCS 283" "Jos'{e} Meseguer" "Ugo Montanari" "Vladimiro Sassone" "On the semantics of {P}etri nets" "Proceedings of the Concur'92 Conference, Stony Brook, New York, August 1992" "W. R. Cleaveland" "1992" "286-301" "Springer LNCS 630" "Jos'{e} Meseguer" "Rewriting as a Unified Model of Concurrency" "Proceedings of the Concur'90 Conference, Amsterdam, August 1990" "1990" "384-400" "Springer LNCS 458" "Jos'{e} Meseguer" "Rewriting logic as a semantic framework for concurrency: a progress report" "Proc. CONCUR'96, Pisa, August 1996" "U. Montanari" "V. Sassone" "331-372" "1996" "Springer LNCS 1119" "Jos'e Meseguer" "Carolyn Talcott" "A partial order event model for concurrent objects" "Proc. CONCUR'99, Eindhoven, The Netherlands, August 1999" "J.C.M. Baaten" "S. Mauw" "415-430" "1999" "Springer LNCS 1664" "Jos'{e} Meseguer" "Carolyn Talcott" "A Partial Order Event Model for Concurrent Objects" "Proc. CONCUR'99, Eindhoven, The Netherlands, August 1999" "J. Baeten" "S. Mauw" "415-430" "1999" "Springer LNCS 1664" "D. E. Rydeheard" "J. G. Stell" "Foundations of Equational Deduction: {A} Categorical Treatment of Equational Proofs and Unification Algorithms" "114-139" "Proceedings of the Summer Conference on Category Theory and Computer Science, Edinburgh, Sept. 1987" "1987" "Springer LNCS 283" "H. Ehrig" "Introduction to the Algebraic Theory of Graph Grammars" "Graph-Grammars and their Application to Computer Science and Biology" "V. Claus" "H. Ehrig" "G. Rozenberg" "1979" "1-69" "Springer LNCS 73" "L. Moss" "J. Meseguer" "J. A. Goguen" "Final Algebras, Cosemicomputable Algebras, and Degrees of Unsolvability" "Proceedings of the Summer Conference on Category Theory and Computer Science, Edinburgh, Sept. 1987" "1987" "Springer LNCS 283" "Extended version to appear in {it Theoretical Computer Science}" "T. Coquand" "T. Ehrhard" "An Equational Presentation of Higher Order Logic" "Proceedings of the Summer Conference on Category Theory and Computer Science, Edinburgh, Sept. 1987" "1987" "Springer LNCS" "Thomas Ehrhard" "A categorical semantics of constructions" "Proceedings of the 3rd Sympossium on Logic in Computer Science, Edinburgh, July 1988" "1988" "264-273" "IEEE" "D. S. Scott" "Models for Various Type-free Calculi" "Proc. 4th Intl. Congr. on Logic, Methodology and Philosophy of Science, Bucharest" "1972" "157-187" "North-Holland" "J. C. Reynolds" "Polymorphism is Not Set-Theoretic" "Semantics of Data Types" "1984" "G. Kahn" "D. B. MacQueen" "G. D. Plotkin" "145-156" "Springer LNCS 173" "R. Burstall" "B. Lampson" "A Kernel Language for Abstract Data Types and Modules" "Semantics of Data Types" "1984" "G. Kahn" "D. B. MacQueen" "G. D. Plotkin" "1-50" "Springer LNCS 173" "K. Bruce" "A. Meyer" "The Semantics of Second Order Polymorphic Lambda Calculus" "Semantics of Data Types" "1984" "G. Kahn" "D. B. MacQueen" "G. D. Plotkin" "131-144" "Springer LNCS 173" "K. L. Clark" "Negation as Failure" "Logic and Data Bases" "1978" "H. Gallaire" "J. Minker" "293-322" "Plenum" "J. A. Goguen" "T. Winkler" "Introducing {OBJ3}" "Computer Science Laboratory, SRI International" "SRI-CSL-88-9" "August" "1988" "T. Winkler" "Numerical Computation on the {RRM}" "Computer Science Laboratory, SRI International" "SRI-CSL-TN88-3" "November" "1988" "H.-J. Kreowski" "Partial Algebras Flow from Algebraic Specifications" "FB Informatik, Univ. Bremen" "" "August" "1986" "Order-Sorted Algebra {I}: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations" "Joseph Goguen" "Jos'{e} Meseguer" "Theoretical Computer Science" "1992" "105" "217-273" "Order-Sorted Algebra {I}: Equational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operations" "Joseph Goguen" "Jos'{e} Meseguer" "Theoretical Computer Science" "1992" "105" "217-273" "Order-Sorted Algebra Solves the Constructor-Selector, Multiple Representation and Coercion Problems" "Jos'{e} Meseguer" "Joseph Goguen" "Information and Computation" "1993" "103" "1" "114-158" "Order-Sorted Algebra Solves the Constructor-Selector, Multiple Representation and Coercion Problems" "Jos'{e} Meseguer" "Joseph Goguen" "To appear in {it Information and Computation}" "Duality in closed and linear categories" "Narciso Mart'i-Oliet" "Jos'e Meseguer" "SRI International, Computer Science Laboratory" "1990" "February" "SRI-CSL-90-01" "Inclusions and subtypes {I}: First Order Case" "Narciso Mart'i-Oliet" "Jos'e Meseguer" "J. Logic and Computation" "6" "409-438" "1996" "Inclusions and subtypes {II}: Higher-Order Case" "Narciso Mart'i-Oliet" "Jos'e Meseguer" "To appear in {it J. Logic and Computation}; appeared also as SRI Report SRI-CSL-90-16" "Inclusions and subtypes {I}: First Order Case" "Narciso Mart'i-Oliet" "Jos'e Meseguer" "To appear in {it J. Logic and Computation}, 1996" "Inclusions and subtypes {II}: Higher-Order Case" "Narciso Mart'i-Oliet" "Jos'e Meseguer" "To appear in {it J. Logic and Computation}, 1996" "An Algebraic Axiomatization of Linear Logic Models" "Narciso Mart'i-Oliet" "Jos'e Meseguer" "G. M. Reed" "A. W. Roscoe" "R. Wachter" "1991" "Topology and Category Theory in Computer Science" "Oxford University Press" "335-355" "Types as theories" "Joseph Goguen" "G. M. Reed" "A. W. Roscoe" "R. Wachter" "1991" "Topology and Category Theory in Computer Science" "Oxford University Press" "357-390" "On Types and {FOOPS}" "Joseph Goguen" "David Wolfram" "To appear in {it Proc. IFIP Working Group 2.6 Working Conference on Database Semantics: Object-Oriented Databases: Analysis, Design and Construction, 1990}" "A sheaf semantics for {FOOPS} expressions (extended abstract)" "Joseph Goguen" "David Wolfram" "M. Tokoro" "O. Nierstrasz" "P. Wegner" "Object-Based Concurrent Computing" "Springer LNCS 612" "81-98" "1992" "Object-oriented concurrent reflective architectures" "Satoshi Matsuoka" "Takuo Watanabe" "Yuuji Ichisugi" "Akinori Yonezawa" "M. Tokoro" "O. Nierstrasz" "P. Wegner" "Object-Based Concurrent Computing" "Springer LNCS 612" "211-226" "1992" "Order-sorted algebra {II}" "Jos'e Meseguer" "Joseph Goguen" "In preparation" "Proving and Rewriting" "Joseph Goguen" "In {Proc.} {Conf.} on {Algebraic} and {Logic} {Programming}, {Nancy}, {Springer} {LNCS} 463, 1990" "Logic programs with equational type specifications" "Michael Hanus" "In {Proc.} {Conf.} on {Algebraic} and {Logic} {Programming}, {Nancy}, {Springer} {LNCS} 463, 70-85, 1990" "The Rewrite Rule Machine" "Joseph Goguen" "Jos'{e} Meseguer" "Sany Leinwand" "Timothy Winkler" "Hitoshi Aida" "SRI International, Computer Science Laboratory" "1989" "March" "SRI-CSL-89-6" "Equational Logic Programming" "Maarten H. van Emden" "Keitaro Yukawa" "University of Waterloo" "1986" "March" "CS-86-05" "Standard {ML}" "Robert Harper" "David MacQueen" "Robin Milner" "Dept. of Computer Science, University of Edinburgh" "1986" "ECS-LFCS-86-2" "A calculus of mobile processes {I} and {II}" "Robin Milner" "Joachim Parrow" "David Walker" "Dept. of Computer Science, University of Edinburgh" "1989" "ECS-LFCS-89-85&86" "A Structural Approach to Operational Semantics" "Gordon D. Plotkin" "Computer Science Dept., Aarhus University" "1981" "DAIMI FN-19" "Galleries and Institutions" "Brian H. Mayoh" "Computer Science Dept., Aarhus University" "1985" "DAIMI PB-191" "Domain Theoretic Models of Polymorphism" "T. Coquand" "C. Gunter" "G. Winskel" "Computer Laboratory, Univ. of Cambridge" "1987" "116" "Di-Domains as a Model of Polymorphism" "T. Coquand" "C. Gunter" "G. Winskel" "Computer Laboratory, Univ. of Cambridge" "1987" "107" "The Semantics of Second-Order Lambda Calculus" "K. Bruce" "A. Meyer" "J. Mitchell" "Lab. Computer Sci., MIT" "1985" "to appear" "Dag Prawitz" "Natural Deduction" "Almqvist and Wiksell, Stockholm" "1965" "Wolfgang Reisig" "Petri Nets" "Springer-Verlag" "1985" "Pierre-Louis Curien" "Categorical Combinators, Sequential Algorithms and Functional Programming" "Pitman, London" "1986" "Michael J. O'Donnell" "Equational Logic as a Programming Language" "MIT Press" "1985" "Robert Kowalski" "Logic for Problem Solving" "North-Holand" "1979" "Michael J. O'Donnell" "Computing in Systems Described by Equations" "Springer-Verlag LNCS 58" "1977" "Joseph R. Shoenfield" "Degrees of Unsolvability" "North-Holland" "1971" "M. Barr" "C. Wells" "Toposes, Triples and Theories" "Springer-Verlag" "1985" "Peter Johnstone" "Topos Theory" "Academic Press" "1977" "J. R. Hindley" "J. P. Seldin" "Introduction to Combinators and $lambda$-Calculus" "Cambridge UP" "1986" "J. Barwise" "S. Feferman (eds.)" "Model-Theoretic Logics" "Springer-Verlag" "1985" "J. Lambek" "P. J. Scott" "Introduction to Higher Order Categorical Logic" "Cambridge Univ. Press" "1986" "G. M. Kelly" "Basic Concepts of Enriched Category Theory" "Cambridge Univ. Press" "1982" "Michael J. O'Donnell" "Equational Logic as a Programming Language" "MIT Press" "1985" "Maurice Nivat" "On the Interpretation of Recursive Program Schemes" "Symposia Mathematica" "1975" "XV" "225-281" "Instituto di Alta Matematica, Bologna, Italy, Academic Press" "Glynn Winskel" "Petri Nets, Algebras, Morphisms and Compositionality" "Info and Co" "1987" "72" "197-238" "From {Petri} nets to linear logic through categories: a survey" "Narciso Mart'i-Oliet" "Jos'e Meseguer" "1991" "2" "4" "297-399" "Intl. J. of Foundations of Comp. Sci." "Ross Street" "Limits Indexed by Category-Valued 2-Functors" "J. Pure Appl. Algebra" "1976" "8" "149-181" "J.-C. Raoult" "On Graph Rewritings" "Theoretical Computer Science" "1984" "32" "1-24" "E. W. Stark" "Concurrent Transition Systems" "Theoretical Computer Science" "1989" "64" "221-269" "J.-C. Raoult" "J. Vuillemin" "Operational and semantic equivalence between recursive programs" "J. ACM" "1980" "27" "772-796" "Y. Lafont" "The linear abstract machine" "Theoretical Computer Science" "1988" "59" "157-180" "N. Dershowitz" "M. Okada" "A rationale for conditional equational programming" "Theoretical Computer Science" "1990" "75" "111-138" "Steffen H{\"o}ldobler" "Conditional equational theories and complete sets of transformations" "Theoretical Computer Science" "1990" "75" "85-110" "R. Kennaway" "On ``On Graph Rewritings''" "Theoretical Computer Science" "1987" "52" "37-58" "M. Bauderon" "B. Courcelle" "Graph Expressions and Graph Rewriting" "Math. Systems Theory" "1987" "20" "83-127" "D. Janssens" "G. Rozenberg" "Actor Grammars" "Math. Systems Theory" "1989" "22" "75-107" "J. A. Goguen" "Reusing and Interconnecting Software Components" "Computer" "1986" "19" "2" "February" "16-28" "W. Athas" "C. Seitz" "Multicomputers: Message-Passing Concurrent Computers" "Computer" "1988" "August" "9-24" "J. A. Goguen" "M. Moriconi" "Formalization in Programming Environments" "Computer" "1987" "20" "11" "November" "55-64" "G. Cousineau" "P.-L. Curien" "M. Mauny" "The Categorical Abstract Machine" "Science of Computer Programming" "1987" "8" "173-202" "J.-P. Ban^{a}tre" "D. Le M`{e}tayer" "The {Gamma} model and its discipline of programming" "Science of Computer Programming" "1990" "15" "55-77" "J.-P. Ban^{a}tre" "A. Coutant" "D. Le M`{e}tayer" "Parallel machines for multiset transformation and their programming style" "Informationstechnik {\bf it}" "1988" "30" "2" "99-109" "J. Cartmell" "Generalised Algebraic Theories and Contextual Categories" "Annals Pure Appl. Logic" "1986" "32" "209-243" "J. A. Goguen" "Modular Algebraic Specification of Some Basic Geometrical Constructions" "Artificial Intelligence" "1988" "37" "123-153" "Jos'e Meseguer" "Order Completion Monads" "Algebra Universalis" "1983" "16" "63-82" "T. Coquand" "G. Huet" "The Calculus of Constructions" "Information and Computation" "1988" "76" "95-120" "Donald Sannella" "Andrzej Tarlecki" "Specifications in an Arbitrary Institution" "Information and Computation" "1988" "76" "165-210" "J. Meseguer" "Universe Models and Initial Model Semantics for the Second Order Polymorphic Lambda Calculus" "Abstracts of the AMS" "1988" "August" "338" "Also appeared as a communication in the {em Types} electronic forum (types@theory.lcs.mit.edu), April 13 1988" "L. Henkin" "Completeness in the Theory of Types" "J. Symbolic Logic" "1950" "15" "81-91" "P. Freyd" "Aspects of Topoi" "Bull. Austral. Math. Soc." "1972" "7" "1-76" "Wolfgang K{\"u}hnel" "Jos'e Meseguer" "Michael Pfender" "Ignacio Sols" "Primitive recursive algebraic theories and program schemes" "Bull. Austral. Math. Soc." "1977" "17" "207-233" "Wolfgang K{\"u}hnel" "Jos'e Meseguer" "Michael Pfender" "Ignacio Sols" "Algebras with actions and automata" "Int. J. Math. and Math. Sci." "1982" "5" "61-85" "J. McCarthy" "Circumscription--{A} Form of Non-Monotonic Reasoning" "Artificial Intelligence" "1980" "13" "27-39" "J. Siekmann" "P. Szab'o" "A {Noetherian} and confluent rewrite system for idempotent semigroups" "Semigroup Forum" "1982" "25" "83-110" "Alexander Herold" "J{\"{o}}rg H. Siekmann" "Unification in Abelian Semigroups" "J. Automated Reasoning" "1987" "3" "247-283" "K. J. Barwise" "Axioms for Abstract Model Theory" "Ann. Math. Logic" "1974" "7" "221-265" "J. Meseguer" "Universe Models and Initial Model Semantics for the Second Order Polymorphic Lambda Calculus" "Abstracts Amer. Math. Soc." "1988" "August" "Robin Milner" "Lectures on a Calculus for Communicating Systems" "Control Flow and Data Flow: Concepts of Distributed Programming" "Springer NATO ASI Series F, vol. 14" "1985" "M. Broy" "205-228" "Jos'e Meseguer" "Research Directions in Rewriting Logic" "Computational Logic, NATO Advanced Study Institute, Marktoberdorf, Germany, July 29 -- August 6, 1997" "Springer-Verlag" "1999" "U. Berger" "H. Schwichtenberg" "Architectural design of the rewrite rule machine ensemble" "Hitoshi Aida" "Sany Leinwand" "Jos'{e} Meseguer" "{VLSI} for {Artificial} {Intelligence} and {Neural} {Networks}" "Plenum Publ. Co." "1991" "J. Delgado-{Frias}" "W. R. Moore" "11-22" "Proceedings of an International Workshop held in {Oxford}, England, {September} 1990" "Francis William Lawvere" "Qualitative Distinctions Between Some Toposes of Generalized Graphs" "Proc. AMS Summer Research Conference on Categories in Computer Science and Logic, Boulder, Colorado, June 1987" "J. Gray" "AMS" "1988" "Francis William Lawvere" "Quantifiers and Sheaves" "Actes Congr`{e}s Intl. Math. (Nice 1970), vol. 1" "Gauthier-Villars" "1971" "329-334" "David Park" "Concurrency and Automata on Infinite Sequences" "Proc. Theoretical Computer Science" "Springer LNCS 104" "1981" "P. Deussen" "167-183" "Joseph Goguen" "An Algebraic Approach to Refinement" "Proc. {VDM}'90" "Springer LNCS 428" "1990" "D. Bjorner" "C. A. R. Hoare" "H. Langmaack" "11-28" "A. Sernadas" "J. Fiadeiro" "C. Sernadas" "H.-D. Ehrich" "Abstract Object Types: {A} Temporal Perspective" "Temporal Logic in Specification" "Springer LNCS 398" "1989" "B. Banieqbal" "H. Barringer" "A. Pnueli" "324-350" "K. Ueda" "Guarded Horn Clauses" "Logic Programming" "Springer LNCS 221" "1986" "E. Wada" "168-179" "D. Scott" "Completeness and Axiomatizability in Many-Valued Logic" "Proc. Tarski Symp." "AMS" "1974" "L. Henkin et al." "411-435" "A. Tarski" "On Some Fundamental Concepts of Metamathematics" "Logic, Semantics, Metamathematics" "Oxford U.P." "1956" "30-37" "J. Meseguer" "General Logics" "Logic Colloquium'87" "1989" "H.-D. Ebbinghaus et al." "North-Holland" "275-329" "G. Longo" "Some Aspects of Impredicativity" "Proc. Logic Colloquium'87" "North-Holland" "M. Garrido" "To appear. Also, Carnegie-Mellon Report CMU-CS-88-135" "1988" "Pierpaolo Degano" "Rocco De Nicola" "Ugo Montanari" "Observational Equivalences for Concurrency Models" "Proc. IFIP TC2 Workshop on Formal Description of Programming Concepts IV" "North-Holland" "1987" "M. Wirsing" "To appear." "Pierpaolo Degano" "Ugo Montanari" "Concurrent Histories: {A} Basis for Observing Distributed Systems" "Journal of Computer and System Sciences" "1987" "34" "2/3" "422-461" "April/June" "Andrzej Tarlecki" "Quasi-varieties in Abstract Algebraic Institutions" "Journal of Computer and System Sciences" "1986" "33" "333-360" "F. W. Lawvere" "Adjointness in Foundations" "Dialectica" "1969" "23" "3/4" "281-296" "Ilaria Castellani" "Paola Franceschi" "Ugo Montanari" "Labelled Event Structures: {A} Model for Observable Concurrency" "Proc. IFIP TC2 Workshop on Formal Description of Programming Concepts III" "North-Holland" "1983" "D. Bjo rner" "383-400" "Ilaria Castellani" "Bisimulation and Abstraction Homomorphisms" "Proc. TAPSOFT Conference, Berlin" "Springer LNCS 185" "1985" "H. Ehrig" "C. Floyd" "M. Nivat" "J. Thatcher" "223-238" "Also to appear in JCSS" "M. T. Sanderson" "Proof Techniques for {CCS}" "Computer Science Department, University of Edinburgh" "1982" "Technical Report CST-19-82" "Gert Smolka" "Logic programming over polymorphic order-sorted types" "Computer Science Department, University of Kaiserslautern" "1989" "Vijay Saraswat" "Concurrent constraint programming languages" "Computer Science Department, Carnegie-Mellon University" "1989" "G. Sivakumar" "Proofs and Computations in Conditional Equational Theories" "CS Dept., U. Illinois at Urbana" "1989" "Valeria C. V. de Paiva" "The Dialectica Categories" "Mathematics Department, University of Cambridge" "1988" "P. Taylor" "Recursive Domains, Indexed Category Theory and Polymorphism" "Mathematics Department, University of Cambridge" "1987" "N. McCracken" "An Investigation of a Programming Language with a Polymorphic Type Structure" "Syracuse University" "1979" "D. McCarty" "Realizabity and Recursive Mathematics" "Oxford University" "1984" "G'{e}rard Boudol" "Ilaria Castellani" "On the semantics of concurrency: partial orders and transition systems" "TAPSOFT '87" "1987" "H. Ehrig et al." "123-137" "Springer" "G'{e}rard Boudol" "Towards a lambda calculus for concurrent and communicating systems" "TAPSOFT '89" "1989" "149-161" "Springer LNCS Vol. 351" "Pierpaolo Degano" "Rocco De Nicola" "Ugo Montanari" "A distributed operational semantics for {CCS} based on condition/event systems" "IEI-CNR" "1987" "Nota Interna" "B4-21" "Pisa" "September" "Roberto Amadio" "Formal theories of inheritance for typed functional languages" "University of Pisa, Comp. Sci. Dept." "1989" "TR-28/89" "July" "Robin Milner" "Calculi for Synchrony and Asynchrony" "C.S. Dept, U. Edinburgh" "1982" "CSR-104-82" "February" "J. A. Makowski" "Why {Horn} Formulas Matter in Computer Science: Initial Structures and Generic Examples" "C.S. Dept, Technion" "1984" "329" "July" "Narciso Mart'i-Oliet" "Jos'{e} Meseguer" "From {Petri} Nets to Linear Logic" "D. H. Pitt et al." "Category Theory and Computer Science" "1989" "313-340" "Springer LNCS 389" "Final version in {it Mathematical Structures in Computer Science}, 1:69-101, 1991" "Narciso Mart'i-Oliet" "Jos'{e} Meseguer" "From {Petri} Nets to Linear Logic" "Math. Struct. in Comp. Sci." "1991" "69-101" "1" "H.-J. Kreowski" "T. Mossakowski" "Equivalence and difference between institutions: simulating {Horn Clause Logic} with based algebras" "Math. Struct. in Comp. Sci." "1995" "189-215" "5" "Luca Cardelli" "John Mitchell" "Operations on records" "Math. Struct. in Comp. Sci." "1991" "3-48" "1" "A. J. Power" "An abstract formulation of rewrite systems" "D. H. Pitt et al." "Category Theory and Computer Science" "1989" "300-312" "Springer LNCS, Vol. 389" "A. Pitts" "An Elementary Calculus of Approximations" "Unpublished manuscript, University of Sussex, December 1987" "Jos'{e} Meseguer" "The Category of Commutations of {$Sigma$}-Term Rewriting Systems" "Unpublished manuscript, SRI International, December 1987" "Ross Casley" "Roger Crew" "Jos'{e} Meseguer" "Vaughan Pratt" "Temporal Structures" "D. H. Pitt et al." "Category Theory and Computer Science" "1989" "21-51" "Springer LNCS, Vol. 389" "H. Aida" "J. A. Goguen" "S. Leinwand" "J. Meseguer" "T. Winkler" "The Rewrite Rule Machine" "Computer Science Laboratory, SRI International" "1989" "SRI-CSL-89-6" "March" "Jos'{e} Meseguer" "Relating Models of Polymorphism" "C.S. Lab., SRI International" "1988" "SRI-CSL-TN88-1" "June" "Jos'{e} Meseguer" "Ugo Montanari" "Petri Nets Are Monoids: {A} New Algebraic Foundation for Net Theory" "Proc. LICS'88" "1988" "155-164" "IEEE" "Claude March'e" "Normalised rewriting and normalised completion" "Proc. LICS'94" "1994" "394-403" "IEEE" "Tobias Nipkow" "Functional unification of higher-order patterns" "Proc. LICS'93" "1993" "64-74" "IEEE" "V. Breazu-Tannen" "T. Coquand" "C. A. Gunter" "A. Scedrov" "Inheritance and Explicit Coercion" "Proc. LICS'89" "1989" "112-129" "IEEE" "P. Degano" "J. Meseguer" "U. Montanari" "Axiomatizing Net Computations and Processes" "Proc. LICS'89" "1989" "175-185" "IEEE" "R. Harper" "D. Sannella" "A. Tarlecki" "Structure and Representation in {LF}" "Proc. LICS'89" "1989" "226-237" "IEEE" "Mitchell Wand" "Type Inference for Record Concatenation and Multiple Inheritance" "Proc. LICS'89" "1989" "92-97" "IEEE" "T. Coquand" "Categories of Embeddings" "Proc. LICS'88" "1988" "256-263" "IEEE" "R. Amadio" "K. B. Bruce" "G. Longo" "The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain Equations" "Proc. LICS'86" "1986" "122-130" "IEEE" "P. J. Freyd" "J.-Y. Girard" "A. Scedrov" "P. J. Scott" "Semantic Parametricity in Polymorphic Lambda Calculus" "Proc. LICS'88" "1988" "274-279" "IEEE" "Rob van Glabbeek" "Frits Vaandrager" "Petri net models for algebraic theories of concurrency" "PARLE Conference" "1987" "J. W. de Bakker et al." "" "Springer LNCS 259" "Ernst-R{\"{u}}diger Olderog" "Operational Petri net semantics for {CCSP}" "Advances in Petri Nets 1987" "1987" "G. Rozenberg" "196-223" "" "Springer LNCS 266" "Glynn Winskel" "Categories of Models for Concurrency" "Workshop on the semantics of concurrency" "1984" "S. Brooks" "July" "Glynn Winskel" "Event structures" "University of Cambridge Computer Laboratory" "1986" "Technical Report" "95" "July" "Pierpaolo Degano" "Ugo Montanari" "Specification languages for distributed systems" "TAPSOFT" "1985" "H Ehrig et al." "29-51" "Springer LNCS 185" "Saunders MacLane" "Categories for the Working Mathematician" "Springer-Verlag" "1971" "C. A. R. Hoare" "Communicating Sequential Processes" "Prentice Hall" "1985" "S. Y. Kung" "{VLSI} Processor Arrays" "Prentice Hall" "1988" "Ian Foster" "Stephen Taylor" "Strand: New Concepts in Parallel Programming" "Prentice Hall" "1990" "Robin Milner" "Communication and Concurrency" "Prentice Hall" "1989" "Simon Peyton-Jones" "The Implementation of Functional Programming Languages" "Prentice Hall" "1987" "Herrlich" "Strecker" "Category theory" "Allyn and Bacon" "1973" "Saunders MacLane" "Garrett Birkhoff" "Algebra" "Mac Millan" "1967" "E. Manes" "Algebraic theories" "Springer" "1976" "26" "Graduate Texts in Mathematics" "S. Eilenberg" "J. C. Moore" "Adjoint functors and triples" "Illinois J. Math." "1965" "9" "381-398" "Kim Bruce" "Giuseppe Longo" "A Modest Model of Records, Inheritance and Bounded Quantification" "Information and Computation" "1990" "87" "196-240" "Robin Milner" "Functions as Processes" "Mathematical Structures in Computer Science" "1992" "2" "2" "119-141" "Jos'e Meseguer" "Ugo Montanari" "Vladimiro Sassone" "On the semantics of place/transition {P}etri nets" "Mathematical Structures in Computer Science" "1997" "7" "4" "359-397" "Joseph Goguen" "A Categorical Manifesto" "Mathematical Structures in Computer Science" "1991" "1" "1" "49-67" "Ross Casley" "Roger Crew" "Jos'{e} Meseguer" "Vaughan Pratt" "Temporal Structures" "Mathematical Structures in Computer Science" "1991" "1" "2" "179-213" "Joseph Goguen" "Sheaf semantics for concurrent interacting objects" "Mathematical Structures in Computer Science" "1992" "2" "2" "159-191" "Ross Cassley" "Roger Crew" "Jos'{e} Meseguer" "Vaughan Pratt" "Temporal Structures" "J. Math. Structures in Computer Science" "1991" "1" "2" "179-213" "V. R. Pratt" "Modelling Concurrency with Partial Orders" "Intl. J. Parallel Programming" "1986" "15" "33-71" "F. E. J. Linton" "Autonomous Equational Categories" "J. of Mathematics and Mechanics" "1966" "15" "637-642" "Anders Kock" "Closed categories generated by commutative monads" "J. Australian Math. Soc." "1971" "12" "405-424" "Joseph Goguen" "Claude Kirchner" "Jos'{e} Meseguer" "Concurrent term rewriting as a model of computation" "Proc. Workshop on Graph Reduction, Santa Fe, New Mexico" "1987" "R. Keller" "J. Fasel" "53-93" "Springer LNCS 279" "P. G. Harrison" "M. J. Reeve" "The Parallel Graph Reduction Machine, {Alice}" "Proc. Workshop on graph reduction, Santa Fe, New Mexico" "1987" "R. Keller" "J. Fasel" "181-202" "Springer LNCS 279" "Order-Sorted Unification" "Jos'{e} Meseguer" "Joseph Goguen" "Gert Smolka" "To appear in the {it Journal of Symbolic Computation}, special issue on unification" "T. Naoi" "Y. Inagaki" "Algebraic Semantics of Term Rewriting Systems" "Comp86, pp. 1-10" "Jos'{e} Meseguer" "Lectures on Algebraic Data Types" "ASL-CSLI Summer School on Logic, Language and Computation, Stanford, July 1985" "Luca Cardelli" "John Mitchell" "Semantic Methods for Object-Oriented Languages, Part 2" "Tutorial at OOPSLA'88" "Jean-Yves Girard" "Towards a Geometry of Interaction" "{Proc. AMS Summer Research Conference on Categories in Computer Science and Logic, Boulder, Colorado, June 1987}" "1989" "69-108" "J. W. Gray" "A. Scedrov" "American Mathematical Society" "Jean-Yves Girard" "Geometry of Interaction {III}: the general case" "{Proc. Workshop on Linear Logic}" "1994" "To appear in MIT Press" "A. M. Pitts" "P. Taylor" "A note on {Russell's} Paradox in Locally Cartesian Closed Categories" "1987" "University of Sussex" "P. Taylor" "Stable Categories form a Cartesian Closed Category" "1988" "Dept. of Computing, Imperial College" "F. W. Lawvere" "Skolem Categories" "Unpublished Seminar Lectures at University of Buffalo. Fall of 1974" "A. Asperti" "G. Longo" "Categories for Denotational Semantics" "To appear" "A. Asperti" "A logic for concurrency" "Unpublished manuscript, November 1987" "Edmund Robinson" "How complete is {PER}?" "Queen's University, Department of Computing and Information Science" "1988" "88-229" "Carl Gunter" "Vijay Gehlot" "Nets as Tensor Theories" "Dept. of Computer and Information Science, University of Pennsylvania" "1989" "MS-CIS-89-68" "Edmund Robinson" "Personal Communication" "July 1988" "G. Hotz" "Eine Algebraisierung des Syntheseproblemen von Schaltkreisen, {I} and {II}" "EIK" "1965" "1" "185--206, 209--231" "A. Kock" "Bilinearity and Cartesian Closed Monads" "Math. Scand." "1971" "29" "161-174" "Jos'{e} Meseguer" "Ignacio Sols" "Automata in semimodule categories" "Category Theory Applied to Computation and Control" "Springer LNCS 25" "1975" "E. G. Manes" "193-198" "David B. Benson" "The basic algebraic structures in categories of derivations" "Info. and Co." "1975" "28" "1-29" "Michael G. Main" "David B. Benson" "Functional behaviour of nondeterministic and concurrent programs" "Info. and Co." "1984" "62" "144-189" "Wolfgang Hinderer" "Transfer of graph constructs in Goguen's paper to net constructs" "Application and Theory of Petri Nets" "Springer Informatik-Fachberichte 52" "1982" "Claude Girault" "Wolfgang Reisig" "142-150" "W. M. P. van der Aalst" "Interval timed coloured {Petri} nets and their analysis" "Application and Theory of Petri Nets 1993" "Springer LNCS 691" "1993" "M. Ajmone Marsan" "453-472" "Carl Adam Petri" "Concepts of net theory" "Mathematical Foundations of Computer Science" "1973" "137-146" "Mathematical Institute of the Slovak Academy of Sciences" "Stefan Drees" "Dominik Gomm" "Helmut Pl{\"{u}}nnecke" "Wolfgang Reisig" "Rolf Walter" "Bibliography of Net Theory" "Gesellschaft f{\"{u}}r Mathematik und Datenverarbeitung MBH" "1986" "Arbeitspapiere der GMD" "212" "V. Breazu-Tannen" "A. R. Meyer" "Computable values can be classical" "{Proceedings of the 14th Symposium on Principles of Programming Languages}" "ACM" "238-245" "January" "1987" "V. Breazu-Tannen" "Conservative extensions of type theories" "MIT" "February" "1987" "Supervised by A. R. Meyer" "V. Breazu-Tannen" "T. Coquand" "Extensional models for polymorphism" "{Proceedings of TAPSOFT - Colloquium on Functional and Logic Programming and Specifications, Pisa, March 1987}" "LNCS, Vol. 250, Springer-Verlag" "291-307" "1987" "An expanded version will appear in the special issue of {em Theoretical Computer Science} dedicated to the colloquium" "V. Breazu-Tannen" "A. R. Meyer" "Polymorphism is conservative over simple types" "{Proceedings of the Symposium on Logic in Computer Science}" "IEEE" "June" "1987" "7-17" "L. Bachmair" "N. Dershowitz" "J. Hsiang" "Orderings for Equational Proofs" "{Proceedings of the Symposium on Logic in Computer Science}" "IEEE" "June" "1986" "346-357" "Joseph Goguen" "Jos'{e} Meseguer" "Software for the Rewrite Rule Machine" "Proceedings of the International Conference on Fifth Generation Computer Systems, Tokyo, Japan" "ICOT" "1988" "628-637" "Hideyuki Nakashima" "Hiroyuki Suzuki" "Per-Kristian Halvorsen" "Stanley Peters" "Towards a Computational Interpretation of Situation Theory" "Proceedings of the International Conference on Fifth Generation Computer Systems, Tokyo, Japan" "ICOT" "1988" "489-498" "S. Leinwand" "J. A. Goguen" "T. Winkler" "Cell and Ensemble Architecture for the Rewrite Rule Machine" "Proceedings of the International Conference on Fifth Generation Computer Systems, Tokyo, Japan" "ICOT" "1988" "869-878" "V. Breazu-Tannen" "Proof of a conjecture on polymorphic lambda models with all types non-empty" "Manuscript, Univ. of Pennsylvania, 1987" "V. Breazu-Tannen" "Combining algebra and higher-order types" "{Proceedings of the Symposium on Logic in Computer Science}" "IEEE" "July" "1988" "To appear" "A. Carboni" "P. J. Freyd" "A. Scedrov" "{A Categorical Approach to Realizability and Polymorphic Types}" "{Mathematical Foundations of Programming Language Semantics}" "April" "1987" "M. Main" "A. Melton" "Springer LNCS" "T. Coquand" "C. A. Gunter" "Glynn Winskel" "{dI-domains as a Model of Polymorphism}" "{Mathematical Foundations of Programming Language Semantics}" "April" "1987" "M. Main" "A. Melton" "Springer LNCS" "P. J. Freyd" "A. Scedrov" "{Some Semantic Aspects of Polymorphic Lambda Calculus}" "{Second IEEE Symposium on Logic in Computer Science}" "June" "1987" "D. Gries" "315-319" "IEEE Computer Society" "R. Seely" "Modelling computations: a 2-categorical framework" "{Second IEEE Symposium on Logic in Computer Science}" "June" "1987" "D. Gries" "65-71" "IEEE Computer Society" "P. J. Freyd" "J. Y. Girard" "A. Scedrov" "P. J. Scott" "{Semantic Parametricity in Polymorphic Lambda Calculus}" "{Third IEEE Symposium on Logic in Computer Science}" "July" "1988" "IEEE Computer Society" "P. Giannini" "G. Longo" "{Effectively Given Domains and Lambda Calculus Models}" "Information and Control" "1984" "62" "36-63" "Jean-Yves Girard" "Interpr'etation Fonctionelle et 'Elimination des Coupures dans l'Arithm'etique d'ordre Sup'erieure" "Univ. Paris VII" "1972" "Jean-Yves Girard" "{The System F of Variable Types, Fifteen Years Later}" "Theoretical Computer Science" "1986" "45" "159-192" "D. A. Schmidt" "{Approximation Properties of Abstract Data Types}" "Theoretical Computer Science" "1983" "24" "73-94" "Andrzej Tarlecki" "{On the Existence of Free Models in Abstract Algebraic Institutions}" "Theoretical Computer Science" "1985" "37" "269-304" "Jean-Yves Girard" "{Linear Logic}" "Theoretical Computer Science" "1987" "50" "1-102" "Jean-Yves Girard" "{Proof Theory and Logical Complexity}" "Bibliopolis" "1987" "C. A. Gunter" "{Sets and the Semantics of Bounded Non-Determinism}" "In preparation" "G. Huet" "{A Uniform Approach to Type Theory}" "{Logical Foundations of Functional Programming}" "June" "1987" "G. Huet" "Proceedings University of Texas Year of Programming" "J. M. E. Hyland" "E. Robinson" "G. Rosolini" "{Discrete Objects in the Effective Topos}" "Preprint" "1987" "J. M. E. Hyland" "A. Pitts" "The Theory of Constructions: Categorical Semantics and Topos-Theoretic Models" "{Proc. AMS Summer Research Conference on Categories in Computer Science and Logic, Boulder, Colorado, June 1987}" "1988" "J. W. Gray" "A. Scedrov" "137-199" "American Mathematical Society" "P. Martin-Loef" "{Intuitionistic Type Theory}" "Bibliopolis" "1984" "P. Martin-Loef" "{An Intuitionistic Theory of Types: Predicative Part}" "{Logic Colloquium'73}" "H. E. Rose" "J. C. Shepherdson" "Noth-Holland" "1973" "73-118" "J. C. Mitchell" "{Representation Independence and Data Abstraction}" "{13th ACM Symposium on Principles of Programming Languages}" "1986" "263-276" "J. C. Reynolds" "{Towards a Theory of Type Structure}" "{Programming Symposium}" "1974" "B. Robinet" "408-425" "Springer LNCS 19" "J. C. Reynolds" "{Types, Abstraction, and Parametric Polymorphism}" "{Information Processing '83}" "1983" "R. E. A. Mason" "513-523" "North-Holland" "G. Rosolini" "{Continuity and Effectiveness in Topoi}" "Oxford University" "{Doctoral Dissertation}" "1986" "A. Scedrov" "{Recursive Realizability Semantics for Calculus of Constructions}" "{Logical Foundations of Functional Programming}" "June" "1987" "G. Huet" "Proceedings University of Texas Year of Programming" "D. S. Scott" "{Data Types as Lattices}" "SIAM Journal of Computing" "1976" "5" "522-587" "Jos'e Meseguer" "Ir`ene Guessarian" "{On the axiomatization of if-then-else}" "SIAM Journal of Computing" "1987" "16" "332-357" "D. S. Scott" "{Domains for Denotational Semantics}" "{International Colloquium on Automata, Languages and Programs}" "1982" "M. Nielsen" "E. M. Schmidt" "577-613" "Springer LNCS 140" "D. S. Scott" "{Realizability and Domain Theory}" "Lecture at the AMS Conference on Categories in Computer Science and Logic" "June" "1987" "M. B. Smyth" "G. D. Plotkin" "{The Category-Theoretic Solution of Recursive Domain Equations}" "SIAM Journal of Computing" "1982" "11" "761-783" "A. S. Troelstra" "{Metamathematical Investigation of Intuitionistic Arithmetic and Analysis}" "Springer Lecture Notes in Mathematics 344" "1973" "N. McCracken" "The Type-Checking of Programs with Implicit Type Structure" "G. Kahn" "D. B. MacQueen" "G. Plotkin" "Proceedings of the Conference on Semantics of Data Types, Sophia-Antipolis, June 1984" "{em LNCS}, Vol. 173, Springer-Verlag" "301-315" "1984" "J. C. Mitchell" "Type Inference and Type Containment" "G. Kahn" "D. B. MacQueen" "G. Plotkin" "Proceedings of the Conference on Semantics of Datan Types, Sophia-Antipolis, June 1984" "{em LNCS}, Vol. 173, Springer-Verlag" "257-277" "1984" "R. L. Constable" "{Implementing Mathematics with the Nuprl Proof Development System}" "Prentice Hall" "1987" "E. Moggi" "Communication in the {sc Types} electronic forum (types@theory.lcs.mit.edu), {February 10, 1986}" "A. M. Pitts" "An extension of {Reynolds'} result on the non-existence of set-models of polymorphism" "Communication in the {it Types} electronic forum (types@theory.lcs.mit.edu), {May 29, 1988}" "H. Huwig" "A. Poign'{e}" "A note on inconsistencies caused by fixpoints in a cartesian closed category" "Manuscript, C.S. Dept., Univ. of Dortmund" "E. Moggi" "Communication in the {sc Types} electronic forum (types@theory.lcs.mit.edu), {July 23, 1986}" "D. S. Scott" "Relating theories of the lambda calculus" "To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism" "J. P. Seldin" "J. R. Hindley" "Academic Press" "1980" "403-450" "J.-J. L'{e}vy" "Optimal reductions in the lambda calculus" "159-191" "To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism" "J. P. Seldin" "J. R. Hindley" "Academic Press" "1980" "R. A. G. Seely" "Higher order polymorphic lambda calculus and categories" "Mathematical Reports, Academy of Science (Canada)" "{VIII}" "2" "1986" "135-139" "R. A. G. Seely" "Locally cartesian closed categories and type theory" "Math. Proc. Camb. Phil. Soc." "95" "1984" "33-48" "R. A. G. Seely" "Categorical semantics for higher order polymorphic lambda calculus" "J. Symbol. Logic" "52" "4" "1987" "969-989" "A. Boileau" "A. Joyal" "La Logique des Topos" "J. Symbol. Logic" "46" "1" "1981" "6-16" "J. M. E. Hyland" "A small complete category" "1987" "Manuscript, to appear in the proceedings of the Conference on Church's Thesis: Fifty Years Later" "A. Ohori" "P. Buneman" "OhoriBuneman" "{Type Inference in a Database Programming Language}" "University of Pennsylvania" "Technical report" "November" "1987" "J. Meseguer J. A. Goguen" "E. Munthe-Kaas." "{Object-Oriented Programming and Specification is a Natural Extension of Pure Functional Programming}" "SRI International" "Technical report" "To appear" "1989" "P. Buneman" "S. Davidson" "Watters A." "Buneman, Davidson & Watters" "{A Semantics for Complex Objects and Approximate Queries}" "Principles of Database Systems" "ACM" "March" "1988" "C. A. Gunter" "Profinite Solutions for Recursive Domain Equations" "University of Wisconsin at Madison" "1985" "{A Semantics of Multiple Inheritance}" "Luca Cardelli" "Semantics of Data Types, LNCS 173" "G. Kahn" "D. Mac{Queen}" "G. Plotkin" "Springer LNCS 173" "51-67" "1984" "{A Semantics of Multiple Inheritance}" "Luca Cardelli" "Information and Computation" "76" "138-164" "1988" "{Structural Subtyping and the Notion of Power Type}" "Luca Cardelli" "Proc. POPL'88" "ACM" "1988" "{Reflection and Semantics in {Lisp}}" "Brian C. Smith" "Proc. POPL'84" "23-35" "ACM" "1984" "Modeling concurrency with geometry" "Vaughan Pratt" "311-322" "Proc. POPL'91" "ACM" "1991" "Algorithmic aspects of type inference with subtypes" "Patrick Lincoln" "John Mitchell" "" "Proc. POPL'92" "ACM" "1992" "Coercion and type inference" "John Mitchell" "175-185" "Proc. POPL'84" "ACM" "1984" "{Relating Models of Polymorphism}" "Jos'e Meseguer" "Proc. POPL'89" "ACM" "228-241" "1989" "{Inheritance is not Subtyping}" "William Cook" "Walter Hill" "Peter Canning" "Proc. POPL'90" "ACM" "125-135" "1990" "{Toward a Typed Foundation for Method Specialization and Inheritance}" "John Mitchell" "Proc. POPL'90" "ACM" "109-124" "1990" "{Explicit Substitutions}" "M. Abadi" "L. Cardelli" "P.-L. Curien" "J.-J. L'evy" "Proc. POPL'90" "ACM" "31-46" "1990" "{Rewrite, Rewrite, Rewrite, Rewrite, Rewrite,...}" "N. Dershowitz" "S. Kaplan" "Proc. POPL'89" "ACM" "250-259" "1989" "{Empty Types in Polymorphic $lambda$ Calculus}" "A. R. Meyer" "J. R. Mitchell" "E. Moggi" "R. Statman" "Proc. POPL'87" "ACM" "253-262" "1987" "Luca Cardelli" "{A polymorphic $lambda$-calculus with Type:Type}" "DEC System Research Center" "Palo Alto, CA" "1986" "10" "Leslie Lamport" "{A Temporal Logic of Actions}" "DEC System Research Center" "Palo Alto, Ca" "1990" "Luca Cardelli" "{A Quest Preview}" "DEC System Research Center" "Palo Alto, Ca" "1988" "Luca Cardelli" "Giuseppe Longo" "{A semantic basis for {Quest}}" "DEC System Research Center" "Palo Alto, Ca" "55" "1990" "G. Winskel" "{On Powerdomains and Modalities}" "{Theoretical Computer Science}" "1985" "36" "127-137" "D. Miller" "A. Felty" "An Integretation of Resolution and Natural Deduction Theorem Proving" "Proceedings of the Fifth National Conference on Artificial Intelligence" "August" "1986" "D. Miller" "G. Nadathur" "A. Scedrov" "Hereditary Harrop Formulas and Uniform Proofs Systems" "{Second Annual Symposium on Logic in Computer Science}" "Cornell University" "June" "1987" "98-105" "Proving Properties of Programs by Structural Induction" "Rod Burstall" "1969" "Computer Journal" "12" "1" "41-48" "Putting Theories together to Make Specifications" "Rod Burstall" "Joseph Goguen" "Proceedings, Fifth International Joint Conference on Artificial Intelligence" "Raj Reddy" "Department of Computer Science, Carnegie-Mellon University" "1977" "1045-1058" "Rod Burstall" "Joseph A. Goguen" "The Semantics of {C}lear, a Specification Language" "Proceedings of the 1979 Copenhagen Winter School on Abstract Software Specification" "Dines Bjorner" "Springer LNCS 86" "292-332" "1980" "An Informal Introduction to Specifications using Clear" "Rod Burstall" "Joseph Goguen" "1981" "The Correctness Problem in Computer Science" "Robert Boyer" "J Moore" "Academic Press" "185-213" "Reprinted in {it Software Specification Techniques}, Narain Gehani and Andrew McGettrick, Eds., Addison-Wesley, 1985, pages 363-390" "Joseph Goguen" "Semantics of Computation" "1974" "Proceedings, First International Symposium on Category Theory Applied to Computation and Control" "Ernest G. Manes" "University of Massachusetts at Amherst" "234-249" "Also published in LNCS, Volume 25, Springer-Verlag, 1975, pages 151-163" "Some Remarks on Data Structures" "Joseph Goguen" "1973" "Abstract of 1973 Lectures at Eidgenoschiche Technische Hochschule, Zurich" "Mathematical Representation of Hierarchically Organized Systems" "Joseph Goguen" "1971" "E. Attinger" "Global Systems Dynamics" "S. Karger" "112-128" "A Categorical Approach to General Systems Theory" "Joseph Goguen" "Susanna Ginali" "1978" "Applied General Systems Research" "George Klir" "257-270" "Plenum" "Algebraic Denotational Semantics using Parameterized Abstract Modules" "Joseph Goguen" "Kamran Parsaye-Ghomi" "1981" "Formalizing Programming Concepts" "J. Diaz" "I. Ramos" "LNCS, Volume 107" "292-309" "Springer-Verlag" "The Specification and Application to Programming of Abstract Data Types" "John Guttag" "1975" "University of Toronto" "Computer Science Department, Report CSRG-59" "Abstract Data Types and the Development of Data Structures" "John Guttag" "Communications of the Association for Computing Machinery" "1977" "20" "June" "297-404" "Asynchronous Distributed Simulation via a Sequence of Parallel Computations" "K. M. Chandy" "J. Misra" "Communications of the Association for Computing Machinery" "1981" "24" "April" "198-206" "An Expert System for a Resource Allocation Problem" "J. R. Slagle" "H. Hamburger" "Communications of the Association for Computing Machinery" "1985" "28" "September" "994-1004" "Concurrent object-oriented programming" "G. Agha" "Communications of the Association for Computing Machinery" "1990" "33" "September" "125-141" "Linda in context" "N. Carriero" "D. Gelernter" "Communications of the Association for Computing Machinery" "1989" "32" "April" "444-458" "Parallel Discrete Event Simulation" "Richard M. Fujimoto" "Communications of the Association for Computing Machinery" "1990" "33" "October" "31-53" "Pascal User Manual and Report" "K. Jensen" "Niklaus Wirth" "1978" "Springer-Verlag" "second" "Order Sorted Algebra" "Joseph Goguen" "1978" "14" "UCLA Computer Science Department" "Semantics and Theory of Computation Series" "Abstract Errors for Abstract Data Types" "Joseph Goguen" "1977" "Proceedings of First IFIP Working Conference on Formal Description of Programming Concepts" "Peter Neuhold" "MIT" "21.1--21.32" "Also published in {it Formal Description of Programming Concepts}, Peter Neuhold, Ed., North-Holland, pages 491-522, 1979" "Concurrency issues in object-oriented programming languages" "M. Papathomas" "1989" "Object Oriented Development" "D. Tsichritzis" "Universit'e de Geneve" "207-246" "Reductive conditional term rewriting systems" "J.-P. Jouannaud" "B. Waldmann" "1986" "Proceedings of Third IFIP Working Conference on Formal Description of Programming Concepts" "Ebberup, Denmark" "Fair termination is decidable for ground systems" "Sophie Tison" "1989" "462-476" "Nachum Dershowitz" "Rewriting Techniques and Applications, Chappel Hill, North Carolina" "Springer LNCS 355" "Termination for the direct sum of term rewriting systems" "Y. Toyama" "J. W. Klop" "H. P. Barendregt" "1989" "477-491" "Nachum Dershowitz" "Rewriting Techniques and Applications, Chappel Hill, North Carolina, Springer LNCS No. 355" "H. Kaphengst" "Horst Reichel" "Initial Algebraic Semantics for Non-Context-Free Languages" "1977" "Fundamentals of Computation Theory" "Marek Karpinski" "LNCS, Volume 56" "Springer-Verlag" "120-126" "An Initial Algebra Approach to the Specification, Correctness and Implementation of Abstract Data Types" "Joseph Goguen" "James Thatcher" "Eric Wagner" "1976" "October" "IBM T. J. Watson Research Center" "RC 6487" "Appears in {it Current Trends in Programming Methodology, IV}, Raymond Yeh, editor, Prentice-Hall, 1978, pages 80-149" "Abstract Data Types as Initial Algebras and the Correctness of Data Representations" "Joseph Goguen" "James Thatcher" "Eric Wagner" "Jesse Wright" "1975" "Computer Graphics, Pattern Recognition and Data Structure" "Alan Klinger" "IEEE Press" "89-93" "Joseph Goguen" "James Thatcher" "Eric Wagner" "Jesse Wright" "Initial Algebra Semantics and Continuous Algebras" "Journal of the Association for Computing Machinery" "24" "1" "68-95" "January" "1977" "Computable Algebra: General Theory and Theory of Computable Fields" "Michael Rabin" "1960" "Transactions of the American Mathematical Society" "95" "341-360" "Ordinary Specification of Some Construction in Plane Geometry" "Joseph Goguen" "1982" "Proceedings, Workshop on Program Specification" "J{o}rgen Staunstrup" "Springer-Verlag" "31-46" "LNCS, Volume 134" "Institutions: Abstract Model Theory for Computer Science" "Joseph Goguen" "Rod Burstall" "1985" "Center for the Study of Language and Information, Stanford University" "{CSLI}-85-30" "Also submitted for publication" "Universal Realization, Persistent Interconnection and Implementation of Abstract Modules" "Joseph Goguen" "Jos'{e} Meseguer" "1982" "Proceedings, 9th International Conference on Automata, Languages and Programming" "265-281" "M. Nielsen" "E. M. Schmidt" "Springer LNCS 140" "Infinite Normal Forms" "Nachum Dershowitz" "Stephan Kaplan" "David Plaisted" "1989" "Proceedings, 16th International Conference on Automata, Languages and Programming" "249-262" "G. Ausiello" "M. Dezani-Ciancaglini" "S. Ronchi Della Rocca" "Springer-Verlag" "LNCS, Volume 372" "Models and Equality for Logical Programming" "Joseph Goguen" "Jos'e Meseguer" "Proceedings TAPSOFT'87" "H. Ehrig" "G. Levi" "R. Kowalski" "U. Montanari" "1987" "Springer-Verlag" "1-22" "250" "Lecture Notes in Computer Science" "Eqlog: Equality, Types, and Generic Modules for Logic Programming" "Joseph Goguen" "Jos'{e} Meseguer" "Logic Programming: Functions, Relations and Equations" "Douglas DeGroot" "Gary Lindstrom" "1986" "Prentice-Hall" "295-363" "Joseph Goguen" "Jos'{e} Meseguer" "Equality, Types, Modules and (Why Not?) Generics for Logic Programming" "Journal of Logic Programming" "1" "2" "1984" "179-210" "Specification Language {Z}" "Jean-Raymond Abrial" "S. A. Schuman" "Bertrand Meyer" "1979" "Massachusetts Computer Associates" "Unifying Functional, Object-Oriented and Relational Programming with Logical Semantics" "Joseph Goguen" "Jos'{e} Meseguer" "Research Directions in Object-Oriented Programming" "Bruce Shriver" "Peter Wegner" "1987" "417-477" "MIT Press" "Order-Sorted Algebra Solves the Constructor Selector, Multiple Representation and Coercion Problems" "Joseph Goguen" "Jos'{e} Meseguer" "Proceedings, Second Symposium on Logic in Computer Science" "1987" "18-29" "IEEE Computer Society Press" "Extended version to appear in {it Information and Computation}" "A Framework for Defining Logics" "R. Harper" "F. Honsell" "G. Plotkin" "Proceedings, Second Symposium on Logic in Computer Science" "1987" "194-204" "IEEE Computer Society Press" "How to Prove Algebraic Inductive Hypotheses without Induction: with Applications to the Correctness of Data Type Representations" "Joseph Goguen" "1980" "Proceedings, Fifth Conference on Automated Deduction" "Springer-Verlag" "LNCS, Volume 87" "Wolfgang Bibel" "Robert Kowalski" "356-373" "Canonical Forms and Unification" "Jean-Marie Hullot" "1980" "Proceedings, Fifth Conference on Automated Deduction" "Springer-Verlag" "LNCS, Volume 87" "Wolfgang Bibel" "Robert Kowalski" "318-334" "{OBJ} as a Language for Concurrent Programming" "Joseph Goguen" "Claude Kirchner" "Jos'{e} Meseguer" "Timothy Winkler" "Proceedings, Second International Supercomputing Conference, Volume I" "Steven Kartashev" "Svetlana Kartashev" "International Supercomputing Institute, Inc." "1987" "195-198" "Simulation of Concurrent Term Rewriting" "Timothy Winkler" "Sany Leinwand" "Joseph Goguen" "Proceedings, Second International Supercomputing Conference, Volume I" "Steven Kartashev" "Svetlana Kartashev" "International Supercomputing Institute, Inc." "1987" "199-208" "Architectural Options for the Rewrite Rule Machine" "Sany Leinwand" "Joseph Goguen" "Proceedings, Second International Supercomputing Conference, Volume I" "Steven Kartashev" "Svetlana Kartashev" "International Supercomputing Institute, Inc." "1987" "63-70" "Graphical Programming by Generic Example" "Joseph Goguen" "Proceedings, Second International Supercomputing Conference, Volume I" "Steven Kartashev" "Svetlana Kartashev" "International Supercomputing Institute, Inc." "1987" "209-216" "Larch in Five Easy Pieces" "John Guttag" "James Horning" "Jeanette Wing" "Digital Equipment Corporation, Systems Research Center" "5" "1985" "July" "Mobile ambients" "L. Cardelli" "A. D. Gordon" "Digital Equipment Corporation, Systems Research Center" "1997" "Progress Report on the Rewrite Rule Machine" "Joseph Goguen" "Claude Kirchner" "Sany Leinwand" "Jos'{e} Meseguer" "Timothy Winkler" "1986" "{IEEE} Computer Architecture Technical Committee Newsletter" "March" "7-21" "Compiling Pattern-Matching" "Lennart Augustsson" "University of GH{o}teborg, Programming Methodology Group" "25" "September" "1986" "Epsilon-Reduction: Another View of Unification" "Klaus Berkling" "Syracuse University" "1986" "Can Programming be Liberated from the von Neumann Style?" "John Backus" "1978" "Communications of the Association for Computing Machinery" "21" "8" "613-641" "Operational Semantics of Order-Sorted Algebra" "Joseph Goguen" "Jean-Pierre Jouannaud" "Jos'{e} Meseguer" "1985" "221-231" "Proceedings, 1985 International Conference on Automata, Languages and Programming" "W. Brauer" "194" "Lecture Notes in Computer Science" "Springer-Verlag" "Equations and Rewrite Rules: {A} Survey" "G'{e}rard Huet" "Derek Oppen" "1980" "Formal Language Theory: Perspectives and Open Problems" "Ron Book" "Academic Press" "Initiality, Induction and Computability" "Jos'{e} Meseguer" "Joseph Goguen" "Algebraic Methods in Semantics" "Maurice Nivat" "John Reynolds" "Cambridge University Press" "1985" "459-541" "Computational semantics of term rewriting systems" "G. Boudol" "Algebraic Methods in Semantics" "Maurice Nivat" "John Reynolds" "Cambridge University Press" "1985" "169-236" "Deduction with Many-Sorted Rewrite Rules" "Jos'{e} Meseguer" "Joseph Goguen" "1985" "December" "Center for the Study of Language and Information, Stanford University" "{CSLI}-85-42" "Resource Control in a Demand-Driven Data-Flow Model" "Bharadwaj Jayaraman" "Robert Keller" "1980" "{IEEE C}onference on Parallel Processing" "August" "" "118-127" "Rediflow Multiprocessing" "Robert Keller" "F. C. H. Lin" "J. Tanaka" "1984" "{IEEE C}ompcon" "February" "" "410-417" "A Loosely-Coupled Applicative Multi-Processing System" "Robert Keller" "Gary Lindstrom" "S. Patil" "1979" "{AFIPS} Conference Proceedings" "June" "" "613-622" "Cynthia Dwork" "Paris Kanellakis" "Larry Stockmeyer" "Parallel Algorithms for Term Matching" "1986" "{MIT}" "Cynthia Dwork" "Paris Kanellakis" "John Mitchell" "On the Sequential Nature of Unification" "Journal of Logic Programming" "1" "1" "1984" "35-50" "{MIT}" "Laurent Fribourg" "Oriented Equational Clauses as a Programming Language" "Journal of Logic Programming" "1" "2" "1984" "179-210" "Computations in Non-ambiguous Linear Term Rewriting Systems" "G'{e}rard Huet" "Jean-Jacques Levy" "{INRIA L}aboria" "1979" "Computational Semantics of Term Rewriting Systems" "G'{e}rard Boudol" "Algebraic Methods in Semantics" "Maurice Nivat" "John Reynolds" "Cambridge University Press" "1985" "169-236" "M. Bauderon" "Bruno Courcelle" "Graph expressions and graph rewritings" "1985" "Universit'{e} de Bordeaux 1" "Completion of a Set of Rules Modulo a Set of Equations" "Jean-Pierre Jouannaud" "helene Kirchner" "1984" "Proceedings 11th ACM Symposium on Principles of Programming Languages" "To appear in {it {SIAM J}ournal of Computing}" "Completion of a Set of Rules Modulo a Set of Equations" "Jean-Pierre Jouannaud" "helene Kirchner" "1986" "November" "{SIAM} {Journal} of {Computing}" "15" "1155-1194" "Lazy Memo-Functions" "John Hughes" "University of GH{o}teborg, Programming Methodology Group" "21" "September" "1985" "Christoph M. Hoffmann" "Michael O'Donnell" "Programming with Equations" "Transactions on Programming Languages and Systems" "1" "4" "1982" "83-112" "Association for Computing Machinery" "Alberto Martelli" "Ugo Montanari" "An efficient unification algorithm" "Transactions on Programming Languages and Systems" "4" "2" "1982" "258-282" "Association for Computing Machinery" "D. R. Jefferson" "Virtual Time" "Transactions on Programming Languages and Systems" "7" "3" "1985" "404-425" "Association for Computing Machinery" "F. Wieland" "The performance of a distributed combat simulation with the time warp operating system" "Concurrency: Practice and Experience" "1" "1" "1989" "35-50" "John Wiley & Sons, Ltd." "P. L. Reiher" "D. R. Jefferson" "Dynamic Load Management in the Time Warp Operating System" "Transactions of the Society for Computer Simulation" "7" "2" "1990" "91-120" "Algebras, Theories and Freeness: An Introduction for Computer Scientists" "Rod Burstall" "Joseph Goguen" "1982" "Theoretical Foundations of Programming Methodology" "Proceedings, 1981 Marktoberdorf NATO Summer School, NATO Advanced Study Institute Series, Volume C91" "Reidel" "329-350" "Manfred Wirsing" "Gunther Schmidt" "John Reynolds" "Using Category Theory to Design Implicit Conversions and Generic Operators" "Semantics Directed Compiler Generation" "Neal D. Jones" "1980" "Springer LNCS 94" "211-258" "Philip Wadler" "Views: {A} Way for Pattern Matching to Cohabit with Data Abstraction" "Proceedings, 14th Symposium on Principles of Programming Languages" "Steve Munchnik" "1987" "ACM" "307-312" "Modern Analytic Geometry" "W. K. Morrill" "S. M. Selby" "W. G. Johnson" "1972" "Intext (Scranton PA)" "third" "Geometrical Constructions" "J{o}rgen Staunstrup" "1982" "Proceedings, Aarhus Workshop on Specification" "J{o}rgen Staunstrup" "Springer-Verlag" "25-30" "LNCS, Volume 134" "David Parnas" "On the Criteria to be Used in Decomposing Systems into Modules" "Communications of the Association for Computing Machinery" "15" "1053-1058" "1972" "Mitchell Wand" "Final Algebra Semantics and Data Type Extension" "1979" "Journal of Computer and System Sciences" "19" "27-44" "Hiroto Yasuura" "On the Parallel Computational Complexity of Unification" "Yajima Lab" "ER 83-01" "October" "1983" "Christoph Hoffmann" "Michael O'Donnell" "Robert Strandh" "Implementation of an Interpreter for Abstract Equations" "Software -- Practice and Experience" "15" "12" "1985" "December" "1185-1204" "John Wiley and Sons" "Christoph M. Hoffmann" "Michael O'Donnell" "Pattern Matching in Trees" "Journal of the Association for Computing Machinery" "29" "1" "1982" "68-95" "Association for Computing Machinery" "Joseph Goguen" "Rod Burstall" "Institutions: Abstract Model Theory for Specification and Programming" "Journal of the ACM" "39" "1" "95-146" "1992" "R. M. Karp" "R. E. Miller" "S. Winograd" "The organization of computations for uniform recurrence equations" "Journal of the Association for Computing Machinery" "14" "3" "1967" "563-590" "Association for Computing Machinery" "Mathew Hennessy" "Robin Milner" "Algebraic laws for nondeterminism and concurrency" "Journal of the Association for Computing Machinery" "32" "1" "1985" "137-172" "Association for Computing Machinery" "Maarten H. van Emden" "Robert A. Kowalski" "The Semantics of Predicate Logic as a Programming Language" "Journal of the Association for Computing Machinery" "23" "4" "1976" "733-742" "Refutational Theorem Proving using Term Rewriting Systems" "Jieh Hsiang" "1981" "Univeristy of Illinois at Champaign-Urbana" "An Algebraic Model of Subtypes in Object-Oriented Languages (Draft)" "Kim Bruce" "Peter Wegner" "SIGPLAN Notices" "21" "10" "163-172" "1986" "October" "Completeness of Many-sorted Equational Logic" "Joseph Goguen" "Jos'{e} Meseguer" "SIGPLAN Notices" "16" "7" "24-37" "1981" "July" "On understanding types, data abstracton and polymorphism" "Luca Cardelli" "Peter Wegner" "Computing Surveys" "17" "471-522" "1985" "Proofs by Induction in Equational Theories with Constructors" "Gerard Huet" "Jean-Marie Hullot" "Journal of Computing and System Sciences" "25" "2" "October" "1982" "239-266" "Preliminary version in Proceedings 21th Symposium on Foundations of Computer Science, IEEE, 1980" "David Musser" "On Proving Inductive Properties of Abstract Data Types" "Proceedings, 7th Symposium on Principles of Programming Languages" "1980" "Association for Computing Machinery" "Claude Kirchner" "{M}'{e}thodes et outils de conception syst'{e}matique d'algorithmes d'uni-fi-ca-tion dans les th'{e}ories '{e}quationnelles" "l'Universit'{e} de Nancy 1" "1985" "Claude Kirchner" "helene Kirchner" "Reveur-3: implementation of a general completion procedure parameterized by built-in theories and strategies" "Science of Computer Programming" "1986" "helene Kirchner" "A general inductive completion algorithm and application to abstract data types" "Proceedings, 7th Conference on Automated Deduction" "Springer-Verlag" "LNCS, Volume 170" "282-302" "1984" "helene Kirchner" "Preuves par compl'{e}tion dans les vari'{e}t'{e}s d'alg`{e}bres" "Universit'{e} de Nancy 1" "1985" "Simple Word Problems in Universal Algebra" "Donald Knuth" "P. Bendix" "1970" "Computational Problems in Abstract Algebra" "J. Leech" "Pergamon Press" "Pierre Lescanne" "Computer experiments with the {R}eve term rewriting systems generator" "Proceedings, 10th ACM Symposium on Principles of Programming Languages" "ACM" "1983" "{OBJ3}" "Kokichi Futatsugi" "Joseph Goguen" "Jean-Pierre Jouannaud" "Claude Kirchner" "helene Kirchner" "Jos'{e} Meseguer" "In preparation" "1988" "Joseph Goguen" "Joseph Tardo" "{OBJ}-0 Preliminary Users Manual" "1977" "UCLA" "Semantics and Theory of Computation Report 10" "An Introduction to {OBJ}: {A} Language for Writing and Testing Software Specifications" "Joseph Goguen" "Joseph Tardo" "1979" "Specification of Reliable Software" "Marvin Zelkowitz" "IEEE Press" "170-189" "Reprinted in {it Software Specification Techniques}, Nehan Gehani and Andrew McGettrick, Eds., Addison-Wesley, 1985, pages 391-420" "Joseph Goguen" "Some Design Principles and Theory for {OBJ}-0, a Language for Expressing and Executing Algebraic Specifications of Programs" "Proceedings, Mathematical Studies of Information Processing" "Edward Blum" "Manfred Paul" "Satsoru Takasu" "Springer-Verlag" "1979" "LNCS, Volume 75; Proceedings of a Workshop held August 1978" "425-473" "A Practical Method for Testing Algebraic Specifications" "Joseph Goguen" "Joseph Tardo" "Norman Williamson" "Maria Zamfir" "1979" "UCLA Computer Science Department Quarterly" "7" "1" "59-80" "The Design, Specification and Implementation of {OBJT}: {A} Language for Writing and Testing Abstract Algebraic Program Specifications" "Joseph Tardo" "1981" "UCLA, Computer Science Department" "Joseph Goguen" "Jos'{e} Meseguer" "Rapid Prototyping in the {OBJ} Executable Specification Language" "Software Engineering Notes" "Association for Computing Machinery, Special Interest Group on Software Engineering" "1982" "December" "7" "5" "75-84" "Proceedings of Rapid Prototyping Workshop" "Programming with Parameterized Abstract Objects in {OBJ}" "Joseph Goguen" "Jos'{e} Meseguer" "David Plaisted" "Theory and Practice of Software Technology" "Domenico Ferrari" "Mario Bolognani" "Joseph Goguen" "1983" "163-193" "North-Holland" "Parameterized Programming" "Joseph Goguen" "Transactions on Software Engineering" "1984" "September" "IEEE" "SE-10" "5" "528-543" "A relational notation for state transition systems" "S. S. Lam" "A. U. Shankar" "Transactions on Software Engineering" "1990" "July" "IEEE" "SE-16" "7" "755-775" "Kokichi Futatsugi" "Joseph Goguen" "Jos'{e} Meseguer" "Koji Okada" "Parameterized Programming in {OBJ2}" "Proceedings, Ninth International Conference on Software Engineering" "Robert Balzer" "IEEE Computer Society Press" "1987" "March" "51-60" "S. Nakajima" "K. Futatsugi" "An object-oriented modeling method for algebraic specifications in {CafeOBJ}" "Proceedings, 19th International Conference on Software Engineering" "IEEE Computer Society Press" "1997" "May" "34-44" "Kokichi Futatsugi" "Joseph Goguen" "Jos'{e} Meseguer" "Koji Okada" "Parameterized Programming and its Application to Rapid Prototyping in {OBJ2}" "Japanese Perspectives in Software Engineering" "Y. Matsumoto" "Y. Ohno" "Addison-Wesley" "1989" "77-102" "Writing Programs in {OBJ2}" "Steffan Bonnier" "Department of Computer and Information Science, Linkoping University, Linkoping, Sweden" "1987" "The Design of a Rewrite Rule Interpreter from Algebraic Specifications" "Derek Coleman" "Robin Gallimore" "Victoria Stavridou" "IEE Software Engineering Journal" "95-104" "1987" "July" "{UMIST OBJ} Manual, Version 1.0" "Colin Walter" "Derek Coleman" "Robin Gallimore" "Victoria Stavridou" "UMIST, Manchester, England" "1986" "The Design of a Rewrite Rule Interpreter from Algebraic Specifications" "Derek Coleman" "Robin Gallimore" "Victoria Stavridou" "IEE Software Engineering Journal" "95-104" "1987" "July" "Specifying in {OBJ}, Verifying in {REVE}, and Some Ideas about Time" "Victoria Stavridou" "Department of Computer Science, University of Manchester" "1987" "Draft" "An Implementation of {OBJ2}: An Object-Oriented Language for Abstract Program Specification" "S. Sridhar" "Proceedings, Sixth Conference on Foundations of Software Technology and Theoretical Computer Science" "K. V. Nori" "Springer-Verlag" "1986" "81-95" "LNCS, Volume 241" "{MC-OBJ}: a {C} Interpreter for {OBJ}" "C. Cavenathi" "M. De Zanet" "Giancarlo Mauri" "Note di Software" "36/37" "Dipmentarto Scienze dell'Informazione, Universita de Milano" "1988" "October" "16-26" "In Italian" "An Introduction to {OBJ3}" "Joseph Goguen" "Claude Kirchner" "H'{e}l`{e}ne Kirchner" "Aristide M'{e}grelis" "Jos'{e} Meseguer" "Timothy Winkler" "Proceedings, Conference on Conditional Term Rewriting, Orsay, France, July 8-10, 1987" "Jean-Pierre Jouannaud" "Stephane Kaplan" "Springer LNCS 308" "258-263" "1988" "Confluence of conditional rewrite systems" "N. Dershowitz" "M. Okada" "G. Sivakumar" "Proceedings, Conference on Conditional Term Rewriting, Orsay, France, July 8-10, 1987" "Jean-Pierre Jouannaud" "Stephane Kaplan" "Springer-Verlag, LNCS No. 308" "31-44" "1988" "A completion procedure for conditional equations" "H. Ganzinger" "Proceedings, Conference on Conditional Term Rewriting, Orsay, France, July 8-10, 1987" "Jean-Pierre Jouannaud" "Stephane Kaplan" "Springer-Verlag, LNCS No. 308" "62-83" "Final version will appear in J. Symb. Comp." "1988" "Notes on the elimination of conditions" "E. Giovannetti" "C. Moiso" "Proceedings, Conference on Conditional Term Rewriting, Orsay, France, July 8-10, 1987" "Jean-Pierre Jouannaud" "Stephane Kaplan" "Springer-Verlag, LNCS No. 308" "91-97" "1988" "Operational Semantics of {OBJ3}" "Claude Kirchner" "H'el`ene Kirchner" "Jos'{e} Meseguer" "Proceedings, 15th Intl. Coll. on Automata, Languages and Programming, Tampere, Finland, July 11-15, 1988" "T. Lepist{\"{o}}" "A. Salomaa" "Springer LNCS 317" "287-301" "1988" "Simple Examples of Parameterized Programming in {OBJ2}" "Kokichi Futatsugi" "Proceedings, Summer Programming Symposium" "Information Processing Society of Japan" "1986" "55-61" "An Overview of {OBJ2}" "Kokichi Futatsugi" "Proceedings, France-Japan AI and CS Symposium" "Kazuhiru Fuchi" "Maurice Nivat" "ICOT" "Also, Information Processing Society of Japan, Technical Memorandum PL-86-6" "1986" "Natural semantics on the computer" "D. Cl'ement" "J. Despeyroux" "L. Hascoet" "G. Kahn" "Proceedings, France-Japan AI and CS Symposium" "Kazuhiru Fuchi" "Maurice Nivat" "49-89" "ICOT" "Also, Information Processing Society of Japan, Technical Memorandum PL-86-6" "1986" "Algebraic Specification of {M}acintosh's {Q}uick{D}raw Using {OBJ2}" "Ataru Nakagawa" "Kokichi Futatsugi" "S. Tomura" "T. Shimizu" "ElectroTechnical Laboratory, Tsukuba Science City, Japan" "1987" "Draft" "To appear, {it Proceedings}, Tenth International Conference on Software Engineering, Singapore, April 1988" "Abstract Pascal: {A} Tutorial Introduction" "John T. Latham" "1987" "Version 2.1" "University of Manchester, Department of Computer Science" "The Specification and Controlled Implementation of a Configuration Management Tool using {OBJ} and {A}da" "Christopher Paul Gerrard" "Experience with {OBJ}" "Derek Coleman" "Robin Gallimore" "Joseph Goguen" "Addison-Wesley" "1988" "To appear" "{OBJ} for {OBJ}" "Claude Kirchner" "helene Kirchner" "Aristide Megrelis" "Experience with {OBJ}" "Derek Coleman" "Robin Gallimore" "Joseph Goguen" "Addison-Wesley" "1988" "To appear" "{OBJSA} Net Systems: a Class of High-Level Nets having Objects as Domains" "E. Battiston" "F. DeCindio" "Giancarlo Mauri" "Experience with {OBJ}" "Derek Coleman" "Robin Gallimore" "Joseph Goguen" "Addison-Wesley" "1988" "To appear" "Concerning the Compatibility of {PHIGS} and {GKS}" "D. A. Duce" "Experience with {OBJ}" "Derek Coleman" "Robin Gallimore" "Joseph Goguen" "Addison-Wesley" "1988" "To appear" "Using Mathematical Tools to Aid System Development" "Martin Loomes" "Richard Mitchell" "Experience with {OBJ}" "Derek Coleman" "Robin Gallimore" "Joseph Goguen" "Addison-Wesley" "1988" "To appear" "A Brief History of {OBJ}" "Joseph Goguen" "Experience with {OBJ}" "Derek Coleman" "Robin Gallimore" "Joseph Goguen" "Addison-Wesley" "1988" "To appear" "Higher-Order Functions Considered Unnecessary for Higher-Order Programming" "Joseph Goguen" "Proceedings, Univeristy of Texas Year of Programming, Institute on Declarative Programming" "David Turner" "Addison-Wesley" "1988" "To appear" "Actors: {A} Model of Concurrent Computation in Distributed Systems" "Gul Agha" "1986" "MIT Press" "G. Agha" "Abstracting Interaction Patterns: {A} Programming Paradigm for Open Distribute Systems" "Formal Methods for Open Object-based Distributed Systems" "E. Najm" "J-B. Stefani" "1997" "135-153" "Chapman & Hall" "Foundations of Actor Semantics" "Will Clinger" "1981" "Massachusetts Institute of Technology, Artificial Intelligence Laboratory" "Technical Report {AI-TR-633}" "Computational Aspects of {VLSI}" "Jeffrey Ullman" "1983" "Computer Science Press" "An Abstract Machine for Fast Parallel Matching of Linear Patterns" "Ugo Montanari" "Joseph Goguen" "1987" "May" "Computer Science Laboratory, SRI International" "SRI-CSL-87-3" "Recherches sur la Th'eorie de la {D}'emonstration" "Jacques Herbrand" "Travaux de la Soci'et'e des Sciences et des Lettres de Varsovie, Classe III" "33" "128" "1930" "Functorial Semantics of Algebraic Theories" "F. William Lawvere" "1963" "Proceedings, National Academy of Sciences" "50" "869-873" "Summary of Ph.D. Thesis, Columbia University" "Categories for the Working Mathematician" "Saunders Mac Lane" "1971" "Springer-Verlag" "Topoi, The Categorial Analysis of Logic" "Robert Goldblatt" "1979" "North-Holland" "Categories" "Horst Schubert" "1972" "Springer-Verlag" "J. Alan Robinson" "A Machine-Oriented Logic Based on the Resolution Principle" "1965" "Journal of the Association for Computing Machinery" "12" "23-41" "Order-Sorted Unification" "Jos'{e} Meseguer" "Joseph Goguen" "Gert Smolka" "1989" "J. Symbolic Computation" "8" "383-413" "Basic narrowing revisited" "Werner Nutt" "Pierre R'ety" "Gert Smolka" "1989" "J. Symbolic Computation" "7" "295-317" "Computational Category Theory" "David Rydeheard" "Rod Burstall" "1988" "Prentice-Hall" "To appear" "On the Theory of Specification, Implementation and Parameterization of Abstract Data Types" "Hans-Dieter Ehrich" "1982" "Journal of the Association for Computing Machinery" "29" "206-227" "Hans-Dieter Ehrich" "Udo Lipeck" "Algebraic Domain Equations" "Theoretical Computer Science" "27" "1983" "167-196" "Dana Scott" "Outline of a Mathematical Theory of Computation" "1970" "Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems" "Also appeared as Technical Monograph PRG 2, Oxford University, Programming Research Group" "Princeton University" "169-176" "Dana Scott" "Lattice Theory, Data Types and Semantics" "Formal Semantics of Algorithmic Languages" "Randall Rustin" "1972" "Prentice Hall" "65-106" "Remarks on Remarks on Many-Sorted Equational Logic" "Joseph Goguen" "Jos'{e} Meseguer" "Bulletin of the European Association for Theoretical Computer Science" "30" "October" "1986" "66-73" "Also in {it SIGPLAN Notices}, Volume 22, Number 4, pages 41-48, April 1987" "On a categorical tensor calculus for automata" "Jos'{e} Meseguer" "Ignacio Sols" "Bull. Acad. Polon. Sci., ser. math. astr. et phys." "23" "1975" "1161-1166" "Order-Sorted Equational Computation" "Gert Smolka" "Werner Nutt" "Joseph Goguen" "Jos'{e} Meseguer" "Resolution of Equations in Algebraic Structures" "2" "297-367" "Maurice Nivat" "Hassan A{\"{i}}t-Kaci" "Academic Press" "1989" "Completion algorithms for conditional rewriting systems" "S. Kaplan" "J.-L. R'{e}my" "Resolution of Equations in Algebraic Structures" "2" "141-170" "Maurice Nivat" "Hassan A{\"{i}}t-Kaci" "Academic Press" "1989" "Thomas Johnsson" "Target code generation from {G}-machine code" "Graph Reduction" "Joseph Fasel" "Robert Keller" "LNCS, Volume 279" "Springer-Verlag" "119-159" "1987" "Richard Kieburtz" "The {G}-machine: a fast, graph-reduction evaluator" "Proceedings, Conference on Functional Programming Languages and Computer Architecture" "400-413" "Jean-Pierre Jouannaud" "LNCS, Volume 201" "Springer-Verlag" "1985" "A. Appel" "D. Mac{Queen}" "A {Standard} {ML} compiler" "Proceedings, Conference on Functional Programming Languages and Computer Architecture" "LNCS, Volume 274" "Springer-Verlag" "301-324" "1987" "Peter Canning" "William Cook" "Walt Hill" "John Mitchell" "Walter Olthoff" "{F}-Bounded Quantification for Object-Oriented Programming" "Proceedings, Conference on Functional Programming Languages and Computer Architecture" "David MacQueen" "LNCS" "Springer-Verlag" "1989" "Unification Theory" "{J\"{o}rg} Siekmann" "To appear in {it Journal of Symbolic Computation}" "1988" "Preliminary Version in {it Proceedings}, European Conference on Artificial Intelligence, Brighton, 1986" "What is Unification? | {A} Categorical View of Substitution, Equation and Solution" "Joseph Goguen" "Resolution of Equations in Algebraic Structures" "Maurice Nivat" "Hassan A{\"{i}}t-Kaci" "Academic Press" "217-261" "1989" "Foundations of Logic Programming" "John Lloyd" "Springer-Verlag" "1984" "Hope: an Experimental Applicative Language" "Rod Burstall" "David MacQueen" "Donald Sannella" "1980" "Proceedings, First LISP Conference" "Stanford University" "136-143" "1" "Etude et {R}'ealisation d'un Syst`eme {Prolog}" "A. Colmerauer" "H. Kanoui" "M. van Caneghem" "Groupe d'Intelligence Artificielle, U.E.R. de Luminy, Universit'e d'Aix-Marseille II" "1979" "Unification in Many-sorted Equational Theories" "Proceedings, 8th International Conference on Automated Deduction" "Manfred Schmidt-Schauss" "Springer-Verlag" "1986" "538-552" "LNCS, Volume 230" "Computational aspects of order-sorted logic with term declarations" "Manfred Schmidt-Schauss" "Springer LNCS 395" "1989" "A Classification of Many-Sorted Unification Theories" "Proceedings, 8th International Conference on Automated Deduction" "Christoph Walther" "Springer-Verlag" "1986" "525-537" "LNCS, Volume 230" "Building-in Equational Theories" "Gordon Plotkin" "Machine Intelligence" "7" "1972" "November" "Edinburgh University Press" "73-90" "An Introduction to Unification-Based Approaches to Grammar" "Stuart Shieber" "1986" "Center for the Study of Language and Information" "Prolog and Infinite Trees" "Alain Colmerauer" "Logic Programming" "Keith Clark" "Sten-{AA}ke T{\"{a}}rnlund" "1982" "231-251" "Academic Press" "A Lattice-Theoretic Approach to Computation Based on a Calculus of Partially-Ordered Type Structures" "Hassan Ait-Kaci" "1984" "University of Pennsylvania" "An Algebraic Semantics Approach to the Effective Resolution of Type Equations" "Hassan Ait-Kaci" "1986" "Theoretical Computer Science" "45" "293-351" "Inheritance Hierarchies: Semantics and Unification" "Gert Smolka" "Hassan A{\"{i}}t-Kaci" "1989" "Journal of Symbolic Computation" "7" "343-370" "Data Types" "Daniel Lehmann" "Michael Smyth" "The University of Warnick" "1977" "May" "19" "Theory of Computation Report" "Unification over Complex Indeterminates in Prolog" "Kuniaki Mukai" "1985" "ICOT" "TR-113" "Mitchell Wand" "On the Recursive Specification of Data Types" "Proceedings, Symposium on Category Theory Applied to Computation and Control" "Ernest Manes" "214-217" "Springer-Verlag" "LNCS, Volume 25" "1975" "Some Fundamental Algebraic Tools for the Semantics of Computation, Part 1: Comma Categories, Colimits, Signatures and Theories" "Joseph Goguen" "Rod Burstall" "1984" "Theoretical Computer Science" "31" "2" "175-209" "A Unification Algorithm for Associative-Commutative Functions" "Mark Stickel" "Journal of the Association for Computing Machinery" "28" "1981" "423-434" "Structures Alg'ebriques dans les Cat'egories" "Jean B'{e}nabou" "Cahiers de Topologie et G'eometrie Diff'erentielle" "10" "1-126" "1968" "Structures defined by finite limits in the enriched context, {I}" "G. M. Kelly" "Cahiers de Topologie et G'eometrie Diff'erentielle" "23" "3-42" "1982" "The Category-Theoretic Solution of Recursive Domain Equations" "Michael Smyth" "Gordon Plotkin" "1982" "11" "761-783" "{SIAM} Journal of Computation" "Also Technical Report D.A.I. 60, University of Edinburgh, Department of Artificial Intelligence, December 1978" "Functional Analysis" "Kosaku Yosida" "1968" "Second Edition" "Springer-Verlag" "Ernest Manes" "Algebraic Theories" "1976" "Springer-Verlag" "Graduate Texts in Mathematics, Volume 26" "A Theory of Type Polymorphism in Programming" "Robin Milner" "Journal of Computer and System Sciences" "17" "3" "1978" "348-375" "Edinburgh {LCF}" "Michael Gordon" "Robin Milner" "Christopher Wadsworth" "Springer-Verlag" "1979" "LNCS, Volume 78" "Logic and Data Bases" "Herve Gallaire" "Jack Minker" "1978" "Plenum Press" "Logic Programming: Functions, Relations and Equations" "Douglas DeGroot" "Gary Lindstrom" "1986" "Prentice-Hall" "{HOL}: {A} Machine Oriented Formulation of Higher-Order Logic" "Michael Gordon" "1985" "July" "85" "University of Cambridge, Computer Laboratory" "Characterization of Computable Data Types by Means of a Finite Equational Specification Method" "Jan Bergstra" "John Tucker" "Automata, Languages and Programming, Seventh Colloquium" "Springer-Verlag" "1980" "J. W. de Bakker" "J. van Leeuwen" "76-90" "LNCS, Volume 81" "Permutation of transitions: an event structure semantics for {CCS} and {SCCS}" "G'erard Boudol" "Illaria Castellani" "Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency" "Springer-Verlag" "1988" "J. W. de Bakker" "W.-P. de Roever" "G. Rozenberg" "411-427" "LNCS, Volume 354" "Algebraic Specifications of Computable and Semicomputable Data Structures" "Jan Bergstra" "John Tucker" "1987" "To appear in {it Theoretical Computer Science}; originally, Preprint IW 115, Mathematisch Centrum, Department of Computer Science, Amsterdam, August 1979" "A view of systolic design" "Christian Lengauer" "1991" "To appear in Proc. of {it Parallel Computing Technologies}, Novosibirsk, USSR, September 1991" "Completeness of Proof Systems for Equational Specifications" "David MacQueen" "Donald Sannella" "IEEE Transactions on Software Engineering" "1985" "SE-11" "5" "May" "454-461" "The mapping of linear recurrence equations on regular arrays" "P. Quinton" "V. van Dongen" "J. VLSI Signal Processing" "1989" "1" "2" "October" "95-113" "On the Structure of Abstract Algebras" "Garrett Birkhoff" "1935" "Proceedings of the Cambridge Philosophical Society" "31" "433-454" "Completeness of Many-sorted Equational Logic" "Joseph Goguen" "Jos'{e} Meseguer" "1985" "Houston Journal of Mathematics" "11" "3" "307-334" "Preliminary versions have appeared in: {it SIGPLAN Notices}, July 1981, Volume 16, Number 7, pages 24-37; SRI Computer Science Laboratory Technical Report CSL-135, May 1982; and Report CSLI-84-15, Center for the Study of Language and Information, Stanford University, September 1984" "Inductive Methods for Reasoning about Abstract Data Types" "Stephen Garland" "John Guttag" "Proceedings, Fifteenth Symposium on Principles of Programming Languages" "1988" "January" "ACM" "219-229" "A Computational Logic" "Robert Boyer" "J Moore" "Academic Press" "1980" "A {P}rolog Technology Theorem Prover" "Mark Stickel" "First International Symposium on Logic Programming" "Association for Computing Machinery" "1984" "February" "Social Processes and Proofs of Theorems and Programs" "R. A. DeMillo" "Richard Lipton" "Alan Perlis" "1977" "Proceedings, Fourth Symposium on Principles of Programming Languages" "Association for Computing Machinery" "206-214" "Logic and Computation: Interactive Proof with {C}ambridge {LCF}" "Lawrence Paulson" "Cambridge University Press" "1987" "Cambridge Tracts in Theoretical Computer Science, Volume 2" "Department of Defense" "Reference Manual for the Ada Programming Language" "United States Government, Report ANSI/MIL-STD-1815 A" "1983" "Kokichi Futatsugi" "Koji Okada" "Specification Writing as Construction of Hierarchically Structured Clusters of Operators" "Information Processing '80" "IFIP Press" "1980" "287-292" "Proceedings of 1980 IFIP Congress" "H. G. Baker" "C. Hewitt" "Laws for communicating parallel processes" "Proceedings of the 1977 IFIP Congress" "IFIP Press" "1977" "987-992" "Kokichi Futatsugi" "Koji Okada" "A Hierarchical Structuring Method for Functional Software Systems" "Proceedings, Sixth International Conference on Software Engineering" "IEEE Press" "1982" "393-402" "Abstract Specification of Data Types" "Steven Zilles" "1974" "Computation Structures Group, MIT" "119" "Stop Losing Sleep over Incomplete Data Type Specification" "Jean-Jacques Thiel" "Proceedings, Eleventh Symposium on Principles of Programming Languages" "Ken Kennedy" "Association for Computing Machinery" "1984" "Reiji Nakajima" "T. Yuasa" "The {IOTA} Programming System" "1983" "Springer-Verlag" "LNCS, Volume 160" "Graham Birtwistle" "Ole-Johan Dahl" "Bjorn Myhrhaug" "Kristen Nygaard" "Simula underline{Begin}" "1979" "Charwell-Bratt Ltd" "The {SIMULA} 67 Common Base Language" "Ole-Johan Dahl" "Bjorn Myhrhaug" "Kristen Nygaard" "1970" "Norwegian Computing Center, Oslo" "Publication S-22" "Logic for Problem Solving" "Robert Kowalski" "Department of Artificial Intelligence, University of Edinburgh" "1974" "DCL Memo 75" "Also, a book in the Artificial Intelligence Series, North-Holland Press, 1979" "Source Level Tools for Logic Programming" "Richard O'Keefe" "1985" "Symposium on Logic Programming" "IEEE" "68-72" "A Study in the Foundations of Programming Methodology: Specifications, Institutions, Charters and Parchments" "Joseph Goguen" "Rod Burstall" "Proceedings, Conference on Category Theory and Computer Programming" "David Pitt" "Samson Abramsky" "Axel Poign'{e}" "David Rydeheard" "Springer-Verlag" "1986" "313-333" "LNCS, Volume 240; also, Report Number CSLI-86-54, Center for the Study of Language and Information, Stanford University, June 1986" "Introducing Institutions" "Joseph Goguen" "Rod Burstall" "Logics of Programs" "Edmund Clarke" "Dexter Kozen" "Springer-Verlag" "1984" "221-256" "LNCS, Volume 164" "One, None, {A} Hundred Thousand Specification Languages" "Joseph Goguen" "1986" "Information Processing '86" "H.-J. Kugler" "Proceedings of 1986 IFIP Congress" "Elsevier" "995-1003" "Unification Revisited" "Foundations of Deductive Databases and Logic Programming" "Jack Minker" "Jean-Louis Lassez" "Michael Maher" "Kimbal Marriott" "1988" "587-625" "Morgan Kaufmann" "Unification in Categories" "Several Aspects of Unification" "Toshiaki Kurokawa" "Takanori Adachi" "1984" "35-43" "ICOT, Technical Report TM-0029" "Formal Philosophy: Selected Papers of Richard Montague" "Richard Montague" "Yale University Press" "1974" "Edited and with an introduction by Richard Thomason" "Peter van Emde Boas" "Theo Janssen" "The Impact of Frege's Principle of Compositionality for the Semantics of Programming and Natural Languages" "University of Amsterdam, Department of Mathematics" "79-07" "1979" "Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware" "Formal Aspects of {VLSI} Design" "George Milne" "P. A. Subrahmanyam" "Michael Gordon" "1986" "North-Holland" "Hardware Verification Using Higher-Order Logic" "Albert Camilleri" "Michael Gordon" "Tom Melham" "1986" "June" "91" "University of Cambridge, Computer Laboratory" "Compiling for the Rewrite Rule Machine" "Hitoshi Aida" "Joseph Goguen" "Jos'e Meseguer" "In preparation" "Fairness in term rewriting systems" "Sara Porat" "Nissim Francez" "Manuscript, Technion, May 3, 1990." "Implementing Term Rewriting by Graph Reduction: Termination of Combined Systems" "Detlef Plump" "To appear in S. Kaplan and M. Okada (eds.) Proc. Intl. Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990, Springer LNCS" "Compiling Concurrent Rewriting onto the Rewrite Rule Machine" "Hitoshi Aida" "Joseph Goguen" "Jos'e Meseguer" "S. Kaplan" "M. Okada" "Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990" "Springer LNCS 516" "320-332" "1991" "Conditional rewriting logic: deduction, models and concurrency" "Jos'e Meseguer" "S. Kaplan" "M. Okada" "Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990" "Springer LNCS 516" "64-91" "Also Technical Report SRI-CSL-90-14, SRI International, Computer Science Laboratory, November 1990" "1991" "Transforming Conditional Rewrite Rules into Unconditional Ones" "Hitoshi Aida" "Jos'e Meseguer" "In preparation" "The Rewrite Rule Machine" "Joseph Goguen" "Jos'{e} Meseguer" "Sany Leinwand" "Timothy Winkler" "Hitoshi Aida" "SRI International, Computer Science Laboratory" "1989" "March" "SRI-CSL-89-6" "Arvind" "D. E. Culler" "Dataflow Architectures" "Annual Reviews in Computer Science" "1986" "H. P. Barendregt" "M. C. J. D. van Eekelen" "J. R. W. Glauert" "J. R. Kennaway" "M. J. Plasmeijer" "M. R. Sleep" "Towards an Intermediate Language Based on Graph Rewriting" "Proceedings, PARLE Conference" "LNCS, Volume 259" "Springer-Verlag" "1987" "J. R. W. Glauert" "J. R. Kennaway" "M. R. Sleep" "Specification of {Dactl}" "School of Information Systems, University of East Anglia" "1987" "R. Kennaway" "Graph Rewriting in Some Categories of Partial Morphisms" "School of Information Systems, University of East Anglia" "1990" "A Categorical Construction for Generalised Graph Rewriting" "J. R. W. Glauert" "J. R. Kennaway" "Submitted to PARLE 89 conference" "Simon L Peyton Jones" "Chris Clack" "Jon Salkild" "Mark Hardie" "{GRIP} - a high-performance architecture for parallel graph reduction" "Proceedings, IFIP Conference on Functional Programming Languages and Computer Architecture" "Portland" "G. Kahn" "LNCS, Volume 274" "Springer-Verlag" "98-112" "September" "1987" "B. Jayaraman" "D. Plaisted" "Functional programming with sets" "Proceedings, IFIP Conference on Functional Programming Languages and Computer Architecture" "Portland" "G. Kahn" "LNCS, Volume 274" "Springer-Verlag" "194-210" "September" "1987" "A Network of Microprocessors to Execute Reduction Languages" "Gulyo Mag'o" "International Journal of Computer and Information Sciences" "8" "5 and 6" "1979" "349--358 and 435--481" "The {FFP} Machine -- {A} Progress Report" "Gulyo Mag'o" "D. Middleton" "Proceedings, International Workshop on High-level Computer Architecture" "IEEE Press" "5.13--5.25" "1984" "G. Wiederhold" "Mediators in the Architecture of Future Information Systems" "IEEE Computer" "1992" "25" "3" "38-49" "March" "G. Wiederhold" "P. Wegner" "S. Ceri" "Toward Megaprogramming" "Communications of the ACM" "1992" "35" "11" "89-99" "November" "P. Mills" "L. Nyland" "J. Prins" "J. Reif" "Prototyping high performance parallel computing applications in Proteus" "Proceedings of 1992 DARPA Software Conference" "1992" "433-442" "DARPA" "N. J. Pelc" "R. J. Herfkens" "A. Shimakawa" "D. R. Enzmann" "Phase Contrast Cine Magnetic Resonance Imaging" "Magnetic Resonance Quarterly" "1991" "7" "229-254" "N. J. Pelc" "F. G. Sommer" "D. R. Enzmann" "L. R. Pelc" "G. H. Glover" "Accuracy and Precision of Phase-Contrast {MR} Flow Measurements" "77th {RSNA}, Radiology 189" "1991" "Chicago, Illinois" "S. Napel" "D. H. Lee" "R. Frayne" "B. K. Rutt" "Visualizing Three-Dimensional Flow with Simulated Streamlines and Three-Dimensional Phase-Contrast {MR} Imaging" "J. Magn. Reson. Imaging" "1992" "2" "143-53" "C. A. Pelizzari" "G. T. Chen" "D. R. Spelbring" "R. R. Weichselbaum" "C. T. Chen" "Accurate Three-Dimensional Registration of {CT}, {PET}, and/or {MR} Images of the Brain" "J. Comput. Assist. Tomogr." "1989" "13" "20-6" "P. van den Elsen" "E.-J. D. Pol" "T. S. Sumanaweera" "P. F. Hemler" "S. Napel" "J. R. Adler" "Grey Value Correlation Techniques Used for Automatic Matching of {CT} and {MR} Brain and Spine Images" "Manuscript" "1994" "E. Astesiano" "M. Cerioli" "Free Objects and Equational Deduction for Partial Conditional Specifications" "Dipartimento de Matematica, University of Genova" "1990" "3" "E. Astesiano" "M. Cerioli" "Partial Higher-Order Specifications" "Fundamenta Informaticae" "1992" "16" "2" "101-126" "E. Astesiano" "M. Cerioli" "Relationships between Logical Frameworks" "Recent Trends in Data Type Specification" "1993" "M. Bidoit" "C. Choppy" "126-143" "Springer-Verlag" "655" "LNCS" "A. Avron" "F. Honsell" "I. A. Mason" "R. Pollack" "Using Typed Lambda Calculus to Implement Formal Systems on a Machine" "Journal of Automated Reasoning" "1992" "9" "3" "309-354" "December" "M. Barr" "C. Wells" "Category Theory for Computing Science" "Prentice-Hall" "1990" "D. A. Basin" "R. L. Constable" "Metalogical Frameworks" "Logical Environments" "1993" "G. Huet" "G. Plotkin" "1-29" "Cambridge University Press" "M. Bidoit" "H.-J. Kreowski" "P. Lescanne" "F. Orejas" "D. Sannella" "Algebraic System Specification and Development. {A} Survey and Annotated Bibliography" "Springer-Verlag" "1991" "501" "LNCS" "M. P. Bonacina" "J. Hsiang" "A Category Theory Approach to Completion-Based Theorem Proving Strategies" "Unpublished manuscript presented at {em Category Theory 1991}, Mc Gill University, Montr'eal, Canada" "1991" "M. Broy" "M. Wirsing" "Partial Abstract Types" "Acta Informatica" "1982" "18" "47-64" "U. Montanari" "F. Rossi" "Contextual nets" "Acta Informatica" "1995" "32" "545-596" "L. Cardelli" "G. Longo" "A Semantic Basis for {Q}uest" "Journal of Functional Programming" "1991" "1" "4" "417-458" "M. Cerioli" "Relationships between Logical Formalisms" "Technical Report TD-4/93, Dipartimento di Informatica, Universit`a di Pisa" "1993" "F. Gadducci" "On the algebraic approach to concurrent term rewriting" "Dipartimento di Informatica, Universit`a di Pisa" "1996" "J. Darlington" "Y. Guo" "Constrained Equational Deduction" "Proc. Second Int. Workshop on Conditional and Typed Rewriting Systems, Montreal, Canada, June 1990" "1991" "S. Kaplan" "M. Okada" "424-435" "Springer-Verlag" "516" "LNCS" "G. Denker" "M. Gogolla" "Translating {TROLL} {it light} concepts to {M}aude" "Recent Trends in Data Type Specification" "1994" "H. Ehrig" "F. Orejas" "173-187" "Springer-Verlag" "785" "LNCS" "H. Ehrig" "M. Baldamus" "F. Orejas" "New Concepts of Amalgamation and Extension of a General Theory of Specifications" "Recent Trends in Data Type Specification" "1993" "M. Bidoit" "C. Choppy" "199-221" "Springer-Verlag" "655" "LNCS" "S. Feferman" "Finitary Inductively Presented Logics" "Logic Colloquium'88" "1989" "R. Ferro" "others" "191-220" "North-Holland" "A. Felty" "D. Miller" "Encoding a Dependent-Type $lambda$-Calculus in a Logic Programming Language" "Proc. 10th. Int. Conf. on Automated Deduction, Kaiserslautern, Germany, July 1990" "1990" "M. E. Stickel" "221-235" "Springer-Verlag" "449" "LNCS" "J. Fiadeiro" "J. Costa" "Mirror, Mirror in my Hand: {A} Duality Between Specifications and Models of Process Behaviour" "Research Report, DI-FCUL, Lisboa, Portugal" "May" "1994" "J. Fiadeiro" "T. Maibaum" "Generalising Interpretations between Theories in the Context of ($pi$-)Institutions" "G. Burn" "S. Gay" "M. Ryan" "Theory and Formal Methods 93" "Springer-Verlag" "126-147" "1993" "D. Gabbay" "Labelled Deductive Systems. {V}olume 1: Foundations" "Max Planck Institut f{\"u}r Informatik" "Saarbr{\"u}cken, Germany" "1994" "MPI-I-94-223" "May" "D. Gabbay" "Fibred Semantics and the Weaving of Logics 1" "Unpublished manuscript" "May" "1993" "P. Gardner" "Representing Logics in Type Theory" "Technical Report CST-93-92, Department of Computer Science, University of Edinburgh" "1992" "M. Gogolla" "Partially Ordered Sorts in Algebraic Specifications" "Proc. Ninth Colloquium on Trees in Algebra and Programming" "1984" "B. Courcelle" "139-153" "Cambridge University Press" "Martin Gogolla" "Maura Cerioli" "What is an {A}bstract {D}ata {T}ype after all?" "DISI- University of Genova" "To appear" "1994" "J. A. Goguen" "R. Diaconescu" "Towards an Algebraic Semantics for the Object Paradigm" "Recent Trends in Data Type Specification" "1994" "H. Ehrig" "F. Orejas" "1-29" "Springer-Verlag" "785" "LNCS" "J. A. Goguen" "A. Stevens" "K. Hobley" "H. Hilberdink" "{2OBJ}: {A} Meta-logical Framework Based on Equational Logic" "Philosophical Transactions of the Royal Society, Series A" "1992" "339" "69-86" "R. Harper" "F. Honsell" "G. Plotkin" "A Framework for Defining Logics" "Journal of the Association Computing Machinery" "1993" "40" "1" "143-184" "J. A. Bergstra" "J. Heering" "P. Klint" "Module Algebra" "Journal of the Association Computing Machinery" "1990" "37" "335-372" "J. A. Bergstra" "J. Heering" "P. Klint" "Algebraic Specification" "ACM Press" "1989" "R. Harper" "D. Sannella" "A. Tarlecki" "Structure Theory Presentations and Logic Representations" "Annals of Pure and Applied Logic" "1994" "67" "113-160" "C. Kirchner" "H. Kirchner" "M. Vittek" "Designing Constraint Logic Programming Languages using Computational Systems" "Principles and Practice of Constraint Programming: The Newport Papers" "1995" "133-160" "V. Saraswat" "P. van Hentenryck" "MIT Press" "C. Laneve" "U. Montanari" "Axiomatizing Permutation Equivalence in the $lambda$-Calculus" "Proc. Third Int. Conf. on Algebraic and Logic Programming, Volterra, Italy, September 1992" "1992" "H. Kirchner" "G. Levi" "350-363" "Springer-Verlag" "632" "LNCS" "C. Laneve" "U. Montanari" "Axiomatizing Permutation Equivalence" "Mathematical Structures in Computer Science" "1996" "6" "219-249" "J. Levy" "A Higher Order Unification Algorithm for Bi-Rewriting Systems" "Segundo Congreso Programaci'on Declarativa" "1993" "291-305" "J. Agust'{i}" "P. Garc'{i}a" "CSIC" "Blanes, Spain" "September" "J. Levy" "J. Agust'{i}" "Bi-Rewriting, a Term Rewriting Technique for Monotonic Order Relations" "Proc. Fifth Int. Conf. on Rewriting Techniques and Applications, Montreal, Canada, June 1993" "1993" "17-31" "C. Kirchner" "Springer-Verlag" "690" "LNCS" "Narciso Mart'{i}-Oliet" "Jos'e Meseguer" "Action and Change in Rewriting Logic" "Dynamic Worlds: From the Frame Problem to Knowledge Management" "R. Pareschi" "B. Fronhoefer" "1998" "To be published by Kluwer Academic Publishers" "P. Martin-L{\"o}f" "Constructive Mathematics and Computer Programming" "Proc. 6th Int. Congress for Logic, Methodology, and Philosophy of Science, Hannover, 1979" "L. J. Cohen" "others" "1982" "153-175" "North-Holland" "S. Matthews" "A. Smaill" "D. Basin" "Experience with {{it FS}$_0$} as a Framework Theory" "Logical Environments" "1993" "G. Huet" "G. Plotkin" "61-82" "Cambridge University Press" "K. Meinke" "Universal Algebra in Higher Types" "Theoretical Computer Science" "1992" "100" "385-417" "G. Nadathur" "D. Miller" "An Overview of {$lambda$Prolog}" "Fifth Int. Joint Conf. and Symp. on Logic Programming" "1988" "K. Bowen" "R. Kowalski" "810-827" "The MIT Press" "L. Paulson" "The Foundation of a Generic Theorem Prover" "Journal of Automated Reasoning" "1989" "5" "363-39" "F. Pfenning" "Elf: {A} Language for Logic Definition and Verified Metaprogramming" "Proc. Fourth Annual IEEE Symp. on Logic in Computer Science" "1989" "313-322" "Asilomar, California" "June" "A. Poign'e" "On Specifications, Theories, and Models with Higher Types" "Information and Control" "1986" "68" "1-46" "A. Poign'e" "Foundations Are Rich Institutions, but Institutions Are Poor Foundations" "Categorical Methods in Computer Science with Aspects from Topology" "1989" "H. Ehrig" "H. Herrlich" "H.-J. Kreowski" "G. Preuss" "82-101" "Springer-Verlag" "393" "LNCS" "A. Poign'e" "Parametrization for Order-Sorted Algebraic Specification" "Journal of Computer and System Sciences" "1990" "40" "2" "229-268" "A. Poign'e" "Typed {H}orn Logic" "Proc. 15th. Int. Symp. on Mathematical Foundations of Computer Science, Bansk'a Bystrica, Czechoslovaquia, August 1990" "1990" "B. Rovan" "470-477" "Springer-Verlag" "452" "LNCS" "H. Reichel" "An Approach to Object Semantics Based on Final Coalgebras" "Unpublished manuscript presented at {em Dagstuhl Seminar on Specification and Semantics}, Schloss Dagstuhl, Germany, May 1993" "A. Salibra" "G. Scollo" "A Soft Stairway to Institutions" "Recent Trends in Data Type Specification" "1993" "M. Bidoit" "C. Choppy" "310-329" "Springer-Verlag" "655" "LNCS" "A. Salibra" "G. Scollo" "Compactness and {L}{\"o}wenheim-{S}kolem Properties in Pre-Institution Categories" "Laboratoire d'Informatique de l'Ecole Normale Sup'erieure" "1992" "LIENS-92-10" "Paris" "March" "D. Sannella" "A. Tarlecki" "Toward Formal Development of Programs from Algebraic Specifications: Implementations Revisited" "Acta Informatica" "1988" "25" "233-281" "R. M. Smullyan" "Theory of Formal Systems" "Princeton University Press" "1961" "47" "Annals of Mathematics Studies" "R. M. Smullyan" "Diagonalization and Self-Reference" "Oxford University Press" "1994" "A. Tarlecki" "Free Constructions in Algebraic Institutions" "Proc. Mathematical Foundations of Computer Science '84" "1984" "M. P. Chytil" "V. Koubek" "526-534" "Springer-Verlag" "176" "LNCS" "A. Tarlecki" "Bits and Pieces of the Theory of Institutions" "Proc. Workshop on Category Theory and Computer Programming, Guildford, UK, September 1985" "1986" "D. Pitt" "S. Abramsky" "A. Poign'e" "D. Rydeheard" "334-363" "Springer-Verlag" "240" "LNCS" "A. Tarlecki" "R. M. Burstall" "J. A. Goguen" "Some Fundamental Algebraic Tools for the Semantics of Computation. {P}art 3: Indexed Categories" "Theoretical Computer Science" "1991" "91" "239-264" "P. Viry" "Rewriting: An Effective Model of Concurrency" "PARLE'94, Proc. Sixth Int. Conf. on Parallel Architectures and Languages Europe, Athens, Greece, July 1994" "1994" "648-660" "C. Halatsis" "D. Maritsas" "G. Philokyprou" "S. Theodoridis" "Springer-Verlag" "817" "LNCS" "David Culler" "Andrea Dusseau" "Seth Copen Goldstein" "Arvind Krishnamurthy" "Steven Lumetta" "Thorsten {von} Eicken" "Katherine Yelick" "Parallel Programming in Split-{C}" "{Proceedings of Supercomputing '93}" "1993" "Sunderam" "V. Sunderam" "{PVM: } {A} Framework for Parallel Distributed Computing" "Concurrency: Practice and Experience" "2" "4" "1990" "December" "K. M. Chandy" "C. Kesselman" "{{CC++}: A Declarative Concurrent Object-Oriented Programming Notation}" "{Research Directions in Concurrent Object-Oriented Programming}" "1993" " {Agha, Wegner}" "Yonezawa" "175-211" "MIT Press" "Valentin F. Turchin" "The Concept of a Supercompiler" "{ACM} Transactions on Programming Languages and Systems" "8" "3" "292-325" "1986" "Valentin F. Turchin" "{REFAL}-5, Programming Guide and Reference Manual" "1989" "New England Publishing Co." "Valentin F. Turchin" "Andrei P. Nemytykh" "Metavariables: their Implementation and Use in Program Transformation" "City College of CUNY" "CSc-TR-95-012" "1995" "Anders Bondorf" "A Self-Applicable Partial Evaluator for Term Rewriting Systems" "TAPSOFT'89" "1989" "J. D'{i}az" "F. Orejas" "81-95" "Springer LNCS 352" "Leon Sterling" "Ehud Shapiro" "The Art of Prolog" "MIT Press" "1986" "Takuo Watanabe" "Towards a Foundation of Computational Reflection based on Abstract Rewriting (Preliminary Result)" "IMSA'95" "1995" "143-145" "Information-Technology Promotion Agency, Japan" "F. Kumeno" "Y. Tahara" "A. Ohsuga" "S. Honiden" "Agent oriented programming language, {Flage}" "IMSA'95" "1995" "29-44" "Information-Technology Promotion Agency, Japan" "David Sherman" "Robert Strandh" "Ir`{e}ne Durand" "Optimization of Equational Programs Using Partial Evaluation" "PEPM'91" "1991" "72-82" "SIGPLAN Notices" "N. Jones" "Mix ten year later" "PEPM'95" "1995" "24-38" "ACM-SIGPLAN" "Efficient self-interpretation in lambda calculus" "Torben AE. Mogensen" "1992" "Journal of Functional Programming" "2" "3" "345-364" "Harald Ruess" "Formal Meta-Programming in the Calculus of Constructions" "Universit{\"{a}}t Ulm" "1995" "Lawrence Paulson" "Tactics and Tacticals in {Cambridge LCF}" "University of Cambridge" "39" "1983" "Patricia Hill" "John Lloyd" "The {G\"{o}del} Programming Language" "MIT Press" "1994" "G. L. {Steele, Jr.}" "G. J. Sussman" "The Art of the Interpreter or, the Modularity Complex" "{AIM-453}" "{MIT AI-Lab}" "May" "1978" "The Mystery of the Tower Revealed" "M. Wand" "D. P. Friedman" "1988" "Lisp and Symbolic Computation" "1" "1" "11-38" "Prolegomena to a Theory of Mechanized Formal Reasoning" "Richard W. Weyhrauch" "1980" "Artificial Intelligence" "13" "133-170" "Metafunctions: proving them correct and using them efficiently as new proof procedures" "R. S. Boyer" "J Strother Moore" "1981" "The Correctness Problem in Computer Science" "Robert Boyer" "J Moore" "Academic Press" "103-185" "N. Shankar" "Metamathematics, Machines, and {G\"{o}del's} Proof" "Cambridge University Press" "1994" "Reflecting the Semantics of Reflected Proof" "Douglas J. Howe" "1990" "Proof Theory" "Peter Aczel" "Harold Simmons" "Stanley S. Wainer" "Cambridge University Press" "229-250" "Se'{a}n Matthews" "Reflection in Logical Systems" "IMSA'92" "1992" "178-183" "Information-Technology Promotion Agency, Japan" "Fausto Giunchiglia" "Paolo Traverso" "Alessandro Cimatti" "Paolo Pecchiari" "A System for Multi-Level Reasoning" "IMSA'92" "1992" "190-195" "Information-Technology Promotion Agency, Japan" "Alessandro Coglio" "Fausto Giunchiglia" "Jos'e Meseguer" "Carolyn Talcott" "Composing and Controlling Search in Reasoning Theories Using Mappings" "Frontiers of Combining Systems, FroCos 2000" "2000" "200-216" "Information-Technology Promotion Agency, Japan" "Luis H. {Rodriguez, Jr.}" "A Study on the Viability of a Production-Quality Metaobject Protocol-Based Statically Parallelizing Compiler" "IMSA'92" "1992" "107-112" "Information-Technology Promotion Agency, Japan" "Hideaki Okamura" "Yutaka Ishikawa" "Mario Tokoro" "{AL-1/D}: {A} Distributed Programming System with Multi-Model Reflection Framework" "IMSA'92" "1992" "36-47" "Information-Technology Promotion Agency, Japan" "Manuel Clavel" "Jose Meseguer" "Reflection in rewriting logic and its applications in the {Maude} language" "IMSA'97" "1997" "128-139" "Information-Technology Promotion Agency, Japan" "Hiroshi Ishikawa" "Jose Meseguer" "Takuo Watanabe" "Kokichi Futatsugi" "Hideyuki Nakashima" "On the semantics of {GAEA}---an object-oriented specification of a concurrent reflective language in rewriting logic" "IMSA'97" "1997" "70-109" "Information-Technology Promotion Agency, Japan" "Hideyuki Nakashima" "Organic programming for situation-thick {AI} systems" "IMSA'97" "1997" "156-163" "Information-Technology Promotion Agency, Japan" "Analysis of meta-programs" "Patricia Hill" "John Lloyd" "1989" "Meta-Programming in Logic Programming" "H. D. Abramson" "M. H. Rogers" "MIT Press" "23-52" "Program transformation with metasystem transitions" "Valentin F. Turchin" "1993" "Journal of Functional Programming" "3" "3" "283-313" "Microsoft Corporation" "The {COM} Specificication" "1995" "Common Object Model Specification" "Microsoft Corp." "Digital Equipment Corp." "1994" "{OMG} Document 94.10.9" "The Common Object Request Broker: Architecture and Specification" "Object Management Group" "1993" "{OMG} Document 93-12-43" "J. R. Abrial" "Steam-boiler control specification problem" "1994" "Distributed to the participants of a {D}agstuhl seminar on {'}Methods for {S}emantics and {S}pecification{'}. Available via url{http://www.informatik.uni-kiel.de/~{ }procos/dag9523/dag9523.html}" "See also {'}Additional Information Concerning the Physical Behaviour of the Steam-boiler{'} at the same address" "A. Agarwal" "Limits on Interconnection Network Performance" "{IEEE} Transactions on Parallel and Distributed Systems" "1991" "4" "2" "398-412" "Rajeev Alur" "David Dill" "The Theory of Timed Automata" "Real-Time: Theory in Practice" "J. W. de Bakker" "G. Huizing" "W. P. de Roever" "G. Rozenberg" "Lecture Notes in Computer Science" "600" "1991" "T. A. Henzinger" "Z. Manna" "A. Pnueli" "Timed Transition Systems" "Real-Time: Theory in Practice" "J. W. de Bakker" "G. Huizing" "W. P. de Roever" "G. Rozenberg" "Lecture Notes in Computer Science" "600" "1991" "L. Bachmair" "Proof by Consistency in Equational Theories" "Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK)" "1988" "228-233" "L. Bachmair" "Proof methods for equational theories" "University of Illinois, Urbana-Champaign" "1987" "L. Bachmair" "Completion for Rewriting modulo a Congruence" "Theoretical Computer Science" "1989" "67" "173-201" "L. Bachmair" "N. Dershowitz" "J. Hsiang" "Completion Without Failiure" "H. A{\"i}t-Kaci" "M. Nivat" "Resolution of Equations in Algebraic Structures" "Rewriting Techniques" "2" "1" "Academic Press" "1989" "H. P. Barendregt" "The Lambda Calculus, its Syntax and Semantics" "North Holland, Amsterdam, 2nd ed." "1984" "H. P. Barendregt" "Handbook of Logic in Computer Science" "Typed lambda calculi" "1993" "Oxford Univ. Press" "eds. Abramsky et al." "L. Bachmair" "Canonical equational proofs" "Birkh{\"a}user Verlag AG" "1991" "Computer Science Logic, Progress in Theoretical Computer Science" "E. Bevers" "J. Lewi" "Proof by Consistency in Conditional Equational Theories" "Proceedings Second International Workshop on Conditional and Typed Rewriting Systems" "1990" "Springer-Verlag" "Lecture Notes in Computer Science" "516" "194-205" "K. Becker" "Proving Ground Confluence and Inductive Validity in Constructor Based Equational Specifications" "Lecture Notes in Computer Science" "Proceedings from TAPSOFT'93: Theory and Practice of Software Development (Orsay France)" "1993" "668" "46-60" "J. A. Bergstra" "J. V. Tucker" "Initial and Final Algebra Semantics for Data Type Specificartions: Two Characterization Theorems" "SIAM Journal on Computing" "1983" "12" "2" "366-387" "G. Birkhoff" "On the structure of abstract algebras" "Proc. Cambridge Philosophical Society 31" "1935" "433-454" "A. Boudet" "E. Contejean" "{AC}-unification is easy" "Laboratoire de Recherche en Informatique, Universite Paris-Sud, Orsay, France" "April1989" "R. S. Boyer" "J. S. Moore" "A Computational Logic Handbook" "Academic Press, Inc." "1988" "V. Breazu-Tannen" "Combining Algebra and Higher-Order Types" "Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK)" "1988" "July" "V. Breazu-Tannen" "J. Gallier" "Polymorphic Rewriting Conserves Algebraic Strong Normalization and Confluence" "Lecture Notes in Computer Science" "Proceedings 16th International Colloquium on Automata, Languages and Pro-gramming" "1988" "Springer-Verlag" "372" "137-150" "R. Burstall" "Proving Properties of Programs by Structural Induction" "Computer Journal" "1969" "12(1)" "41-48" "H.-J. B{\"u}rckert" "Solving Disequations in Equational Theories" "Lecture Notes in Computer Science" "Proceedings 9th International Conference on Automated Deduction, Argonne (Illinois, USA)" "1988" "310" "517-526" "J. Chabin" "P. R{'e}ty" "Narrowing directed by a graph of terms" "Lecture Notes in Computer Science" "Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy)" "1991" "488" "112-123" "K. M. Chandy" "J. Misra" "Parallel Program Design: {A} Foundation" "Addison-Wesley" "1988" "J. Christian" "Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (NY, USA)" "Some Termination Criteria for Narrowing and {E}-Narrowing" "1992" "Lecture Notes in Artificial Intelligence" "Springer-Verlag" "607" "E. M. Clarke" "Verification of the Futurebus+Cache Coherence Protocol" "H. Comon" "P. Lescanne" "Equational Problems and Disunification" "Journal of Symbolic Computation" "1989" "7" "371-425" "H. Comon" ". Haberstrau M" "J.-P. Jouannaud" "Proceedings 7th IEEE Symposium on Logic in Computer Science, Santa Cruz, (California, USA)" "Decidable Problems in Shallow Equational Theories" "1992" "255-265" "O.-J. Dahl" "D. F. Langmyhr" "O. Owe" "Preliminary Report on the Specification and Programming Language {ABEL}" "Department of informatics, University of Oslo, Norway" "1986" "Research Report" "106" "O.-J. Dahl" "O. Owe" "Formal Development with {ABEL}" "Department of informatics, University of Oslo, Norway" "1991" "Research Report" "552" "O.-J. Dahl" "O. Owe" "Proceedings 4th International Symposium of VDM Europe" "Formal Development with {ABEL}" "1991" "Lecture Notes in Computer Science" "Springer-Verlag" "552" "O.-J. Dahl" "Verifiable Programming" "Prentice Hall" "1992" "N. Dershowitz" "Orderings for term-rewriting systems" "Theoretical Computer Science" "1982" "17" "279-301" "N. Dershowitz" "Termination of rewriting" "Journal of Symbolic Computation" "1987" "3" "69-116" "N. Dershowitz" "Completion and Its Applications" "H. A{\"i}t-Kaci" "M. Nivat" "Resolution of Equations in Algebraic Structures" "Rewriting Techniques" "2" "2" "Academic Press" "1989" "N. Dershowitz" "Open Problems in Rewriting" "Lecture Notes in Computer Science" "Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy)" "1991" "488" "445-456" "N. Dershowitz" "M. Okada" "G. Sivakumar" "Confluence of Conditional Rewrite Systems" "Proceedings 1st International Workshop on Conditional Term Rewriting Systems, Orsay (France)" "1987" "Springer-Verlag" "Lecture Notes in Computer Science" "308" "31-44" "N. Dershowitz" "L. Marcus" "A. Tarlecki" "Existence, Uniqueness and Construction of Rewrite Systems" "SIAM Journal on Computing" "1988" "4" "629-639" "N. Dershowitz" "J.-P. Jouannaud" "Rewrite Systems" "J. van Leeuwen" "Handbook of Theoretical Computer Science" "B" "6" "Elsevier, Amsterdam" "1990" "N. Dershowitz" "C. Hoot" "Topics in Termination" "Proceedings 5th Conference on Rewriting Techniques and Applications, Montreal (Canada)" "1993" "Springer-Verlag" "Lecture Notes in Computer Science" "690" "198-212" "H. Devie" "Linear Completion" "Proceedings Second International Workshop on Conditional and Typed Rewriting Systems" "1990" "Springer-Verlag" "Lecture Notes in Computer Science" "516" "233-245" "H. Devie" "Proce'dures de comple'tion e'quationnelle" "Universite' de Paris-Sud" "1991" "On Completeness of Narrowing Strategies" "R. Echahed" "Theoretical Computer Science" "1990" "72" "133-146" "Uniform Narrowing Strategies" "R. Echahed" "Proceedings 3rd International Conference on Algebraic and Logic Programming, Pisa (Italy)" "Lecture Notes in Computer Science" "Springer-Verlag" "632" "1992" "259-275" "H. Ehrig" "B. Mahr" "Fundamentals of Algebraic Specifications {I}, Equations and Initial Semantics" "Springer-Verlag" "1985" "EATCS Monographs on Theoretical Computer Science" "6" "Overview of algebraic specification languages, environments and tools, and algebraic specification of software systems" "H. Ehrig" "I. Cla{ss}en" "Bulletin of European Association for Theoretical Computer Science" "1989" "39" "103-111" "The {AFFIRM} Theorem prover: Proof Forests and Management of Large Proofs" "R. W. Erickson" "D. L. Musser" "Proceedings 5th International Conference on Automated Deduction" "Lecture Notes in Computer Science" "87" "1980" "220-231" "Complete Sets of Unifiers and Matchers in Equational Theories" "F. Fages" "G. Huet" "Theoretical Computer Science" "1986" "43" "189-200" "M. Fay" "First-order Unification in an Equational Theory" "Proceedings of the 4th Workshop on Automated Deduction" "1979" "161-167" "Narrowing Based Procedures for Equational Disunification" "M. Fern{'a}ndez" "Applicable Algebra in Engineering, Communication and Computation" "1992" "3" "1-26" "M. C. F. Ferreira" "H. Zantema" "Well-foundedness of Term Orderings" "Proceedings 4th International Workshop on Conditional Term Rewriting Systems, Jesuralem (Israel)" "1994" "To be published by Springer Verlag" "U. Fraus" "H. Hussmann" "A Narrowing-Based Theorem Prover" "Distributed at 2nd International Conference on Algebraic and Logic Programming, Nancy (France)" "October" "1990" "L. Fribourg" "A Narrowing Procedure for Theories with Constructors" "Proceedings 7th International Conference on Automated Deduction, Napa (CA, USA)" "Springer-Verlag" "Lecture Notes in Computer Science" "170" "1984" "259-281" "L. Fribourg" "Handling Function Definitions through Innermost Superposition and Rewriting" "Proceedings 1st Conference on Rewriting Techniques and Applications, Dijon (France)" "Springer-Verlag" "Lecture Notes in Computer Science" "202" "1985" "325-344" "L. Fribourg" "{SLOG:} {A} Logic Programming Interpreter Based on Clausal Superposition and Rewriting" "Proceedings of the 1985 Symposium on Logic Programming, Boston" "1985" "172-184" "L. Fribourg" "A Strong Restriction on the Inductive Completion Procedure" "Proceedings 13th International Colloquium on Automata, Languages and Pro-gramming" "1986" "Springer-Verlag" "Lecture Notes in Computer Science" "226" "105-115" "{D. de} Frutos-Escrig" "M.-I. Fern{'a}ndes-Camacho" "On Narrowing Strategies for Partial Non-Strict Functions" "Proceedings from TAPSOFT'91: Theory and Practice of Software Development" "1991" "Springer-Verlag" "Lecture Notes in Computer Science" "494" "416-437" "H. Ganzinger" "A Completion Procedure for Conditional Equations" "Proceedings 1st International Workshop on Conditional Term Rewriting Systems, Orsay (France)" "1987" "Springer-Verlag" "Lecture Notes in Computer Science" "308" "62-83" "H. Ganzinger" "J. Stuber" "Inductive Theorem Proving by Consistency for First-Order Clauses" "Proceedings 3rd International Workshop on Conditional Term Rewriting Systems, Pont-a-Mousson (France)" "1993" "Springer-Verlag" "Lecture Notes in Computer Science" "656" "226-241" "S. J. Garland" "J. V. Guttag" "Inductive Methods for Reasoning about Abstract Data Types" "Proceedings of the fifteenth annual ACM Symposium on Principles of Programming Languages" "January 1988" "219-228" "S. J. Garland" "J. V. Guttag" "An Overwiew of {LP}, The {L}arch {P}rover" "Proceedings 3rd Conference on Rewriting Techniques and Applications, Chapel Hill (North Carolina, USA)" "137-151" "1989" "Springer-Verlag" "Lecture Notes in Computer Science" "355" "N. Dershowitz" "April" "V. Girranata" "F. Gimona" "U. Montanari" "Observability Concepts in abstract data type specification" "Proceedings 1st Mathematical Foundations of Computer Science, Gdansk (Poland)" "1976" "Springer-Verlag" "Lecture Notes in Computer Science" "45" "576-587" "S. Gjessing" "S. Krogdahl" "E. Munthe-Kaas" "A Top Down Approach to the Formal Specification of {SCI} Cashe Coherence" "Department of informatics, University of Oslo, Norway" "1990" "Research Report" "146" "S. Gjessing" "S. Krogdahl" "E. Munthe-Kaas" "A Linked List Cache Coherence Protocol: Verifying the Bottom Layer" "Proceedings of the 5th International Parallel Processing Symposium, Anaheim (California)" "324-329" "V. K. Prasanna Kumar" "IEEE Computer Society Press" "1991" "I. Gnaedig" "Termination of order-sorted rewriting" "Proc. Algebraic and Logic Programming. Third International Conference" "Springer-Verlag" "1992" "J. A. Goguen" "J. W. Thatcher" "E. G. Wagner" "An initial algebra approach to the specification, correctness and implementation of abstract data types" "Current Trends in Programming Methodology" "R. Yeh" "80-149" "Prentice-Hall" "1978" "J. A. Goguen" "Exception and Error sorts, Coercion and Overload Operations" "SRI International,Computer Science Lab" "1978" "Equality, Types, Modules, and (why not?) Generics for Logic Programming" "J. A. Goguen" "J. Meseguer" "Journal of Logic Programming" "1984" "2" "179-210" "J. A. Goguen" "{OBJ} as a theorem prover with applications to hardware verification" "SRI International,Computer Science Lab" "1988" "J. A. Goguen" "T. Winkler" "Introducing {OBJ3}" "SRI International,Computer Science Lab" "1988" "J. A. Goguen" "J. Meseguer" "Order-Sorted Algebra {I}: {E}quational Deduction for Multiple Inheritance, Overloading, Exceptions and Partial Operators" "Programming Research Group, Oxford University Computing Laboratory" "1989" "J. A. Goguen" "How to prove inductive hypotheses without induction" "Proceedings of the 5th Conference on Automated Deduction" "1980" "Springer-Verlag" "Lecture Notes in Computer Science" "87" "356-373" "W. Bibel" "R. Kowalski" "J. A. Goguen" "Parameterized Programming" "IEEE Transactions on Software Engineering" "1984" "September" "SE-10(5)" "528-543" "J. V. Guttag" "The Specification and Application to Programming of Abstract Data Types" "Computer Science Department, University of Toronto" "1975" "The Algebraic Specification of Abstract Data Types" "J. V. Guttag" "J. J. Horning" "Acta Informatica" "1978" "10" "27-52" "Larch in Five easy Pieces" "J. V. Guttag" "J. J. Horning" "J. M. Wing" "Digital Systems Research Center" "1985" "R. Hennicker" "Observational Implementations" "Springer-Verlag" "Lecture Notes in Computer Science" "Proceedings of the 6th Annual Symposium on Theoretical Aspects of Computer Science" "349" "59-71" "1989" "Context Induction: {A} Proof Principle for Behavioural Abstractions and Algebraic Implementations" "R. Hennicker" "Formal Aspects of Computing" "1991" "3" "326-345" "Verifying a distributed list system: a case history" "S. Krogdahl" "O. Lysne" "Formal Aspects of Computing" "1997" "9" "98-118" "M. Hermann" "On Proving Properties of Completion Strategies" "Springer-Verlag" "Lecture Notes in Computer Science" "Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy)" "488" "398-410" "1991" "R. Hindley" "J. Seldin" "1986" "Introduction to Combinators and $lambda$-calculus" "Cambridge University Press" "C. A. R. Hoare" "Communicating Sequential Processes" "Prentice-Hall" "1985" "G. Hornung" "P. Raulefs" "Terminal Algebra Semantics and Retractions for Abstract Data Types" "Lecture Notes in Computer Science" "85" "310-323" "July 1980" "J. Hsiang" "M. Rusinowitch" "On word problems in equational theories" "Proceedings 14th International Colloquium on Automata, Languages and Pro-gramming, Karlsruhe (Germany)" "1987" "Springer-Verlag" "Lecture Notes in Computer Science" "267" "54-71" "T. Ottmann" "July" "G. Huet" "June" "1975" "A unification algorithm for typed $lambda$-calculus" "Theoretical Computer Science" "1" "1" "27-57" "G. Huet" "A Complete proof of correctness of the {K}nuth and {B}endix completion algorithm" "Journal of Computer and System Sciences" "1981" "23(1)" "11-21" "G. Huet" "J.-M. Hullot" "Proofs by Induction in Equational Theories with Constructors" "Journal of Computer and System Sciences" "1982" "239-266" "J.-M. Hullot" "Canonical Forms and Unification" "Proceedings 5th International Conference on Automated Deduction" "Lecture Notes in Computer Science" "Springer-Verlag" "87" "318-334" "1980" "P. Inverardi" "M. Nesi" "A Rewriting Strategy to Verify Observational Congruence" "Information Processing Letters" "35" "191-199" "1990" "{IEEE working group P1596}" "{IEEE} Standard for {S}calable {C}oherent {I}nterface {(SCI)}" "{IEEE}" "August" "1992" "D. V. James" "A. T. Laundrie" "S. Gjessing" "G. S. Sohi" "New Directions in Scalable Shared-Memory Mulitprocessor Architectures: {S}calable {C}oherent {I}nterface" "{IEEE} Computer" "1990" "June" "R. E. Johnson" "How to Get a Paper Accepted at {OOPSLA}" "1993" "J.-P. Jouannaud" "E. Kounalis" "Automatic Proofs by Induction in Theories without Constructors" "82" "Information and Computation" "1-33" "1" "1989" "July" "J.-P. Jouannaud" "H. Kirchner" "Completion of a Set of Rules modulo a Set of Equations" "SIAM Journal of Computing" "1055-1094" "15" "4" "1986" "November" "J.-P. Jouannaud" "C. March'e" "Completion modulo Associativity, Commutativity and Identity ({AC1})" "Springer-Verlag" "Lecture Notes in Computer Science" "Proceedings of DISCO'90, Capri (Italy)" "429" "111-120" "1990" "J.-P. Jouannaud" "M. Okada" "A Computation Model for Executable Higer-Order Algebraic Specification Languages" "Proceedings 6th IEEE Symposium on Logic in Computer Science" "1991" "350-361" "S. Kamin" "J.-J. L{'e}vy" "Attempts for generalizing the recursive path ordering" "INRIA" "1980" "Rocquencourt" "S. Kamin" "J.-J. L{'e}vy" "Two generalizations of the recursive path ordering" "1980" "Unpublished Note, Department of Computer Science, University of Illinois, Urbana, IL" "S. Kamin" "Final data types and their specification" "ACM Transactions on Programming Languages and Systems" "5" "1" "1983" "January" "97-123" "S. Kaplan" "Conditional Rewrite Rules" "Theoretical Computer Science" "33" "1984" "175-193" "S. Kaplan" "Positive/Negative Conditional Rewriting" "Proceedings 1st International Workshop on Conditional Term Rewriting Systems, Orsay (France)" "1987" "Springer-Verlag" "Lecture Notes in Computer Science" "308" "129-141" "D. Kapur" "P. Narendran" "H. Zhang" "Proof by Induction using Test Sets" "Springer-Verlag" "Lecture Notes in Computer Science" "Proceedings 8th International Conference on Automated Deduction, Oxford (UK)" "230" "99-117" "1986" "D. Kapur" "P. Narendran" "H. Zhang" "On Sufficient-Completeness and Related Properties of Term Rewriting Systems" "Acta Informatica" "24" "4" "395-415" "1987" "Proof by consistency" "D. Kapur" "R. Musser" "Artificial Intelligence" "31" "1987" "125-157" "J. H. Kim" "A. A. Chien" "The Impact of Packetization in Wormhole-Routed Networks" "Springer-Verlag" "Lecture Notes in Computer Science" "Proceedings 5th Conference of Parallel Architectures and Languages Europe" "694" "242-253" "1993" "C. Kirchner" "P. Lescanne" "Solving Disequations" "Proceedings 2nd IEEE Symposium on Logic in Computer Science, Ithaca (New York, USA)" "347-352" "1987" "H. Kirchner" "Proofs in Parameterized Specifications" "Springer-Verlag" "Lecture Notes in Computer Science" "Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy)" "488" "174-187" "1991" "Deduction with Symbolic Constraints" "K. Kirchner" "H. Kirchner" "M. Rusinowitch" "Revue d'intelligence artificielle" "4" "3" "1990" "9-52" "J. W. Klop" "{it Combinatory Reduction Systems}" "Mathematical Centre Tracts 127, Mathematisch Centrum,Amsterdam" "1980" "D. E. Knuth" "P. B. Bendix" "Simple word problems in universal algebras" "Computational Problems in Abstract Algebra" "Pergamon Press" "1970" "J. Leech" "263-297" "Oxford" "Timed Rewriting Logic" "P. Kosiuczenko" "M. Wirsing" "1995" "Working material for the 1995 {M}arktoberdorf {I}nternational {S}ummer {S}chool ``{L}ogic of {C}omputation''" "P. Kosiuczenko" "M. Wirsing" "Timed Rewriting Logic with an Application to Object-Oriented Specification" "Submitted for publication" "1995" "E. Kounalis" "M. Rusinowitch" "Mechanizing inductive reasoning" "Proceedings Eighth National Conference on Artificial Intelligence, Boston" "240-245" "1990" "Verification of a Class of Link-Level Protocols" "S. Krogdahl" "BIT" "1978" "18" "436-448" "W. K{\"u}chlin" "Inductive Completion by Ground Proof Transformation" "H. A{\"i}t-Kaci" "M. Nivat" "Resolution of Equations in Algebraic Structures" "Rewriting Techniques" "2" "7" "Academic Press" "1989" "L. Lamport" "The '{H}oare Logic' of Concurrent Programs" "Acta Informatica" "1980" "14" "21-37" "D. S. Lankford" "Canonical inference" "Department of Mathematics and Computer Science, Univ. of Texas, Austin" "ATP-32" "1975" "P. Lescanne" "Computer experiments with the {REVE} term rewriting system generator" "Proceedings of 10th ACM Symposium on Principles of Programming Languages" "1983" "99-108" "ACM" "P. Lescanne" "Behavioural Categoricity of Abstract Data Type Specifications" "The Computer Journal" "1983" "26" "4" "289-292" "P. Lescanne" "Implementation of completion by transition rules + control: {{sc ORME}}" "Proceedings 2nd International Conference on Algebraic and Logic Programming, Nancy (France)" "1990" "Springer-Verlag" "Lecture Notes in Computer Science" "463" "262-269" "H. Kirchner" "W. Wechler" "C. Lor{'i}a-S{'a}enz" "J. Steinbach" "Termination of Combined (Rewrite and $lambda$-Calculus) Systems" "Proceedings 3rd International Workshop on Conditional Term Rewriting Systems, Pont-a-Mousson (France)" "Springer-Verlag" "Lecture Notes in Computer Science" "656" "143-147" "1992" "C. Lor{'i}a-S{'a}enz" "A Theoretical Framework for Reasoning about Program Con-struction based on Extensions of Rewrite Systems" "Fachbereich Informatik der Universit{\"a}t Kaiserslautern" "1993" "O. Lysne" "Syntaksorientert Editor Basert p{\aa} 2-niv{\aa} {BNF}" "Department of Informatics, University of Oslo, Norway" "1988" "O. Lysne" "A width first approach to completion" "Proceedings from NIK'90: Norsk Informatikk Konferanse, Bergen" "TAPIR" "145-154" "November" "1990" "O. Lysne" "A width first approach to completion" "Department of informatics, University of Oslo, Norway" "1990" "Research Report" "139" "March" "O. Lysne" "Term Rewriting Techniques for Systems based on Generator Induction" "Department of Informatics, University of Oslo, Norway" "1991" "Research Report 163" "O. Lysne" "Proof by Consistency in Constructive Systems with Final Algebra Semantics" "Springer-Verlag" "Lecture Notes in Computer Science" "Proceedings 3rd International Conference on Algebraic and Logic Programming, Pisa (Italy)" "632" "276-290" "1992" "O. Lysne" "O. Owe" "Definedness and Strictness in Generator Inductive Definitions" "Department of informatics, University of Oslo, Norway" "1991" "Research Report" "161" "October" "Also presented at the 3rd Nordic Workshop on Program Correctness, G{\"o}teborg (Sweden)" "O. Lysne" "Towards Mechanizing Proofs by Structural Induction" "Proceedings from NIK'92: Norsk Informatikk Konferanse, Troms{o}" "243-255" "TAPIR" "November" "1992" "The Equational Part of Proofs by Structural Induction" "O. Lysne" "BIT" "1993" "33" "596-618" "O. Lysne" "Linear Proofs in the Final Algebra" "Department of informatics, University of Oslo, Norway" "1993" "Research Report" "173" "April" "O. Lysne" "Initial Equality as a Function in Algebraic Specification" "Department of informatics, University of Oslo, Norway" "1993" "Research Report" "179" "September" "O. Lysne" "{E}-Unification by Consistency" "Presented at the 5th Nordic Workshop on Program Correctness, Turku (Finland)" "1993" "O. Lysne" "On the Connection between Narrowing and Proof by Consistency" "Springer-Verlag" "Lecture Notes in Artificial Intelligence" "Proceedings 12th International Conference on Automated Deduction, Nancy (France)" "814" "133-147" "1994" "O. Lysne" "Heuristics for Completion in Automatic Proofs by Structural Induction" "Nordic Journal of Computing" "1994" "1" "135-156" "O. Lysne" "Extending {B}achmair's method for proof by consistency to the final algebra" "Information Processing Letters" "1994" "51" "303-310" "O. Lysne" "{it E}-Unification by Consistency" "{AA}bo Akademi" "Reports on Computer Science & Mathematics" "Proceedings 5th Nordic Workshop on Program Correctness" "18" "127-136" "1994" "O. Lysne" "J. Piris" "A Termination Ordering for Higher Order Rewrite Systems" "To be presented at {it Rewriting techniques and Applications '95}. Proceedings to be published by Springer Verlag in the series LNCS" "1995" "S. Krogdahl" "O. Lysne" "Verifying a Distributed List System: {A} Case History" "Department of informatics, University of Oslo, Norway" "1993" "Research Report" "182" "December" "K. L. McMillan" "J. Schwalbe" "Formal Verification of the {G}igamax Cache Consistency Protocol" "Proceedings of the International Symposium on Shared Memory Multiprocessing, Tokyo (Japan)" "April" "1991" "242-251" "An Efficient Unification Algorithm" "A. Martelli" "U. Montanari" "Transactions on Programming Languages and Systems" "1982" "April" "4(2)" "258-282" "J. Meseguer" "J. A. Goguen" "Initiality, Induction and Computability" "M. Nivat" "J. C. Reynolds" "Algebraic Methods in Semantics" "14" "Cambridge University Press" "1985" "Conditional rewriting logic as a unified model of concurrency" "J. Meseguer" "Theoretical Computer Science" "1992" "96" "73-155" "J. Meseguer" "T. Winkler" "Parallel programming in {M}aude" "Research {D}irections in {H}igh-{L}evel {P}arallel {P}rogramming {L}anguages" "Lecture Notes in Computer Science" "Springer-Verlag" "574" "1992" "253-293" "R. Bruni" "J. Meseguer" "U. Montanari" "V. Sassone" "A Comparison of Petri Net Semantics under the Collective Token Philosophy" "Proceedings of {ASIAN'98}, 4th Asian Computing Science Conference" "J. Hsiang" "A. Ohori" "Lecture Notes in Computer Science" "Springer-Verlag" "1538" "1998" "225-244" "A Logic Programming Language with Lambda-Abstraction Function Variables, and Simple Unification" "D. Miller" "Journal of Logic and Computation" "1991" "1" "4" "497-536" "A Calculus of Mobile Processes ({P}arts {I} and {II})" "R. Milner" "J. Parrow" "D. Walker" "Information and Computation" "1992" "100" "1-77" "R. Milner" "Communication and Concurrency" "Prentice-Hall" "1989" "P. D. Mosses" "The Use of Sorts in Algebraic Specifications" "Recent trends in Data Type Specification, 8th WADT, August 1991" "M. Bidoit" "C. Choppy" "66-91" "Lecture Notes in Computer Science" "Springer-Verlag" "655" "1993" "Final algebras, cosemicomputable algebras and degrees of unsolvability" "L. S. Moss" "J. Meseguer" "J. A. Goguen" "Theoretical Computer Science" "1992" "100" "267-302" "On proving inductive properties in abstract data types" "D. L. Musser" "Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages" "1980" "January" "154-162" "T. Nipkow" "Higher Order Critical Pairs" "Proceedings 6th IEEE Symposium on Logic in Computer Science" "1991" "342-349" "W. Nutt" "P. R{'e}ty" "G. Smolka" "Basic Narrowing Revisited" "Journal of Symbolic Computation" "1989" "7" "295-317" "F. Orejas" "Implementation and Behavioural Equivalence: {A} Survey" "Recent trends in Data Type Specification" "Lecture Notes in Computer Science" "Springer-Verlag" "655" "1991" "J. Ostroff" "Formal Methods for the Specification and Design of Real-Time Safety-Critical Systems" "Journal of Systems and Software" "Elsevier" "1992" "33-60" "O. Owe" "A specification Technique with Idealization" "Department of informatics, University of Oslo, Norway" "1980" "March" "O. Owe" "Axiomatic Treatment of Processes with Shared Variables Revisited" "Formal Aspects of Computing" "1992" "4" "323-340" "O. Owe" "O.-J. Dahl" "Generator Induction in Ordered Sorted Algebras" "Formal Aspects of Computing" "1991" "3" "2-20" "P. Padawitz" "Strategy-Controlled Reduction and Narrowing" "Proceedings 2nd Conference on Rewriting Techniques and Applications, Bordeaux (France)" "1987" "Springer-Verlag" "Lecture Notes in Computer Science" "256" "242-255" "Complete Sets of Reductions for Some Equational Theories" "G. E. Peterson" "M. E. Stickel" "Journal of the Association Computing Machinery" "1981" "28" "2" "233-264" "Semantic Confluence Tests and Completion Methods" "D. Plaisted" "Information and Control" "1985" "65" "182-215" "D. Plaisted" "A Logic for Conditional Term Rewriting Systems" "Proceedings 1st International Workshop on Conditional Term Rewriting Systems, Orsay (France)" "1987" "Springer-Verlag" "Lecture Notes in Computer Science" "308" "212-227" "J. van de Pol" "Termination Proofs for Higher-order Rewrite Systems" "First International Workshop on Higher-Order Algebra, Logic and Term Rewriting" "1993" "Springer-Verlag" "Lecture Notes in Computer Science" "816" "305-325" "L. Puel" "Proceedings 9th Colloquium on Trees in Algebra and Programming" "1984" "B. Courcelle" "Cambridge University Press" "227-242" "Proof in the Final Algebra" "Z. Qian" "Linear Unification of Higher-Order Patterns" "Proceedings TAPSOFT'93" "1993" "Springer-Verlag" "Lecture Notes in Computer Science" "668" "391-405" "U. S. Reddy" "Term Rewriting Induction" "Proceedings 10th International Conference on Automated Deduction, Kaiserslautern (Germany)" "1990" "Springer-Verlag" "Lecture Notes in Computer Science" "449" "162-177" "P. R{'e}ty" "C. Kirchner" "H. Kirchner" "P. Lescanne" "{NARROWER:} a new algorithm for unification and its application to Logic Programming" "Proceedings 1st Conference on Rewriting Techniques and Applications, Dijon (France)" "1985" "Springer-Verlag" "Lecture Notes in Computer Science" "202" "141-155" "P. R{'e}ty" "Improving basic narrowing techniques" "Proceedings 2nd Conference on Rewriting Techniques and Applications, Bordeaux (France)" "1987" "Springer-Verlag" "Lecture Notes in Computer Science" "256" "228-241" "J. A. Robinson" "A machine-oriented logic based on the resolution principle" "Journal of the Association Computing Machinery" "1965" "12" "1" "23-41" "W. Snyder" "J. H. Gallier" "Higher Order unification Reviseted : Complete Sets of Transformations" "Journal of Symbolic Computation" "8" "101-140" "1989" "M. Stickel" "A unification algorithm for associative-commutative functions" "Journal of the Association Computing Machinery" "1981" "28" "3" "423-434" "M. Wirsing" "J. A. Bergstra" "Algebraic Methods: Theory, Tools and Applications" "Springer-Verlag" "1989" "394" "Lecture Notes in Computer Science" "M. Wirsing" "Algebraic Specification" "J. van Leeuwen" "Handbook of Theoretical Computer Science" "B" "13" "Elsevier, Amsterdam" "1990" "K. A. Yelick" "Using Abstraction in Explicitly Parallel Programs" "Massachusetts Institute of Technology" "1990" "Jia-Huai You" "Outer Narrowing for Equational Theories Based on Constructors" "Proceedings 15th International Colloquium on Automata, Languages and Pro-gramming, Tampere (Finland)" "1988" "Springer-Verlag" "Lecture Notes in Computer Science" "317" "727-741" "R. Bruni" "J. Meseguer" "U. Montanari" "Executable Tile Specifications for Process Calculi" "Proc. of FASE'99, 2nd Intl. Conf. on Fundamental Approaches to Software Engineering" "1992" "Springer-Verlag" "Lecture Notes in Computer Science" "1577" "60-76" "D. Harel" "From play-in scenarios to code: an achievable dream" "Proc. of FASE'00, 3rd Intl. Conf. on Fundamental Approaches to Software Engineering" "2000" "Springer-Verlag" "Lecture Notes in Computer Science" "1783" "22-34" "H. Zantema" "Termination of term rewriting by interpretation" "Proceedings 3rd International Workshop on Conditional Term Rewriting Systems, Pont-a-Mousson (France)" "1992" "Springer-Verlag" "Lecture Notes in Computer Science" "656" "155-167" "P. C. {O}lveczky" "Terminering av typeordnet omskrivning" "Department of informatics, University of Oslo, Norway" "1994" "P. C. {O}lveczky" "Termination of order-sorted rewriting" "Proceedings of the 6th {N}ordic {W}orkshop on {P}rogramming {T}heory, {A}arhus, {D}enmark" "1995" "To appear" "Peter Csaba {\"O}lveczky" "Piotr Kosiuczenko" "Martin Wirsing" "An Object-Oriented Algebraic Steam-Boiler Control Specification" "The Steam-Boiler Case Study Book" "Jean-Raymond Abrial" "Egon B{\"o}rger" "Hans Langmaack" "379-402" "Springer-Verlag" "1996" "Vol. 1165" "R. Jagannathan" "Coarse-Grain Parallel Programming of Conventional Parallel Computers Advanced Topics in Dataflow Computing and Multithreading" "IEEE Computer Society Press" "1995" "L. Bic, J-L. Gaudiot, G. Gao (Editors)" "ECSD98" "H.-D. Ehrich" "C. Caleiro" "A Sernadas" "G. Denker" "{Logics for Specifying Concurrent Information Systems}" "Logics for Databases and Information Systems" "J. Chomicki" "G. Saake" "Kluwer Academic Publishers" "1998" "167-198" "G. Denker" "H.-D. Ehrich" "{Specifying Distributed Information Systems: Fundamentals of an Object-Oriented Approach Using Distributed Temporal Logic}" "{Formal Methods for Open Object-Based Distributed Systems (FMOODS'97), Volume 2, IFIP TC6 WG6.1 Intern. Workshop, 21-23 July, Canterbury, Kent, UK}" "1997" "H. Bowman" "J. Derrick" "89-104" "" "Chapman & Hall" "" "" "" "Ehr96" "H.-D. Ehrich" "{Object Specification}" "TU Braunschweig" "{Informatik-Bericht}" "96--07" "1996" "G. Denker" "{dtlplus: A Distributed Temporal Logic Supporting Several Communication Principles}" "SRI International, Computer Science Laboratory" "{Technical Report}" "1998" "{}" "333 Ravenswood Ave, Menlo Park, CA 94025" "" "{em To appear}" "G. Denker" "J. Meseguer" "C. Talcott" "{Protocol Specification and Analysis in Maude}" "{Proc. of Workshop on Formal Methods and Security Protocols, 25 June 1998, Indianapolis, Indiana}" "1998" "N. Heintze" "J. Wing" "" "" "" "" "" "" "G. Denker" "J. Millen" "{{CAPSL} intermediate language}" "{Proc. of Workshop on Formal Methods and Security Protocols, July 1999, Trento, Italy}" "1999" "N. Heintze" "E. Clarke" "" "" "" "" "" "url{www.cs.bell-labs.com/who/nch/fmsp99/program.html}" "H.-D. Ehrich" "P. Hartel" "{Temporal Specification of Information Systems}" "{Logic and Software Engineering, Proc. Int. Workshop in Honor of C.S. Tang,Beijing, 14-15 August 1995}" "1996" "A. Pnueli" "H. Lin" "43-71" "" "World Scientific" "" "" "" "ESSS94" "H.-D. Ehrich" "A. Sernadas" "G. Saake" "C. Sernadas" "{Distributed Temporal Logic for Concurrent Object Families}" "R. Wieringa" "R. Feenstra" "Working papers of the International Workshop on Information Systems - Correctness and Reusability" "1994" "Vrije Universiteit Amsterdam, RapportNr. IR-357" "22-30" "Kenneth L. McMillan" "Symbolic Model Checking" "Kluwer Academic Publishers" "Boston, MA" "1993" "David L. Dill" "The {Mur{$phi$}} Verification System" "390-393" "CAV" "Computer-Aided Verification, CAV" "Computer-Aided Verification, CAV" "July/August" "1996" "Rajeev Alur" "Thomas A. Henzinger" "New Brunswick, NJ" "Springer-Verlag" "Lecture Notes in Computer Science" "1102" "J. F. Quesada" "Bidirectional and event-driven parsing with multi-virtual trees" "C. Martin-Vide" "Mathematical and Computational Models in Linguistics" "John Benjamins" "1996" "J. F. Quesada" "The {SCP} parsing algorithm based on syntactic constraints propagation" "University of Seville" "June" "1997" "J. F. Quesada" "Overparsing" "Workshop on Mathematical Linguistics" "Pennsylvania State University, State College" "1998" "J. F. Quesada" "The {SCP} parsing algorithm" "SRI International, Computer Science Laboratory" "{Technical Report}" "1999" "{}" "333 Ravenswood Ave, Menlo Park, CA 94025" "{em To appear}" "J. F. Quesada" "The {Maude} parser: Parsing and meta-parsing $\beta$-extended %context-free grammars" "SRI International, Computer Science Laboratory" "{Technical Report}" "1999" "{}" "333 Ravenswood Ave, Menlo Park, CA 94025" "{em To appear}" "Francisco Dur'an" "Jos'e Meseguer" "The {Maude} Specification of {Full Maude}" "Computer Science Laboratory, SRI International" "February" "1999" "M. J. C. Gordon" "Introduction to {HOL:} {A} Theorem Proving Environment" "Cambridge University Press" "1993" "D. J. Howe" "Semantical Foundations for Embedding {HOL} in {Nuprl}" "Algebraic Methodology and Software Technology" "1996" "Martin Wirsing" "Maurice Nivat" "Springer-Verlag" "Berlin" "Lecture Notes in Computer Science" "1101" "85-101" "C. L. Talcott" "Actor Theories in Rewriting Logic" "1999" "Submitted for publication" "Joseph A. Goguen" "Grant Malcolm" "Software Engineering with {OBJ}: Algebraic Specification in Action" "Software Engineering with OBJ: Algebraic Specification in Action" "Kluwer Academic Publishers, Boston" "Advances in Formal Methods" "2" "ISBN 0-7923-7757-5" "2000" "Joseph A. Goguen" "Timothy Winkler" "Jos'{e} Meseguer" "Kokichi Futatsugi" "Jean-Pierre Jouannaud" "Introducing {OBJ}" "1" "3-167" "Software Engineering with OBJ: Algebraic Specification in Action" "Joseph A. Goguen" "Grant Malcolm" "Kluwer, Boston" "2000" "Victoria Stavridou" "Specifying in {OBJ}, Verifying in {REVE} and Some Ideas about Time" "2" "171-191" "Software Engineering with OBJ: Algebraic Specification in Action" "Joseph A. Goguen" "Grant Malcolm" "Kluwer, Boston" "2000" "Ataru T. Nakagawa" "Kokichi Futatsugi" "Constructing a Graphics System with {OBJ2}: {A} Practical Guide" "3" "193-247" "Software Engineering with OBJ: Algebraic Specification in Action" "Joseph A. Goguen" "Grant Malcolm" "Kluwer, Boston" "2000" "David A. Duce" "Applications of {OBJ} to the Specification of Standards for Computer Graphics" "4" "249-279" "Software Engineering with OBJ: Algebraic Specification in Action" "Joseph A. Goguen" "Grant Malcolm" "Kluwer, Boston" "2000" "Joseph A. Goguen" "Semantic Specifications for the {R}ewrite {R}ule {M}achine" "5" "283-306" "Software Engineering with OBJ: Algebraic Specification in Action" "Joseph A. Goguen" "Grant Malcolm" "Kluwer, Boston" "2000" "Claude Kirchner" "H'{e}l`{e}ne Kirchner" "Aristide M'{e}grelis" "{OBJ} for {OBJ}" "6" "307-330" "Software Engineering with OBJ: Algebraic Specification in Action" "Joseph A. Goguen" "Grant Malcolm" "Kluwer, Boston" "2000" "Eugenio Battiston" "Fiorella De Cindio" "Giancarlo Mauri" "{OBJSA} Nets: {OBJ} and Petri Nets for Specifying Concurrent Systems" "7" "331-360" "Software Engineering with OBJ: Algebraic Specification in Action" "Joseph A. Goguen" "Grant Malcolm" "Kluwer, Boston" "2000" "Kazuhito Ohmaki" "Koichi Takahashi" "Kokichi Futatsugi" "A {LOTOS} Simulator in {OBJ}" "8" "363-395" "Software Engineering with OBJ: Algebraic Specification in Action" "Joseph A. Goguen" "Grant Malcolm" "Kluwer, Boston" "2000" "Joseph A. Goguen" "Grant Malcolm" "More Higher Order Programming in {OBJ3}" "9" "397-408" "Software Engineering with OBJ: Algebraic Specification in Action" "Joseph A. Goguen" "Grant Malcolm" "Kluwer, Boston" "2000" "I. A. Mason" "C. L. Talcott" "Actor Languages: Their Syntax, Semantics, Translation, and Equivalence" "1999" "Theoretical Computer Science" "228" "1" "I. A. Mason" "C. L. Talcott" "A Semantically Sound Actor Translation" "{ICALP'97}" "1997" "Lecture Notes in Computer Science" "1256" "369-378" "C. L. Talcott" "Towards a Toolkit for Actor System Specification" "{AMAST 2000}" "2000" "Lecture Notes in Computer Science" "To appear" "J. Van Baalen" "J. L. Caldwell" "S. Mishra" "Specifying and checking fault-tolerant agent-based protocols using {Maude}" "Formal Approaches to Agent-Based Systems" "2000" "Lecture Notes in Computer Science" "To appear" "M.-O. Stehr" "C. Girault" "R. Valk" "Petri Nets for System Engineering -- A Guide to Modelling, Verification, and Applications" "A Rewriting Semantics for Algebraic Nets" "Springer-Verlag" "2000" "To appear" "M.-O. Stehr" "J. Meseguer" "Pure Type Systems in Rewriting Logic" "Proc. of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999" "url{http://www.cs.bell-labs.com/~felty/LFM99/}" "M.-O. Stehr" "P. Naumov" "J. Meseguer" "A Proof-Theoretic Approach to the {HOL-Nuprl} Connection with Applications to Proof Translation" "Manuscript, SRI International, url{http://www.csl.sri.com/~stehr/fi_eng.html}" "February" "2000" "Seven good reasons for mobile agents" "Danny B. Lange" "Mitsuru Oshima" "Communications of the Association for Computing Machinery" "1999" "42" "March" "88-89" "editor {Giovanni Vigna}" "Mobile Agents and Security" "LNCS 1419" "1998" "David Kotz" "Robert S. Gray" "Mobile Agents and the Future of the {Internet}" "ACM Operating Systems Review" "1999" "August" "33" "3" "7-13" "http://www.cs.dartmouth.edu/~dfk/papers/kotz:future2/" "D. Martin" "A. Cheyer" "D. Moran" "The Open Agent Architecture: {A} framework for building distributed software systems" "Applied Artificial Intelligence" "1999" "13" "91-128" "Available via url{http://www.ai.sri.com/~cheyer/papers/aai/oaa.html}" "Robert S. Gray" "David Kotz" "George Cybenko" "Daniela Rus" "{D'Agents}: Security in a multiple-language, mobile-agent system" "Mobile Agents and Security" "Giovanni Vigna" "1998" "LNCS 1419" "154-187" "Springer-Verlag" "http://agent.cs.dartmouth.edu/papers/gray:security-book.ps.Z" "Danny Lange" "Mitsushuru Oshima" "Programming and Deploying Java Mobile Agents with Aglets" "Addison-Wesley" "1998" "M. Abadi" "A. Gordon" "A Calculus for cryptographic protocols: the spi calculus" "Information and Computation" "1999" "148" "1-70" "An extended version of this paper appears as Research Report 149, Digital Equipment Corporation Systems Research Center, January 1998" "James White" "Telescript technology: the foundation for the electronic marketplace" "1994" "General Magic White Paper, General Magic, Inc." "L. Cardelli" "A. Gordon" "Mobile Ambients" "Proceedings of {FoSSaCS'98}: Foundations of Software Science and Computational Structures" "Lecture Notes in Computer Science" "M. Nivat" "Springer-Verlag" "1378" "1998" "140-155" "To appear in TCS July 2000" "G. C. Roman" "P. J. McCann" "J. Y. Plun" "Mobile {UNITY}: Reasoning and specification in mobile computing" "ACM Transactions on Software Engineering and Methodology" "1997" "6" "250-282" "July" "C. Fournet" "G. Gonthier" "The reflexive {CHAM} and the join-calculus" "1996" "Proceedings of 23rd ACM Symposium on Principles of Programming Languages" "ACM" "52-66" "P. Ciancarini" "A. L. Wolf (eds.)" "Coordination Languages And Models" "1999" "Springer LNCS" "1594" "Anand Tripathi" "Neeran Karnik" "Manish Vora" "Tanvir Ahmed" "Ram Singh" "Mobile Agent Programming in Ajanta" "Proceedings of the 19th International Confernce on Distributed Computing Systems (ICDCS '99)" "1999"