OBJ3/Algebra Bibliography
Papers included herein are on many topics related to the OBJ family of systems, (hidden) (many) order-sorted algebras, category theory, and more.
@COMMENT{ $Id: obj_bib.html 19895 2011-03-02 11:19:21Z kiniry $ }
@COMMENT{ Copyright (C) Joseph R. Kiniry 1996-2000 }
@TechReport{AlencarGoguen91a,
author = { Antonio J. Alencar and Joseph A. Goguen },
title = { Two Examples in { OOZE } },
institution = { Programming Research Group, Oxford University },
year = 1991,
number = { PRG-TR-25-91 }
}
@InProceedings{AlencarGoguen91b,
author = { Antonio Alencar and Joseph Goguen },
title = { { OOZE }: An Object-Oriented { Z } Environment },
booktitle = { Proceedings, European Conference on Object Oriented
Programming },
year = 1991,
volume = 512,
series = lncs,
publisher = pub-sv
}
@TechReport{AlencarGoguen92,
author = { Antonio J. Alencar and Joseph A. Goguen },
title = { { OOZE } with Examples },
institution = { Programming Research Group, Oxford University },
year = 1992,
number = { PRG-TR-7-92 }
}
@InCollection{AndrekaNemeti81,
title = { A General Axiomatizability Theorem Formulated In
Terms Of Cone-Injective Subcategories },
author = { Hajnal Andr{\'e}ka and Istv{\'a}n N{\'e}meti },
booktitle = { Universal Algebra },
editor = { B.~Csakany and E.~Fried and E.T.~Schmidt },
year = 1981,
publisher = { North-Holland },
pages = { 13--35 },
note = { Colloquia Mathematics Societas J{\'a}nos Bolyai, 29
}
}
@InProceedings{ArraisFiadeiro96,
title = { Unifying Theories In Different Institutions },
author = { M. Arrais and J.L. Fiadeiro },
booktitle = { Recent Trends in Data Type Specification },
editor = { Magne Haveraaen and Olaf Owe and Ole-Johan Dahl },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
volume = 1130,
pages = { 81--101 },
year = 1996,
note = { Proceedings of 11th Workshop on Specification of
Abstract Data Types. Oslo, Norway, September 1995 }
}
@InProceedings{AstesianoCerioli93,
title = { Relationships Between Logical Frameworks },
author = { Egidio Astesiano and Maura Cerioli },
booktitle = { Recent Trends in Data Type Specification },
editor = { Michel Bidoit and Christine Choppy },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
volume = 655,
pages = {126--143 },
year = 1993
}
@Article{BanaschewskiHerrlich76,
title = { Subcategories Defined By Implications },
author = { Bernhard Banaschewski and Horst Herrlich },
journal = { Houston Journal Mathematics },
volume = 2,
year = 1976,
pages = { 149--171 }
}
@Book{Barendregt91,
author = { H. P. Barendregt },
title = { The Lambda Calculus },
publisher = { North-Holland },
year = { 1991 },
number = { 103 },
series = { Studies in Logic and the Foundations of Mathematics
},
address = { Amsterdam },
edition = { revised },
ISBN = { 0-444-87508-5 },
}
@PhdThesis{Barros95,
author = { Jos\'e Barros },
title = { Semantics Of Non-Terminating Systems Through Term
Rewriting },
school = { Oxford University },
year = { 1995 },
number = { TR-21-95 },
month = aug,
abstract = { This thesis is primarily concerned with the
algebraic semantics of non-terminating term
rewriting systems. The usual semantics for rewrite
system is based in interpreting rewrite rules as
equations and rewriting as a particular case of
equational reasoning. The termination of a rewrite
system ensures that every term has a value (normal
form). But, in general we cannot guarantee this. The
research that has been done on non-terminating
rewrite systems is centered on seeking semantics for
these systems where the usual properties of
confluent systems (like uniqueness of normal forms)
still hold. These approaches extend the original set
of terms (with infinite terms) in such a way that
every term has a value. We propose a new semantics
for rewrite systems based on interpreting rewrite
rules as in-equations between terms in an ordered
algebra. We show that a variant of equational logic
--- inequational logic --- is an institution and we
further prove that rewriting is a sound and complete
proof system for this logic. For the case of
confluent systems, we show that the algebra of
normal forms in a terminating system is a uniquely
minimal covering of the term algebra. In the
non-terminating case, the existence of this minimal
covering is established in the completion of an
ordered algebra formed by rewriting sequences. We
thus generalize the properties of normal forms for
non-terminating systems to this minimal
covering. These include the existence of normal
forms for arbitrary rewrite systems, and their
uniqueness for confluent systems, in which case the
algebra of normal forms is isomorphic to the
canonical quotient algebra associated with the rules
when seen as equations. This extends the benefits of
algebraic semantics to systems with
non-deterministic and non-terminating
computations. We first study properties of abstract
orders, and then instantiate these to term rewriting
systems. Furthermore, we review the theory of
rewriting systems without any restriction on the
form of the rules. In this review we include a
comparison between several definitions of concurrent
rewriting. }
}
@TechReport{BarrosGoguen95,
author = { Jos\'e Barros and Joseph A. Goguen },
title = { Semantics Of Non-Terminating Rewrite Systems Using
Minimal Coverings},
institution = { Programming Research Group, Oxford University },
year = 1995,
number = { PRG-118 },
abstract = { We propose a new semantics for rewrite systems
based on interpreting rewrite rules as inequations
between terms in an ordered algebra. In particular,
we show that the algebra of normal forms in a
terminating system is a uniquely minimal covering of
the term algebra. In the non-terminating case, the
existence of this minimal covering is established in
the completion of an ordered algebra formed by
rewriting sequences. We thus generalize the
properties of normal forms for non-terminating
systems to this minimal covering. These include the
existence of normal forms for arbitrary rewrite
systems, and their uniqueness for confluent systems,
in which case the algebra of normal forms is
isomorphic to the canonical quotient algebra
associated with the rules when seen as
equations. This extends the benefits of algebraic
semantics to systems with non-deterministic and
non-terminating computations. We first study
properties of abstract orders, and then instantiate
these to term rewriting systems. }
}
@Article{BattistonBottiCrivelli1995,
author = { Battiston, E. and Botti, O. and Crivelli, E. and
DeCindio, F. },
title = { An Incremental Specification Of A Hydroelectric
Power Plant Control System Using A Class Of Modular
Algebraic Nets },
journal = { Application And Theory Of Petri Nets 1995 },
volume = { 935 },
year = { 1995 },
pages = { 84--102 }
}
@Article{BattistonDecindioMauri1996,
author = { Battiston, E. and DeCindio, F. and Mauri, G. },
title = { Modular Algebraic Nets To Specify Concurrent
Systems },
journal = ieee-tose,
volume = { 22 },
number = { 10 },
year = { 1996 },
pages = { 689--705 }
}
@Article{BergstraHeeringKlint90,
title = { Module Algebra },
author = { Jan Bergstra and Jan Heering and Paul Klint },
journal = { Journal of the Association for Computing Machinery
},
volume = 37,
number = 2,
pages = { 335--372 },
year = 1990
}
@InCollection{BergstraTucker80,
title = { Characterization Of Computable Data Types By Means
Of A Finite Equational Specification Method },
author = { Jan Bergstra and John Tucker },
booktitle = { Automata, Languages and Programming, Seventh
Colloquium },
location = { Noordwijkerhout, the Netherlands },
publisher = { Springer },
year = 1980,
editor = { Jaco de Bakker and Jan van Leeuwen },
pages = { 76--90 },
note = { Lecture Notes in Computer Science, Volume 81 }
}
@Article{BernotBidoitKnapik95,
author = { Gilles Bernot and Michael Bidoit and Teodor Knapik
},
title = { Observational Specifications And The
Indistinguishability Assumption },
journal = { Theoretical Computer Science },
volume = 139,
number = { 1-2 },
pages = { 275--314 },
year = 1995
}
@InCollection{BerregebBouhoulaRusinowitch98,
author = { Narjes Berregeb and Adel Bouhoula and
Micha$\ddot{\rm e}$l Rusinowitch },
title = { Observational Proofs With Critical Contexts },
booktitle = { Fundamental Approaches to Software Engineering },
publisher = { Springer-Verlag },
volume = { 1382 },
series = { Lecture Notes in Computer Science },
year = { 1998 },
pages = { 38-53 }
}
@Article{BidoitHennicker96,
author = { Michael Bidoit and Rolf Hennicker },
title = { Behavioral Theories And The Proof Of Behavioral
Properties },
journal = { Theoretical Computer Science },
volume = 165,
number = 1,
pages = { 3--55 },
year = 1996
}
@Article{BidoitHennicker98,
title = { Modular Correctness Proofs Of Behavioural
Implementations },
author = { Michael Bidoit and Rolf Hennicker },
journal = { Acta Informatica },
volume = 35,
number = 11,
pages = { 951--1005 },
year = { 1998 },
}
@InCollection{BidoitHennicker99,
title = { Observer Complete Definitions Are Behaviourally
Coherent },
author = { Michael Bidoit and Rolf Hennicker },
editor = { Kokichi Futatsugi and Joseph A. Goguen and Jos\'e
Meseguer },
booktitle = { { OBJ }/{ CafeOBJ }/Maude At Formal Methods '99 },
publisher = { Theta },
note = { Proceedings of a workshop held in Toulouse, France,
20th and 22nd September 1999 },
year = 1999,
pages = { 83--94 }
}
@Article{Birkhoff35,
title = { On The Structure Of Abstract Algebras },
author = { Garrett Birkhoff },
year = 1935,
journal = { Proceedings of the Cambridge Philosophical Society
},
volume = 31,
pages = { 433--454 }
}
@Book{Birkhoff67,
key = { Birkhoff },
author = { Garrett Birkhoff },
title = { Lattice Theory },
publisher = { American Mathematical Society },
year = { 1967 },
volume = { 25 },
series = { American Mathematical Societ Colloquium
Publications },
address = { New York, N.Y. },
edition = { Third edition },
annote = { Many references. },
}
@PhdThesis{Borba95,
author = { Paulo Borba },
title = { Semantics And Refinement For A Concurrent Object
Oriented Language },
school = { Oxford University },
year = 1995,
note = { { FOOPS } related. }
}
@InProceedings{BorbaGoguen94,
author = { Paulo Borba and Joseph A. Goguen },
title = { An Operational Semantics For {FOOPS} },
booktitle = { Proceedings, International Workshop on Information
Systems --- Correctness and Reusability,
{IS-CORE'94}},
year = 1994,
editor = { Roel Wieringa and Remco Feenstra },
note = { Published as Technical Report IR-357, Vrije
Universiteit, Amsterdam, September, 1994. A longer
version appears as a Technical Monograph PRG-115,
Oxford University Computing Laboratory, November,
1994 },
read = { 2-10-00 },
reviewed = { 2-10-00 },
review = { A discussion of the full formal semantics of FOOPS
at the object level together with the introduction
of several new constructs (concurrency, background,
private access, etc.). }
}
@TechReport{BorbaGoguen94a,
author = { Paulo Borba and Joseph A. Goguen },
title = { An Operational Semantics for {FOOPS}: Extended
Abstract },
institution = { Programming Research Group, Oxford University },
year = 1994,
number = { PRG-TR-16-94 },
month = nov,
abstract = { FOOPS is a concurrent object-oriented language. We
give a structural operational semantics for FOOPS,
considering features such as classes of objects with
associated methods and attributes, object identity,
dynamic object creation and deletion, overloading,
polymorphism, inheritance with overriding,
concurrency, nondeterminism, atomic execution,
evaluation of expressions as background processes,
and object protection. }
}
@TechReport{BorbaGoguen94b,
author = { Paulo Borba and Joseph A. Goguen },
title = { On Refinement and {FOOPS} },
institution = { Programming Research Group, Oxford University },
year = 1994,
number = { PRG-TR-17-94 },
month = nov,
abstract = { FOOPS is a concurrent object-oriented
language. Based on FOOPS operational semantics, we
define a notion of refinement, and an associated
proof technique. The use of refinement for stepwise
formal development of programs in FOOPS is
illustrated by examples involving memory cells, and
different implementations of buffers. }
}
@TechReport{BorbaGoguen95,
author = { Paulo Borba and Joseph A. Goguen },
title = { Refinement Of Concurrent Object Oriented Programs },
institution = { Programming Research Group, Oxford University },
year = 1995,
number = { PRG-TR-18-95 },
month = nov,
abstract = { FOOPS is a concurrent object oriented
language. Based on FOOPS operational semantics, we
introduce a notion of refinement for states of FOOPS
systems together with a proof technique for proving
refinement. Using this notion, we define refinement
of FOOPS (method) expressions and programs. Although
we focus on FOOPS, our definition of refinement is
independent of this language. We also illustrate the
use of refinement for stepwise formal development of
programs in FOOPS. Based on that, we give an overall
evaluation of our approach and comment on
alternative approaches for the refinement of
concurrent object oriented programs, concluding that
none of them provide both a general definition of
refinement and an effective proof technique such as
the one presented here. },
read = { 2-X-00 },
reviewed = { 2-X-00 },
review = { }
}
@Article{BuchananBritton1992,
author = { Buchanan, M. and Britton, C. },
title = { Formal Specification And Object-Oriented Design },
journal = { Microprocessing And Microprogramming },
volume = { 34 },
number = { 1-5 },
year = { 1992 },
pages = { 19--22 }
}
@TechReport{BurstallDiaconescu92,
author = { Rod Burstall and R\u{a}zvan Diaconescu },
title = { Hiding Sorts in Institutions },
institution = { Programming Research Group, Oxford University },
year = 1992,
month = apr
}
@InCollection{BurstallDiaconescu94,
title = { Hiding And Behaviour: An Institutional Approach },
author = { Rod Burstall and R\u{a}zvan Diaconescu },
booktitle = { A Classical Mind: Essays in Honour of C.A.R.~Hoare
},
editor = { A.~William Roscoe },
publisher = { Prentice-Hall },
pages = { 75--92 },
year = 1994,
note = { Also Technical Report ECS-LFCS-8892-253, Laboratory
for Foundations of Computer Science, University of
Edinburgh, 1992 }
}
@InProceedings{BurstallGoguen82,
author = {Rod Burstall and Joseph Goguen},
title = {Algebras, Theorie and Freeness: An Introduction for
Computer Scientists},
booktitle = {Theoretical Foundations of Programming Methodology},
pages = {329--350},
year = 1982,
editor = {Martin Wirsing and Gunther Schmidt},
volume = {C91},
series = {1981 Marktoberdorf {NATO} Summer School, {NATO}
Advanced Study Institute Series},
publisher = {Reidel}
}
@Article{Cazanescu72,
title = { Familles Initiales Et Finales },
author = { Virgil Emil C\u{a}z\u{a}nescu },
journal = { Revue Roumaine de Mathematiques et Appliques },
year = 1972,
volume = 17,
number = 6
}
@InCollection{Cazanescu93,
title = { Local Equational Logic },
author = { Virgil Emil C\u{a}z\u{a}nescu },
year = 1993,
booktitle = { Proceedings, 9th International Conference on
Fundamentals of Computation Theory FCT'93 },
editor = { Zoltan Esik },
publisher = { Springer-Verlag },
pages = { 162--170 },
note = { Lecture Notes in Computer Science, Volume 710 }
}
@InCollection{Cazanescu94,
title = { Local Equational Logic 2 },
author = { Virgil Emil C\u{a}z\u{a}nescu },
year = 1994,
booktitle = { Developments in Language Theory: At The Crossroads
of Mathematics, Computer Science and Biology },
editor = { G. Rosenberg and A. Saloma },
publisher = { World Scientific },
pages = { 210-221 }
}
@Article{CazanescuRosu97,
title = { Weak Inclusion Systems },
author = { Virgil Emil C\u{a}z\u{a}nescu and Grigore Ro\c{s}u
},
pages = { 195--206 },
journal = { Mathematical Structures in Computer Science },
year = 1997,
volume = 7,
number = 2
}
@Article{CazanescuStef91,
title = { Classes Of Finite Relations As Initial Abstract
Data Types 1 },
author = { Virgil Emil C\u{a}z\u{a}nescu and Gheorghe \c
Stefanescu },
journal = { Discrete Mathematics },
year = 1991,
volume = 90,
pages = { 233-265 }
}
@Article{CazanescuStef94,
title = { Classes Of Finite Relations As Initial Abstract
Data Types 2 },
author = { Virgil Emil C\u{a}z\u{a}nescu and Gheorghe \c
Stefanescu },
journal = { Discrete Mathematics },
year = 1994,
volume = 126,
pages = { 47-65 }
}
@phdthesis{Cerioli93,
title = { Relationships Between Logical Frameworks },
author = { Maura Cerioli },
year = 1993,
school = { Universities of Genova, Pisa and Udine }
}
@Article{CerioliMeseguer97,
title = { May I Borrow Your Logic? (Transporting Logical
Structures Along Maps) },
author = { Maura Cerioli and Jos{\'e} Meseguer },
year = 1997,
journal = { Theoretical Computer Science },
volume = 173,
number = 2,
pages = { 311--347 }
}
@Book{ChangKeisler73,
title = { Model Theory },
author = { C. C. Chang and H. J. Keisler },
year = 1973,
publisher = { North Holland, Amsterdam }
}
@TechReport{Cirstea95,
author = { Corina C{\^\i}rstea },
title = { A Distributed Semantics For {FOOPS}},
institution = { Programming Research Group, Oxford University },
year = 1995,
month = jun,
number = { PRG-TR-20-95 },
abstract = { FOOPS is a concurrent object-oriented specification
language for which an operational semantics has been
provided. This paper gives an equivalent distributed
semantics which describes how FOOPS objects
co-operate in evaluating a program. The distributed
semantics is presented using transition systems. We
relate transition systems and sheaves to also give a
sheaf-theoretic semantics. By implementing the
distributed semantics in Eqlog, we obtain a FOOPS
simulator. Thus, our distributed semantics is both
axiomatic and executable. }
}
@Misc{Cirstea96,
author = { Corina C{\^\i}rstea },
title = { A Semantical Study Of The Object Paradigm },
note = { Thesis submitted for transfer to DPhil status,
Oxford University, 1996 }
}
@InCollection{Cirstea97,
editor = { F. Parisi-Presicce },
author = { Corina C{\^\i}rstea },
title = { Coalgebra Semantics For Hidden Algebra:
Parameterized Objects And Inheritance },
booktitle = { Recent Trends in Algebraic Development Techniques },
publisher = { Springer },
volume = { 1376 },
series = { Lecture Notes in Computer Science },
year = { 1998 }
}
@InProceedings{Cirstea99,
title = { A Coequational Approach To Specifying Behaviours },
author = { Corina C{\^\i}rstea },
booktitle = { Proceedings of the Second Workshop on Coalgebraic
Methods in Computer Science (CMCS'99), Amsterdam,
The Netherlands, March 1999 },
publisher = { Elsevier Science },
volume = 19,
editor = { Bart Jacobs and Jan Rutten },
series = { Electronic Notes in Theoretical Computer Science },
year = 1999
}
@Article{Clark85,
author = { David Clark },
title = { The Structuring Of Systems Using Upcalls },
pages = { 171--180 },
journal = { SIGOPS (Special Interest Group on Operating
Systems) },
volume = { 19 },
number = { 5 },
month = dec,
year = { 1985 }
}
@TechReport{Corradini97,
author = { Andrea Corradini },
title = { A Complete Calculus For Equational Deduction In
Coalgebraic Specification },
year = 1997,
institution = { CWI },
number = { SEN-R9723, ISSN 1386-396X }
}
@Article{Craig57,
title = { Linear Reasoning. A New Form Of The
Herbrand-Gentzen Theorem },
author = { W. Craig },
journal = { Journal of Symbolic Logic },
volume = 22,
year = 1957,
pages = { 250--268 }
}
@Misc{DiaconFutatsugi99,
title = { Logical Foundations Of { CafeOBJ } },
author = { R\u{a}zvan Diaconescu and Kokichi Futatsugi },
year = 1999,
note = { Submitted to Theoretical Computer Science. }
}
@Article{Diaconescu1998,
author = { Diaconescu, R\u{a}zvan },
title = { Extra Theory Morphisms For Institutions: Logical
Semantics For Multi-Paradigm Languages },
journal = { Applied Categorical Structures },
volume = { 6 },
number = { 4 },
year = { 1998 },
pages = { 427--453 }
}
@TechReport{Diaconescu90,
author = { R\u{a}zvan Diaconescu },
title = { The Logic Of {H}orn clauses is equational },
year = 1990,
institution = { Programming Research Group, Oxford University },
number = { PRG-TR-3-93 }
}
@phdthesis{Diaconescu94,
title = { Category-Based Semantics For Equational And
Constraint Logic Programming },
author = { R\u{a}zvan Diaconescu },
year = 1994,
school = { Oxford University },
note = { Original Eqlog work. }
}
@TechReport{Diaconescu96,
title = { Completeness Of Semantic Paramodulation: A
Category-Based Approach },
author = { R\u{a}zvan Diaconescu },
year = 1996,
institution = { Japan Advanced Institute for Science and Technology
},
number = { IS-RR-96-0006S }
}
@Misc{Diaconescu96b,
title = { Behavioral Rewriting Logic: Semantic Foundations
And Proof Theory },
author = { R\u{a}zvan Diaconescu },
year = 1996,
month = { October },
journal = { Journal of Computer and System Sciences },
note = { Submitted for publication. }
}
@Article{Diaconescu96c,
title = { Category-Based Modularization For Equational Logic
Programming },
author = { R\u{a}zvan Diaconescu },
journal = { Acta Informatica },
volume = 33,
number = 5,
pages = { 477--510 },
year = 1996
}
@InProceedings{Diaconescu96d,
title = { A Category-Based Equational Logic Semantics To
Constraint Programming },
author = { R\u{a}zvan Diaconescu },
booktitle = { Recent Trends in Data Type Specification },
editor = { Magne Haveraaen and Olaf Owe and Ole-Johan Dahl },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
volume = 1130,
pages = { 200--221 },
year = 1996,
note = { Proceedings of 11th Workshop on Specification of
Abstract Data Types. Oslo, Norway, September 1995 }
}
@InProceedings{Diaconescu96e,
title = { Foundations Of Behavioral Specification In
Rewriting Logic },
author = { R\u{a}zvan Diaconescu },
booktitle = { Proceedings, First International Workshop on
Rewriting Logic and its Applications },
publisher = { Elsevier Science },
volume = 4,
series = { Electronic Notes in Theoretical Computer Science },
note = { Asilomar, California },
year = 1996
}
@InProceedings{Diaconescu96f,
title = { Logical Semantics For { CafeOBJ } },
author = { R\u{a}zvan Diaconescu and Kokichi Futatsugi },
booktitle = { Precise Semantics for Software Modeling Techniques
},
year = 1998,
publisher = { Proceedings of an ICSE'98 workshop held in Kyoto,
Japan, published as Technical Report TUM-I9803,
Technical University Munchen },
pages = { 31--54 },
note = { Preliminary version appeared as Technical Report
IS-RR-96-0024S at Japan Advanced Institute for
Science and Technology in 1996. }
}
@Misc{Diaconescu96g,
title = { Constraint Logics },
author = { R\u{a}zvan Diaconescu },
year = 1996,
month = { December },
journal = { Mathematical Structures in Computer Science },
note = { Submitted for publication. }
}
@TechReport{Diaconescu98a,
author = { R\u{a}zvan Diaconescu },
title = { Behavioral Coherence In Object-Oriented Algebraic
Specification },
year = 1998,
number = { IS--RR--98--0017F },
month = { June },
institution = { Japan Advanced Institute for Science and Technology
},
note = { Submitted for publication }
}
@TechReport{Diaconescu98b,
author = { R\u{a}zvan Diaconescu and Petros Stefaneas },
title = { Categorical Foundations Of Modularization For
Multi-Paradigm Languages },
institution = { Japan Advanced Institute for Science and Technology
},
year = 1998,
number = { IS-RR-98-0014F }
}
@Book{DiaconescuFutatsugi98,
author = { R\u{a}zvan Diaconescu and Kokichi Futatsugi },
title = { { CafeOBJ } Report: The Language, Proof Techniques,
and Methodologies for Object-Oriented Algebraic
Specification },
year = 1998,
publisher = { World Scientific },
note = { AMAST Series in Computing, volume 6 }
}
@InCollection{DiaconescuGoguenStefaneas93,
author = { R\u{a}zvan Diaconescu and Joseph A. Goguen and
Petros Stefaneas },
title = { Logical Support For Modularization },
booktitle = { Logical Environments },
editor = { Gerard Huet and Gordon Plotkin },
publisher = { Cambridge },
pages = { 83--130 },
year = 1993
}
@Article{DoakeBrittonMitchell1992,
author = { Doake, J. and Britton, C. and Mitchell, R. },
title = { Strange Bedfellows --- Abstract-Data-Types And
Dbase { Iii }},
journal = { Information And Software Technology },
volume = { 34 },
number = { 2 },
year = { 1992 },
pages = { 83--90 }
}
@Book{EhrigMahr85,
Title = { Fundamentals Of Algebraic Specification 1:
Equations And Initial Semantics },
author = { Hartmut Ehrig and Bernd Mahr },
year = 1985,
publisher = { Springer },
note = { EATCS Monographs on Theoretical Computer Science,
Volume 6 }
}
@TechReport{EhrigOrejasEtal93,
author = { Hartmut Ehrig and Fernando Orejas and Felix
Cornelius and Michael Baldamus },
title = { Abstract And Behaviour Module Specifications },
institution = { Technische Universit{\"a}t Berlin },
number = { Technical Report 93-25 },
year = 1993
}
@InCollection{FiadeiroSernadas88,
author = { Jos\'e Fiadeiro and Amilcar Sernadas },
title = { Structuring Theories On Consequence },
booktitle = { Recent Trends in Data Type Specification },
editor = { Donald Sannella and Andrzej Tarlecki },
publisher = { Springer },
note = { Lecture Notes in Computer Science, Volume 332 },
year = 1988,
pages = { 44--72 }
}
@Article{GallimoreColemanStavridou1989,
author = { Gallimore, { R.M. } and Coleman, D. and Stavridou,
V.},
title = { Umist { OBJ } - A Language For Executable Program
Specifications },
journal = { Computer Journal },
volume = { 32 },
number = { 5 },
year = { 1989 },
pages = { 413--421 }
}
@TechReport{GaudelPrivara91,
author = { Marie-Claude Gaudel and Igor Privara },
title = { Context Induction: An Exercise },
institution = { LRI, Universit\'{e} de Paris-Sud },
number = { 687 },
year = 1991
}
@Article{Gnaedig1992,
author = { Gnaedig, I. },
title = { Elios-{ OBJ } --- Theorem-Proving In A Specification
Language },
journal = lncs,
volume = { 582 },
year = { 1992 },
pages = { 182--199 }
}
@Book{Goguen00,
author = { Joseph A. Goguen },
title = { Theorem Proving And Algebra },
publisher = pub-mit,
year = 2000,
note = { In preparation. }
}
@InCollection{Goguen75,
author = { Joseph A. Goguen },
title = { Semantics Of Computation },
year = 1975,
booktitle = { Proceedings, First International Symposium on
Category Theory Applied to Computation and Control },
editor = { Ernest Manes },
publisher = { Springer },
pages = { 151--163 },
note = { (San Fransisco, February 1974.) Lecture Notes in
Computer Science, Volume 25 }
}
@TechReport{Goguen78,
title = { Order Sorted Algebra },
author = { Joseph A. Goguen },
year = 1978,
number = { 14 },
institution = { UCLA Computer Science Department },
note = { Semantics and Theory of Computation Series }
}
@InBook{Goguen89-Algebra,
author = { Joseph A. Goguen },
editor = { Maurice Nivat and Hassan Ait-Kaci },
title = { Resolution of Equations in Algebraic Structures,
Volume 1: Algebraic Techniques },
chapter = { What is Unification: A Categorical View of
Substitution, Equation and Solution },
publisher = pub-ap,
year = 1989,
pages = { 217--261 }
}
@TechReport{Goguen89-Category,
author = { Joseph A. Goguen },
title = { A Categorical Manifesto },
institution = { Programming Research Group, Oxford University },
year = { 1989 },
month = mar,
number = { PRG-72 },
abstract = { This informal paper tries to motivate the use of
category theory in computing science by giving
heuristic guidelines for applying five basic
categorical concepts: category, functor, natural
transformation, adjoint, and colimit. Several
examples and some general discussion are given for
each concept, and a number of references are cited,
although no attempt has been made for
completeness. Some additional categorical concepts
and suggestions for further research are also
mentioned. The paper concludes with a brief
discussion of some implications for foundations. }
}
@InBook{Goguen89-Param,
author = { Joseph Goguen },
editor = { Ted Biggerstaff and Alan Perlis },
title = { Software Reusability, Volume I: Concepts and Models
},
chapter = { Principles of Parameterized Programming },
publisher = pub-aw,
year = 1989,
pages = {159--225}
}
@TechReport{Goguen90-Four,
author = { Joseph A. Goguen },
title = { Four Pieces on Error, Truth and Reality },
institution = { Programming Research Group, Oxford University },
year = 1990,
number = { PRG-89 },
month = oct,
abstract = { This monograph consists of four papers on social
and philosophical aspects of computing. The first,
third and fourth were written for the book Software
Development and Reality Construction, which grew out
of an interdisciplinary conference held in Schloss
Eringerfeld, Germany, in September of 1988. The
second was written as a position paper for the
conference Formal Methods 89 which was held in
Halifax, Nova Scotia in July of 1989. The first
paper is concerned with the role of errors in
computing, and in particular, with the regrettable
tendency within some schools of Formal Methods to
claim that errors can and should play no role at
all. The second paper is largely concerned with
philosophical aspects of Formal Methods, and in
particular with the recent controversies about
whether computing systems can be "proved correct,"
and indeed, with what we mean by "proved" and by
"correct," and how such mathematical concepts
connect with the real world. The third paper goes
somewhat deeper into certain philosophical problems
about meaning and truth. It contrasts the "modern"
formalist position of the logical positivists like
Carnap with the views of Heidegger and
Wittgenstein. This has serious consequences for our
understanding of correctness problems in
computing. The fourth paper takes us somewhat
further afield. It is an attempt to connect the
process of interpretation with the philosophy of
Buddhist meditation. }
}
@InBook{Goguen90-HOP,
author = { Joseph Goguen },
editor = { David Turner },
title = { Research Topics in Functional Programming },
chapter = { Higher-Order Functions Considered Unnecessary for
Higher-Order Programming },
publisher = pub-aw,
year = 1990,
pages = { 309--352 },
read = { 1-00 },
reviewed = { 2-9-00 },
review = { A review of several more examples of HOP with
OBJ3. In particular, attention is paid to
parameterized modules *as* parameters, recursive
definitions over Nat, HOL abstraction of inductive
proofs, and parameterized views. },
note = { Reviewed original version published as report from
PRG at Oxford and available on the web. }
}
@Article{Goguen91a,
author = { Joseph A. Goguen },
title = { Semantic Specifications For The Rewrite Rule
Machine },
journal = lncs,
volume = { 491 },
year = { 1991 },
pages = { 216--234 }
}
@Article{Goguen91b,
author = { Joseph A. Goguen },
title = { A Categorical Manifesto },
journal = { Mathematical Structures in Computer Science },
year = 1991,
volume = 1,
number = 1,
pages = { 49--67 }
}
@InCollection{Goguen91c,
title = { Types as Theories },
author = { Joseph A. Goguen },
booktitle = { Topology and Category Theory in Computer Science },
editor = { George Michael Reed and Andrew William Roscoe and
Ralph F. Wachter },
publisher = { Oxford University },
year = 1991,
pages = { 357--390 },
note = { Proceedings of a Conference held at Oxford, June
1989 }
}
@TechReport{Goguen92,
author = { Joseph A. Goguen },
title = { The Dry and the Wet },
institution = { Programming Research Group, Oxford University },
year = { 1992 },
number = { PRG-100 },
month = mar,
abstract = { This paper discusses the relationship between
formal, context insensitive information, and
informal, situated information, in the context of
Requirements Engineering; these opposite but
complementary aspects of information are called "the
dry" and "the wet". Requirements Engineering has a
strong need to reconcile the dry and the
wet. Following some background on the culture of
Computing Science, the paper describes some projects
in the Centre for Requirements and Foundations at
Oxford. These are: a taxonomy for Requirements
Engineering methods; applying techniques from
sociology and sociolinguistics to requirements
elicitation, and in particular, to determining the
values of an organisation. These projects draw on
ideas from ethnomethodology and Conversation
Analysis. The paper also demonstrates that
structures as dry as abstract data types occur in
the ordinary discourse of social groups. }
}
@InProceedings{Goguen97,
author = { Joseph A. Goguen },
title = { Stretching First Order Equational Logic: Proofs
about Partiality using Subsorts and Retracts },
booktitle = { Proceedings, International Workshop on First Order
Theorem Proving },
year = 1997,
address = { Schloss Hagenbert, Austria },
month = oct
}
@InProceedings{Goguen99,
author = { Joseph A. Goguen },
title = { An Introduction To Algebraic Semiotics, With
Applications To User Interface Design },
booktitle = { Computation for Metaphor, Analogy and Agents },
pages = { 242--291 },
year = 1999,
editor = { Chrystopher Nehaniv },
volume = 1562,
series = { Springer Lecture Notes in Artificial Intelligence },
url = { https://www-cse.ucsd.edu/users/goguen/ps/as.ps.gz },
summary = { This is the basic paper on algebraic semiotics,
with 3/2-categories, 3/2-colimits, and many
examples, especially from user interface design. }
}
@Article{Goguen99a,
author = { Joseph A. Goguen },
title = { Social And Semiotic Analyses For Theorem Prover
User Interface Design },
journal = { The Computer Journal },
year = 1999,
month = jun,
url = { https://www-cse.ucsd.edu/users/goguen/ps/uitp.ps.gz
},
summary = { A systematic justification of the style guidelines
for proof websites generated by Kumo, based on
algebraic semiotics, narratology, cognitive science,
etc. }
}
@InProceedings{Goguen99c,
author = { Joseph A. Goguen },
title = { Hidden Algebra For Software Engineering },
booktitle = { Combinatorics, Computation and Logic, Proceedings,
Conference on Discrete Mathematics and Theoretical
Computer Science },
pages = { 35--59 },
year = 1999,
editor = { Cristian Calude and Michael Dinneen },
volume = 21,
number = 3,
series = { Australian Computer Science Communications },
address = { University of Auckland, New Zealand },
month = jan,
summary = { A gentle introduction to hidden algebra, with
simple examples, much motivation, and some
history. },
url = { https://www-cse.ucsd.edu/users/goguen/ps/dmtcs.ps.gz
}
}
@InCollection{GoguenBurstall84,
title = { Introducing Institutions },
author = { Joseph A. Goguen and Rod Burstall },
booktitle = { Proceedings, Logics of Programming Workshop },
editor = { Edmund Clarke and Dexter Kozen },
year = 1984,
location = { Carnegie-Mellon University },
publisher = { Springer },
note = { Lecture Notes in Computer Science, Volume 164 },
pages = { 221--256 }
}
@Article{GoguenBurstall84a,
title = { Some Fundamental Algebraic Tools For The Semantics
Of Computation, Part 1: Comma Categories, Colimits,
Signatures And Theories },
author = { Joseph A. Goguen and Rod Burstall },
year = 1984,
journal = { Theoretical Computer Science },
volume = 31,
number = 2,
pages = { 175--209 }
}
@Article{GoguenBurstall84b,
title = { Some Fundamental Algebraic Tools For The Semantics
Of Computation, Part 2: Signed And Abstract Theories
},
author = { Joseph A. Goguen and Rod Burstall },
year = 1984,
journal = { Theoretical Computer Science },
volume = 31,
number = 3,
pages = { 263--295 }
}
@TechReport{GoguenBurstall85,
title = { Institutions: Abstract Model Theory For Computer
Science },
author = { Joseph A. Goguen and Rod Burstall },
year = 1985,
institution = { Center for the Study of Language and Information,
Stanford University },
number = { CSLI-85-30 }
}
@InCollection{GoguenBurstall86,
title = { A Study In The Foundations Of Programming
Methodology: Specifications, Institutions, Charters
And Parchments },
author = { Joseph A. Goguen and Rod Burstall },
booktitle = { Proceedings, Conference On Category Theory And
Computer Programming },
editor = { David Pitt and Samson Abramsky and Axel Poign\'e
and David Rydeheard },
location = { University of Surrey, Guildford, U.K. },
publisher = { Springer },
year = 1986,
pages = { 313--333 },
note = { Lecture Notes in Computer Science, Volume 240 }
}
@Article{GoguenBurstall92a,
title = { Institutions: Abstract Model Theory For
Specification And Programming },
author = { Joseph A. Goguen and Rod Burstall },
journal = { Journal of the Association for Computing Machinery
},
volume = 39,
number = 1,
year = 1992,
month = { January },
pages = { 95--146 }
}
@Article{GoguenDiaconescu94,
title = { An {O}xford Survey of Order Sorted Algebra },
author = { Joseph A. Goguen and R\u{a}zvan Diaconescu },
journal = { Mathematical Structures in Computer Science },
volume = 4,
year = 1994,
pages = { 363--392 }
}
@InProceedings{GoguenDiaconescu94,
title = { Towards An Algebraic Semantics For The Object
Paradigm },
author = { Joseph A. Goguen and R\u{a}zvan Diaconescu },
booktitle = { Proceedings, Tenth Workshop on Abstract Data Types
},
editor = { Hartmut Ehrig and Fernando Orejas },
publisher = { Springer },
year = 1994,
pages = { 1--29 },
note = { Lecture Notes in Computer Science, Volume 785 }
}
@TechReport{GoguenEtal89,
author = { Joseph Goguen and Sany Leinwand and Jose Meseguer
and Timothy Winkler },
title = { The Rewrite Rule Machine, 1988 },
institution = { Programming Research Group, Oxford University },
year = 1989,
number = { PRG-76 },
month = aug,
abstract = { This monograph consists of two papers which jointly
summarize research in the Rewrite Rule Machine (RRM)
Project as of about the end of 1988. Research in
this period focussed on two topics: the design of
very high level multi-paradigm programming
languages; and an architecture for executing such
languages using graph rewriting. The first paper,
"Software for the Rewrite Rule Machine," gives an
overview of RRM implementation techniques for
functional, relational ("logic"), and object
oriented languages, as well as for their
combinations. This paper is nearly the same as one
that appeared on pages 628-637 of the Proceedings of
the International Conference on Fifth Generation
Computer Systems, held in Toyko in November
1988. The languages are unusual because their
designs are based directly on logic, and nothing has
been allowed to compromise their basis in logic. The
second paper, "Cell, Tile and Ensemble Architecture
of the Rewrite Rule Machine," describes the quite
unconventional hierarchical architecture of a custom
VLSI chip, called a rewrite ensemble, which
processes data directly in memory, in SIMD mode. A
complete RRM consists of many independent rewrite
ensembles connected over a network. This paper is a
very substantial modification of one appearing on
pages 869-878 of the same Proceedings. }
}
@Article{GoguenKirchnerKirchner1988,
author = { Joseph A. Goguen and Kirchner, C. and Kirchner,
H. and Megrelis, A. and Meseguer, J. and Winkler,
T. },
title = { An Introduction To { OBJ }-3},
journal = lncs,
volume = { 308 },
year = { 1988 },
pages = { 258--263 }
}
@InProceedings{GoguenLinEtal97,
author = { Joseph A. Goguen and Kai Lin and Akira Mori and
Grigore Ro\c{s}u and Akiyoshi Sato },
title = { Distributed Cooperative Formal Methods Tools },
booktitle = { Proceedings, Automated Software Engineering },
pages = { 55--62},
year = 1997,
address = { Lake Tahoe, NV },
month = nov,
publisher = { IEEE },
url = { https://www-cse.ucsd.edu/users/goguen/ps/ase97.ps.gz
},
summary = { Overview of the Tatami project tools and methods,
including hidden algebra and algebraic semiotics,
with examples. }
}
@InProceedings{GoguenLinEtal98,
author = { Joseph A. Goguen and Kai Lin and Akira Mori and
Grigore Ro\c{s}u },
title = { Tools for Distributed Cooperative Engineering },
booktitle = { Proceedings, { CafeOBJ } Symposium },
pages = { 26--29 },
year = 1998,
address = { Kyoto, Japan },
month = apr,
url = {
https://www-cse.ucsd.edu/users/goguen/ps/icse98.ps.gz
},
summary = { Describes how the Tatami system and Kumo website
editor/proof assistant integrate formal and informal
methods of software development, in a distributed
cooperative environment. ProofWebs can contain scans
of envelope backs, diagrams, applets, as well as
fully formal subproofs. }
}
@InCollection{GoguenLinEtal98,
title = { Tools For Distributed Cooperative Design And
Validation },
author = { Joseph A. Goguen and Kai Lin and Akira Mori and
Grigore Ro\c{s}u and Akiyoshi Sato },
booktitle = { Proceedings, { CafeOBJ } Symposium },
publisher = { Japan Advanced Institute for Science and Technology
},
year = 1998,
note = { Numazu, Japan, April 1998 }
}
@Book{GoguenMalcolm00,
editor = { Joseph A. Goguen and Grant Malcolm },
title = { Software Engineering With { OBJ }: Algebraic
Specification in Action },
publisher = pub-klu,
year = 2000
}
@InBook{GoguenMalcolm00-HOP,
author = { Joseph A. Goguen and Grant Malcolm },
editor = { Joseph A. Goguen and Grant Malcolm },
title = { Software Engineering With { OBJ }: Algebraic
Specification in Action },
chapter = { More Higher Order Programming with { OBJ } },
publisher = pub-klu,
year = 2000
}
@InCollection{GoguenMalcolm94,
title = { Proof Of Correctness Of Object Representation },
author = { Joseph A. Goguen and Grant Malcolm },
booktitle = { A Classical Mind: Essays in Honour of C.A.R.~Hoare
},
editor = { A. William Roscoe },
publisher = { Prentice-Hall },
pages = { 119--142 },
year = 1994
}
@Book{GoguenMalcolm96-ASoIP,
author = { Joseph A. Goguen and Grant Malcolm },
title = { Algebraic Semantics Of Imperative Programs },
publisher = pub-mit,
year = 1996,
series = { Foundations of Computing Series },
callno = { QA76.7.G62 1996 }
}
@InCollection{GoguenMalcolm96-HA,
title = { Extended Abstract Of A Hidden Agenda },
author = { Joseph A. Goguen and Grant Malcolm },
booktitle = { Proceedings, Conference on Intelligent Systems: A
Semiotic Perspective },
editor = { James Albus and Alex Meystel and Richard Quintero },
publisher = { National Inst.\ Standards and Technology },
year = 1996,
note = { Gaithersberg MD, October 20--23 },
pages = { 159--167 }
}
@Article{GoguenMalcolm97,
author = { Joseph A. Goguen and Grant Malcolm },
title = { A Hidden Agenda },
journal = { Theoretical Computer Science },
note = { Also UCSD Dept.\ Computer Science \& Eng.\
Technical Report CS97--538, May 1997 },
year = { to appear 1999 }
}
@InBook{GoguenMalcolm99c,
author = { Joseph A. Goguen and Grant Malcolm },
editor = { Chrystopher Nehaniv and Masami Ito },
title = { Theoretical Computer Science, Special Issue On
Algebraic Engineering },
chapter = { A Hidden Agenda },
publisher = pub-esp,
year = 1999,
summary = { This is the basic paper on hidden algebra, treating
coinduction, nondeterminism, concurrency and more. },
url = { https://www-cse.ucsd.edu/users/goguen/ps/ha.ps.gz }
}
@Article{GoguenMalcolm99a,
author = { Joseph A. Goguen and Grant Malcolm },
title = { Hidden Coinduction },
journal = { Mathematical Structures in Computer Science },
year = { to appear 1999 }
}
@InBook{GoguenMalcolm99b,
author = { Joseph A. Goguen and Grant Malcolm },
editor = { G. Longo },
title = { Mathematical Structures In Computer Science },
chapter = { Hidden Coinduction },
publisher = pub-cup,
year = 1999,
url = { https://www-cse.ucsd.edu/users/goguen/ps/coind.ps.gz
},
summary = { This is a sister paper to GoguenMalcolm99a. }
}
@Article{GoguenMalcolmKemp98,
author = { Joseph A. Goguen and Grant Malcolm and Tom Kemp },
title = { A Hidden Herbrand Theorem: Combining The Object,
Logic And Functional Paradigms },
journal = { Electronic Journal of Functional and Logic
Programming },
year = 1998,
note = { Original version of paper published in PLIP/ALP'98
as Principles of Declarative Programming },
url = { https://www-cse.ucsd.edu/users/goguen/ps/hherb.ps.gz
},
summary = { Shows how to combine the logic and object paradigms
using hidden algebra with existential quantifiers. }
}
@InBook{GoguenMalcolm96,
author = { Joseph A. Goguen and Grant Malcolm },
editor = { Michael Hinchey and C. Nevill Dean },
title = { Teaching And Learning Formal Methods },
chapter = { An Executable Course in Algebraic Semantics of
Imperative Programs },
publisher = pub-ap,
year = 1996,
pages = { 161--179 },
read = { 1-00 },
reviewed = { 2-9-00 },
review = { A summary of the teaching methodology at Oxford wrt
using OBJ. The examples are mainly taken from the
many other sets of examples of the same. Special
care is taken in section 4 to mention that OBJ is
only a notation, not a method or process. Also
metioned is the fact that teamwork and management
and social issues can dominate complex program
development. }
}
@Article{GoguenMeseguer85,
title = { Completeness Of Many-Sorted Equational Logic },
author = { Joseph A. Goguen and Jos\'e Meseguer },
year = 1985,
journal = { Houston Journal of Mathematics },
volume = 11,
number = 3,
pages = { 307--334 },
note = { Preliminary versions have appeared in: {\it SIGPLAN
Notices}, July 1981, Volume 16, Number 7, pages
24--37; SRI Computer Science Lab, Report CSL-135,
May 1982; and Report CSLI-84-15, Center for the
Study of Language and Information, Stanford
University, September 1984 }
}
@InBook{GoguenMeseguer86,
author = { Joseph Goguen and Jos\'e Meseguer },
editor = { Douglas DeGroot and Gard Lindstrom },
title = { Logic Programming: Functions, Relations and
Equations },
chapter = { Eqlog: Equality, Types, and Generic Modules for
Logic Programming },
publisher = pub-ph,
year = 1986,
pages = { 295--363 },
note = { Earlier version appears in Journal of Logic
Programming, Volume 1, Number 2, pages 179--210,
September 1984 }
}
@InProceedings{GoguenMeseguer87-Eqlog,
author = { Joseph Goguen and Jos\'e Meseguer },
title = { Models and Equality for Logical Programming },
booktitle = { Proceedings, 1987 TAPSOFT },
pages = { 1--22 },
year = 1987,
editor = { Hartmut Ehrig and Giorgio Levi and Robert Kowalski
and Ugo Mont },
volume = 250,
series = lncs,
publisher = pub-sv
}
@InBook{GoguenMeseguer87-Foops,
author = { Joseph Goguen and Jos\'e Meseguer },
editor = { Bruce Shriver and Peter Wegner },
title = { Research Directions in Object-Oriented Programming
},
chapter = { Unifying Functional, Object-Oriented and Relational
Programming with Logical Semantics },
publisher = pub-mit,
year = 1987,
pages = { 417--477 },
note = { Preliminary version in SIGPLAN Notices, Volume 21,
Number 10, pages 153--162, October 1986 }
}
@TechReport{GoguenMeseguer89,
author = { Joseph Goguen and Jose Meseguer },
title = { Order-Sorted Algebra I : Equational Deduction For
Multiple Inheritance, Overloading, Exceptions And
Partial Operations },
institution = { Programming Research Group, Oxford University },
year = 1989,
number = { PRG-80 },
month = dec,
abstract = { This paper generalizes many-sorted algebra
(hereafter, MSA) to order-sorted algebra (hereafter,
OSA) by alowing a partial ordering relation on the
set of sorts. This supports abstract data types with
multiple inheritance (in roughly the sense of
object-oriented programming), several forms of
polymorphism and overloading, partial operations (as
total on equationally defined subsorts), exception
handling, and an operational semantics based on term
rewriting. We give the basic algebraic constructions
for OSA, including Quotient, Homomorphism, and
Initiality Theorems. The paper's major mathematical
results include a notion of OSA deduction, a
Completeness Theorem for it, and an OSA Birkhoff
Variety Theorem. We also develop conditional OSA,
including Initiality, Completeness, and
McKinsey-Malcev Quasivariety Theorems, and we reduce
OSA to (conditional) MSA, which allows lifting many
known MSA results to OSA. Retracts, which
intuitively are left inverses to subsort inclusions,
provide relatively inexpensive run-time error
handling. We show that it is safe to add retracts to
any OSA signature, in the sense that it gives rise
to a conservative extension. A final section
compares and contrasts many different approaches to
OSA. This paper also includes several examples
demonstrating the flexibility and applicability of
OSA, including some standard benchmarks like STACK
and LIST, as well as a much more substantial
example, the number hierarchy from the naturals up
to the quaternions. }
}
@TechReport{GoguenMeseguer89,
author = {J. Goguen and J. Meseguer},
title = {Order-Sorter Algebra {I}},
institution = {SRI CSL},
year = 1989,
number = {SRI-CSL-89-10},
note = {This is the primary paper on the theoretical
framework for the semantics of OBJ3.}
}
@InProceedings{GoguenMoriLin97,
author = { Joseph A. Goguen and Akira Mori and Kai Lin },
title = { Algebraic Semiotics, Proofwebs, And Distributed
Cooperative Proving },
booktitle = { Proceedings of the 1997 Conference on User
Interfaces for Theorem Provers },
pages = { 24--34 },
year = 1997,
month = sep,
url = { https://www-cse.ucsd.edu/users/goguen/ps/tat97.ps.gz
},
summary = { Describes the Tatami ProofWeb data structure and
the Kumo proof assistant and website generator, plus
how semiotics was used in their design. }
}
@InProceedings{GoguenRosu99,
author = { Joseph A. Goguen and Grigore Ro\c{s}u },
title = { Hiding More of Hidden Algebra },
booktitle = { FM'99 --- Formal Methods, Proceedings of World
Congress on Formal Methods },
pages = { 1704--1709 },
year = 1999,
volume = 1709,
series = lncs,
address = { Toulouse, France },
month = aug,
publisher = pub-sv,
url = { https://www-cse.ucsd.edu/users/goguen/ps/moreh.ps.gz
},
summary = { New results relating information hiding to hidden
algebra, compelling examples of behavioral
operations with multiple hidden arguments, and an
improved institution for hidden algebra. }
}
@InProceedings{GoguenRosu99b,
title = { A Protocol For Distributed Cooperative Work },
author = { Joseph A. Goguen and Grigore Ro\c{s}u },
booktitle = { Proceedings of Workshop on Distributed Systems 1999
(WDS'99), Iasi, Romania, 2 September 1999 },
publisher = { Elsevier Science },
volume = 28,
editor = { Gheorghe \c{S}tef\u{a}nescu },
series = { Springer Electronic Notes in Theoretical Computer
Science },
year = 1999,
address = { Iasi, Romania },
month = sep,
url = { https://www-cse.ucsd.edu/users/goguen/ps/iasi.ps.gz
},
summary = { Uses hidden algebra to prove correctness of a novel
internet broadcast protocol designed to support
synchronous distributed cooperative proving; also
contains the most recent brief summary of the main
definitions and results of hidden algebra. }
}
@TechReport{GoguenSocorro95,
author = { Joseph A. Goguen and Adolfo Socorro },
title = { Module Composition And System Design For The Object
Paradigm },
institution = { Programming Research Group, Oxford University },
year = { 1995 },
number = { PRG-117 },
month = jan,
abstract = { This paper argues that a powerful module
composition facility can enhance the ability of
object oriented languages to reuse and compose
designs, specifications and code. In addition,
several flexible ways to produce prototypes can be
supported, including symbolic execution of designs,
composing prototype versions of components, and
using "built-in" modules. Much of this power comes
from having module expressions, theories and views
as first class citizens; some comes from providing
both vertical and horizontal composition, and from
distinguishing between sorts for values, classes for
objects, modules for code, and theories as types for
modules. New features introduced in this paper
include dynamic binding with views, vertical
wrappers, support for abstract classes and private
class inheritance, and the dynamic integration of
components from different libraries. Although we
illustrate these features using the FOOPS language,
they could be added to many other languages, and
some comparison with other languages is given. }
}
@Article{GoguenStevensEtal92,
author = { Joseph Goguen and Andrew Stevens and Keith Hobley
and Hendrik Hilberdink },
title = { {2OBJ}, a Metalogical Framework Based on Equational
Logic },
journal = { Philosophical Transactions of the Royal Society,
Series A },
year = 1992,
volume = 339,
pages = { 69--86 }
}
@InCollection{GoguenTardo79,
title = { An Introduction To { OBJ }: A Language for Writing
and Testing Software Specifications },
author = { Joseph A. Goguen and Joseph Tardo },
year = 1979,
booktitle = { Specification Of Reliable Software },
editor = { Marvin Zelkowitz },
publisher = { IEEE },
location = { Cambridge MA },
pages = { 170--189 },
note = { Reprinted in {\it Software Specification
Techniques\/}, Nehan Gehani and Andrew McGettrick,
editors, Addison Wesley, 1985, pages 391--420 }
}
@Misc{GoguenTatami,
author = { Joseph A. Goguen },
title = { The Tatami System Design And Its Motivation },
howpublished = { www },
url = { https://www-cse.ucsd.edu/users/goguen/ps/tata.ps.gz
}
}
@InBook{GoguenThatcherEtal75,
author = {Joseph Goguen and James Thatcher and Eric Wagner and
Jesse Wright},
title = {Computer Graphics, Pattern Recognition and Data
Structure},
chapter = {Abstract Data Types as Initial Algebras and the
Correctness of Data Representation},
publisher = pub-ieee,
year = 1975,
pages = {89--93}
}
@InCollection{GoguenThatcherWagner76,
title = { An Initial Algebra Approach To The Specification,
Correctness And Implementation Of Abstract Data
Types },
author = { Joseph A. Goguen and James Thatcher and Eric Wagner
},
booktitle = { Current Trends In Programming Methodology, Iv },
year = 1978,
publisher = { Prentice-Hall },
editor = { Raymond Yeh },
pages = { 80--149 }
}
@Misc{GoguenTracz97,
author = { Joseph A. Goguen and Will Tracz },
title = { An Implementation-Oriented Semantics For Module
Composition },
year = 1997
}
@InCollection{GoguenWinklerEtal00,
author = { Joseph A. Goguen and Timothy Winkler and Jos\'e
Meseguer and Kokichi Futatsugi and Jean-Pierre
Jouannaud },
title = { Introducing { OBJ } },
booktitle = { Software Engineering with { OBJ }: Algebraic
Specification in Action },
editor = { Joseph A. Goguen and Grant Malcolm },
year = { 2000 },
publisher = pub-klu,
note = { Also Technical Report SRI-CSL-88-9, August 1988,
SRI International }
}
@InBook{GoguenWolfram91,
author = { Joseph Goguen and David Wolfram },
editor = { Robert Meersman and William Kent and Samit Khosla },
title = { Object Oriented Databases: Analysis, Design and
Construction },
chapter = { On Types and {FOOPS} },
publisher = { North Holland },
year = 1991,
note = { Also in Proceedings, IFIP TC2 Conference,
Windermere, UK, 2--6 July 1990 }
}
@Book{Gratzer71,
author = { George Gr{\"a}tzer },
title = { Lattice Theory },
publisher = { W.H. Freeman and Company },
year = { 1971 },
address = { San Francisco },
}
@Article{Grothendieck57,
title = { Sur Quelques Points D'alg\'ebre Homologique },
author = { Alexandre Grothendieck },
journal = { T\^ohoku Mathematical Journal },
volume = 2,
pages = { 119--221 },
year = 1957
}
@InProceedings{Gumm98,
title = { Equational And Implicational Classes Of
Coalgebras. Extended Abstract. },
author = { H. Peter Gumm },
booktitle = { The 4th International Seminar on Relational Methods
in Logic, Algebra and Computer Science },
note = { Warsaw },
year = 1998
}
@InProceedings{GummSchroder98,
title = { Covarieties And Complete Covarieties },
author = { H. Peter Gumm and Tobias Schr\"oder },
booktitle = { Proceedings of the First Workshop on Coalgebraic
Methods in Computer Science (CMCS'98), Lisbon,
Portugal, March 1998 },
publisher = { Elsevier Science },
pages = { 43-56 },
volume = 11,
editor = { Bart Jacobs and Larry Moss and Horst Reichel and
Jan Rutten },
series = { Electronic Notes in Theoretical Computer Science },
year = 1998
}
@TechReport{Hamel94,
author = { Lutz H. Hamel },
title = { Towards a Provable Correct Compiler for { OBJ3 }},
institution = { Programming Research Group, Oxford University },
year = 1994,
number = { TR-1-94 }
}
@PhDThesis{Hamel96,
title = { Behavioural Verification And Implementation Of An
Optimizing Compiler For { OBJ3 } },
author = { Lutz Hamel },
school = { Oxford University Computing Lab },
year = 1996
}
@TechReport{Hamel01,
title = { Introducing { TRIM } },
author = { Lutz Hamel },
school = { Department of Computer Science and Statistics,
University of Rhode Island },
year = 2001
}
@Article{Hennicker91,
title = { Context Induction: A Proof Principle For Behavioral
Abstractions },
author = { Rolf Hennicker },
journal = { Formal Aspects of Computing },
volume = 3,
number = 4,
pages = { 326--345 },
year = 1991
}
@InProceedings{HennickerBidoit99,
title = { Observational Logic },
author = { Rolf Hennicker and Michel Bidoit },
booktitle = { Algebraic Methodology and Software Technology
(AMAST'98) },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
volume = 1548,
pages = { 263--277 },
year = 1999
}
@InProceedings{HennickerKurz99,
title = { On The Algebraic Extension Of Coalgebraic
Specifications },
author = { Rolf Hennicker and Alexander Kurz },
booktitle = { Proceedings of the Second Workshop on Coalgebraic
Methods in Computer Science (CMCS'99), Amsterdam,
The Netherlands, March 1999 },
publisher = { Elsevier Science },
volume = 19,
editor = { Bart Jacobs and Jan Rutten },
series = { Electronic Notes in Theoretical Computer Science },
year = 1999
}
@Book{HerrlichStrecker73,
title = { Category Theory },
author = { Horst Herrlich and George Strecker },
year = 1973,
publisher = { Allyn and Bacon }
}
@Misc{Hilberdink96,
title = { Inclusion Systems },
author = { Hendrik Hilberdink },
school = { Oxford University },
note = { Unpublished paper },
year = 1996
}
@Book{HindleySeldin86,
author = { J. Roger Hindley and Jonathan P. Seldin },
title = { Introduction To Combinatory Logic And Lambda
Calculus },
publisher = { Cambridge University Press },
year = { 1986 },
}
@TechReport{IidaMatsumotoEtal97,
author = { Shusaku Iida and Michihiro Matsumoto and R\u{a}zvan
Diaconescu and Kokichi Futatsugi and Dorel Lucanu },
title = { Concurrent Object Composition In { CafeOBJ } },
year = 1997,
institution = { Japan Advanced Institute for Science and Technology
},
number = { IS-RR-96-0024S }
}
@Article{Isbell64,
title = { Subobjects, Adequacy, Completeness And Categories
of Algebras },
author = { J. R. Isbell },
journal = { Rozprawy Matematyczne },
volume = 36,
pages = { 1--33 },
year = 1964
}
@InCollection{Jacobs95,
author = { Bart Jacobs },
title = { Mongruences And Cofree Coalgebras },
booktitle = { Algebraic Methodology and Software Technology
(AMAST95) },
editor = { Maurice Nivat },
publisher = { Springer },
note = { Lecture Notes in Computer Science, Volume 936 },
pages = { 245--260 },
year = 1995
}
@Article{JacobsRutten97,
title = { A Tutorial On (Co)Algebras And (Co)Induction },
author = { Bart Jacobs and Jan Rutten },
journal = { Bulletin of the European Association for
Theoretical Computer Science },
volume = 62,
year = 1997,
pages = { 222--259 }
}
@Article{JouannaudKirchnerKirchner1988,
author = { Jouannaud, { J.P. } and Kirchner, C. and Kirchner,
H. and Megrelis, A. },
title = { { OBJ } - Programming With Equalities, Subsorts,
Overloading And Parameterization },
journal = lncs,
volume = { 343 },
year = { 1988 },
pages = { 41--52 }
}
@Article{JouannaudKirchnerKirchner1992,
author = { Jouannaud, { J.P. } and Kirchner, C. and Kirchner,
H. and Megrelis, A. },
title = { Programming With Equalities, Subsorts, Overloading,
And Parametrization In { OBJ }},
journal = jolp,
volume = { 12 },
number = { 3 },
year = { 1992 },
pages = { 257--279 }
}
@TechReport{KieburtzLewis94,
author = { Richard B. Kieburtz and Jeffrey Lewis },
title = { Algebraic Design Language (Preliminary Definition)
},
institution = { Oregon Graduate Insitute of Science and Technology
},
year = 1994,
month = jan,
url = { https://www.cse.ogi.edu/~sheard/adl.html }
}
@Article{KirchnerKirchnerMeseguer1988,
author = { Kirchner, C. and Kirchner, H. and Meseguer, J. },
title = { Operational Semantics Of { OBJ }-3},
journal = lncs,
volume = { 317 },
year = { 1988 },
pages = { 287--301 }
}
@Book{Lambek66,
author = { Joachim Lambek },
title = { Completions Of Categories },
year = 1966,
publisher = { Springer-Verlag },
note = { Lecture Notes in Mathematics, Volume 24 }
}
@Book{LambekScott86,
title = { Introduction To Higher Order Categorical Logic },
author = { Joachim Lambek and Phil Scott },
publisher = { Cambridge },
year = 1986,
note = { Cambridge Studies in Advanced Mathematics, Volume 7
}
}
@InCollection{Lucanu99a,
title = { Algebraic Specification Of Object Aggregation },
author = { Dorel Lucanu },
editor = { Kokichi Futatsugi and Joseph A. Goguen and Jos\'e
Meseguer },
booktitle = { { OBJ }/{ CafeOBJ }/Maude At Formal Methods '99 },
publisher = { Theta },
note = { Proceedings of a workshop held in Toulouse, France,
20th and 22nd September 1999 },
year = 1999,
pages = { 115--132 }
}
@InProceedings{LucanuGheorghiesApetrei99,
title = { Bisimulation And Hidden Algebra },
author = { Dorel Lucanu and Ovidiu Gheorghie\c{s} and Adriana
Apetrei },
booktitle = { Proceedings of the Second Workshop on Coalgebraic
Methods in Computer Science (CMCS'99), Amsterdam,
The Netherlands, March 1999 },
pages = { 213--232 },
editor = { Bart Jacobs and Jan Rutten },
publisher = { Elsevier Science },
volume = 19,
series = { Electronic Notes in Theoretical Computer Science },
year = 1999
}
@Book{MacLane71,
title = { Categories For The Working Mathematician },
author = { Saunders Mac~Lane },
year = 1971,
publisher = { Springer }
}
@TechReport{MalcolmGoguen94,
author = { Grant Malcolm and Joseph A. Goguen },
title = { Proving Correctness Of Refinement And
Implementation },
institution = { Programming Research Group, Oxford University },
year = { 1994 },
number = { PRG-114 },
month = nov,
abstract = { The notions of state and observable behaviour are
fundamental to many areas of computer
science. Hidden sorted algebra, an extension of many
sorted algebra, captures these notions through
hidden sorts and the behavioural satisfaction of
equations. This makes it a powerful formalisation of
abstract machines, and many results suggest that it
is also suitable for the semantics of the object
paradigm. Another extension of many sorted algebra,
namely order sorted algebra, has proved useful in
system specification and prototyping because of the
way it handles subtypes and errors. The combination
of these two algebraic approaches, hidden order
sorted algebra, has also been proposed as a
foundation for object paradigm, and has much promise
as a foundation for Software Engineering. This paper
extends recent work on hidden order sorted algebra
by investigating the refinement and implementation
of hidden order sorted specifications. We present
definitions of refinement and implementation for
such specifications, and techniques for proving that
one specification refines or implements another. It
is important that the notions of refinement and
implementation be tractable, in the sense that there
are efficient techniques for proving their
correctness. The proof techniques given in this
paper lead, we believe, to correctness proofs that
are much simpler than others in the literature. We
found that proving refinement is an effective way to
prove implementation correctness. Some examples are
given. Any foundation for the semantics of
programming should also support modular
specifications. The "institutions" developed by
Goguen and Burstall are useful for this
purpose. Institutions formalise the notion of
logical system, and provide an encapsulation
property for specifications: when one specification
is imported into another, properties that hold of
that specification in isolation remain true in its
new context. An important technical result of this
paper is that hidden order sorted algebra forms an
institution, and therefore supports the modular
specification of systems of objects. The paper also
includes an exposition of hidden order sorted
algebra, and brief introductions to many sorted
algebra, order sorted algebra, and institutions. }
}
@InProceedings{MalcolmGoguen98,
author = { Grant Malcolm and Joseph A. Goguen },
title = { Signs And Representations: Semiotics For User
Interface Design },
booktitle = { Visual Representations and Interpretations },
pages = { 163--172 },
year = 1998,
editor = { Ray Paton and Irene Nielson },
series = { Springer Workshops in Computing },
note = { Proceedings of a workshop held in Liverpool. },
summary = { An informal introduction to algebraic semiotics
with examples, including aspects of operating
systems interfaces. },
url = {
https://www-cse.ucsd.edu/users/goguen/ps/sigreps.ps.gz }
}
@InCollection{MatsumiyaIidaFutatsugi99,
title = { A Component-Based Algebraic Specification Of Odp
Trading Function },
author = { Chiyo Matsumiya and Shusaku Iida and Kokichi
Futatsugi },
editor = { Kokichi Futatsugi and Joseph A. Goguen and Jos\'e
Meseguer },
booktitle = { { OBJ }/{ CafeOBJ }/Maude At Formal Methods '99 },
publisher = { Theta },
note = { Proceedings of a workshop held in Toulouse, France,
20th and 22nd September 1999 },
year = 1999,
pages = { 227--241 }
}
@InProceedings{MatsumotoFutatsugi98,
author = { Michihiro Matsumoto and Kokichi Futatsugi },
title = { Test Set Coinduction -- Toward Automated
Verification Of Behavioral Properties },
booktitle = { Proceedings of the Second International Workshop on
Rewriting Logic and Its Applications (WRLA'98) },
series = { Electronic Notes in Theoretical Computer Science },
volume = 15,
publisher = { Elsevier Science },
year = { 1998 }
}
@InCollection{MatsumotoFutatsugi99,
title = { Object Composition And Refinement By Using
Non-Observable Projection Operators },
author = { Michihiro Matsumoto and Kokichi Futatsigi },
editor = { Kokichi Futatsugi and Joseph A. Goguen and Jos\'e
Meseguer },
booktitle = { { OBJ }/{ CafeOBJ }/Maude At Formal Methods '99 },
publisher = { Theta },
note = { Proceedings of a workshop held in Toulouse, France,
20th and 22nd September 1999 },
year = 1999,
pages = { 133--157 }
}
@InCollection{Meseguer89,
author = { Jos\'e Meseguer },
title = { General Logics },
booktitle = { Proceedings, Logic Colloquium 1987 },
publisher = { North-Holland },
editor = { H.-D. Ebbinghaus and others },
pages = { 275--329 },
year = 1989
}
@InCollection{MeseguerGoguen85,
title = { Initiality, Induction And Computability },
author = { Jos\'e Meseguer and Joseph A. Goguen },
booktitle = { Algebraic Methods in Semantics },
editor = { Maurice Nivat and John Reynolds },
publisher = { Cambridge },
year = 1985,
pages = { 459--541 }
}
@InCollection{Mikami98,
title = { Semantics Of Equational Specifications With Module
Import And Verification Method Of Behavioral
Equations },
author = { Seik\^{o} Mikami },
booktitle = { Proceedings, { CafeOBJ } Symposium },
publisher = { Japan Advanced Institute for Science and Technology
},
year = 1998,
note = { Numazu, Japan, April 1998 }
}
@Book{Mitchell65,
title = { Theory Of Categories },
author = { Mitchell, B. },
year = 1965,
publisher = { Academic Press, New York }
}
@InCollection{MoriFutatsugi99,
title = { Verifying Behavioural Specifications In { CafeOBJ }
Environment },
author = { Akira Mori and Kokichi Futatsugi },
booktitle = { FM'99 -- Formal Methods },
note = { Lecture Notes in Computer Sciences, Volume 1709,
Proceedings of World Congress on Formal Methods,
Toulouse, France },
publisher = { Springer },
pages = { ????--???? },
year = 1999
}
@phdthesis{Mossakowski96,
title = { Representations, Hierarchies, And Graphs Of
Institutions },
author = { Till Mossakowski },
year = 1996,
school = { University of Bremen }
}
@Misc{Mossakowski98,
title = { Version Control And Registration For Casl Libraries
},
author = { Till Mossakowski },
note = { CoFi Note: M-5, 29 September 1998. {\tt
https://www.brics.dk/Projects/CoFI/Notes/M-5} }
}
@InCollection{Mosses89,
author = { Peter Mosses },
title = { Unified Algebras And Institutions },
year = 1989,
booktitle = { Proceedings, Fourth Annual Conference on Logic in
Computer Science },
pages = { 304--312 },
publisher = { IEEE }
}
@InProceedings{NakajimaFutatsugi97,
author = { Shin Nakajima and Kokichi Futatsugi },
title = { An Object-Oriented Modeling Method For Algebraic
Specifications In { CafeOBJ }},
booktitle = { Proceedings of the 1997 International Conference on
Software Engineering },
pages = { 34--44 },
year = 1997,
address = { Boston, MA }
}
@Article{Nemeti82,
title = { On Notions Of Factorization Systems And Their
Applications To Cone-Injective Subcategories },
author = { Istv{\'a}n N{\'e}meti },
journal = { Periodica Mathematica Hungarica },
year = 1982,
volume = 13,
number = 3,
pages = { 229--335 }
}
@InCollection{NemetiSain81,
title = { Cone-Implicational Subcategories And Some
Birkhoff-Type Theorems },
author = { Istv{\'a}n N{\'e}meti and Ildick{\'o} Sain },
booktitle = { Universal Algebra },
editor = { B. Csakany and E. Fried and E.T. Schmidt },
year = 1981,
publisher = { North-Holland },
pages = { 535--578 },
note = { Colloquia Mathematics Societas J{\'a}nos Bolyai, 29
}
}
@Misc{NielsenPlatet86,
title = { Polymorphism In An Institutional Framework },
author = { Mogens Nielsen and Udo Platet },
year = 1986,
note = { Technical University of Denmark }
}
@InProceedings{Padawitz96,
author = { Peter Padawitz },
title = { Swinging Data Types: Syntax, Semantics, And Theory
},
booktitle = { Proceedings, WADT'95 },
series = { Lecture Notes in Computer Science },
volume = 1130,
publisher = { Springer },
pages = { 409--435 },
year = 1996
}
@InProceedings{Padawitz98,
author = { Peter Padawitz },
title = { Towards The One-Tiered Design Of Data Types And
Transition Systems },
booktitle = { Proceedings, WADT'97 },
series = { Lecture Notes in Computer Science },
volume = 1376,
publisher = { Springer },
pages = { 365--380 },
year = 1998
}
@Misc{Padawitz99,
title = { Integrating Functional-Logic And State-Oriented
Specifications },
author = { Peter Padawitz },
year = { 1999 },
note = { Presented at WFLP'99. {\tt
https://issan.informatik.uni-dortmund.de/~peter} }
}
@Misc{Padawitz99a,
title = { Swinging Types = Functions + Relations + Transition
Systems },
author = { Peter Padawitz },
year = { 1999 },
note = { In preparation. {\tt
https://issan.informatik.uni-dortmund.de/\~{ }peter}
}
}
@Book{Papadimitriou94,
author = { Christos H. Papadimitriou },
title = { Computational Complexity },
publisher = { Addison-Wesley },
address = { New York },
year = { 1994 }
}
@InProceedings{Pawlowski96,
title = { Context Institutions },
author = { Wieslaw Pawlowski },
booktitle = { Recent Trends in Data Type Specification },
editor = { Magne Haveraaen and Olaf Owe and Ole-Johan Dahl },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
volume = 1130,
pages = { 436--457 },
year = 1996,
note = { Proceedings of 11th Workshop on Specification of
Abstract Data Types. Oslo, Norway, September 1995 }
}
@Article{Pigozzi74,
title = { The Join Of Equational Thories },
author = { Don Pigozzi },
journal = { Colloquium Mathematicum },
year = 1974,
volume = 30,
pages = { 15--25 }
}
@Article{PinheiroGoguen96-TOOR,
author = { Francisco Pinheiro and Joseph Goguen },
title = { An Object-Oriented Tool for Trancing Requirements },
journal = ieee-soft,
year = 1996,
pages = { 52--64 },
month = mar,
note = { Special issue of papers from ICRE'96 },
}
@TechReport{RapanottiSocorro92,
author = { Lucia Rapanotti and Adolfo Socorro },
title = { Introducing {FOOPS} },
institution = { Programming Research Group, Oxford University },
year = 1992,
number = { PRG-TR-28-92 },
read = { 2-9,2-10-00 },
reviewed = { 2-10-00 },
review = { Points of note:
0. Very strong reliance on OBJ3 semantics and
features. FOOPS is just OBJ3++. :)
1. Semantics of class inheritance are fixed.
(method redefinition is only contravariant)
See Castago95 for more details.
2. Accessing original versions of methods (i.e.
"super" access) is defined (in a limited fashion
but not supported in the implementation.
3. The term "kind" is used as "sort or class".
4. Views can only be defined between modules and
theories at the same level in the language in
the present implementation.
5. View definitions can even be more terse than as
seen in OBJ3. In particular, a class, sort,
operator, attribute, or method can be used as
the view to construct a default abbreviated view
to the theory or module containing the construct.
Thoughts:
0. Kind Theory is just FOOPS extended to the
meta-level.
1. Use of diagrams was claimed to be essential in
GoguenTracz97. Consider the use of UML and OPEN
as self-specification at the metalevel plus the
use of Category Theory. (!) }
}
@InCollection{Reichel81,
title = { Behavioural Equivalence -- A Unifying Concept For
Initial And Final Specifications },
author = { Horst Reichel },
editors = { M. Arata and L. Varga },
year = 1981,
booktitle = { Proceedings, Third Hungarian Computer Science
Conference },
publisher = { Akademiai Kiado },
note = { Budapest }
}
@Article{Reichel95,
title = { An Approach To Object Semantics Based On Terminal
Co-Algebras },
author = { Horst Reichel },
journal = { Mathematical Structures in Computer Science },
year = 1995,
volume = 5,
pages = { 129--152 }
}
@Article{Rodenburg91,
title = { A Simple Algebraic Proof Of The Equational
Interpolation Theorem },
author = { Pieter Hendrik Rodenburg },
year = 1991,
journal = { Algebra Universalis },
volume = 28,
pages = { 48--51 }
}
@TechReport{RodenburgGlabbeek88,
author = { Pieter Hendrik Rodenburg and Rob van Glabbeek },
title = { An Interpolation Theorem In Equational Logic },
year = 1988,
institution = { CWI },
number = { CS-R8838 }
}
@Misc{Rosu,
title = { Kan Extensions Of Institutions },
author = { Grigore Ro\c{s}u },
note = { Submitted for publication }
}
@Article{Rosu00,
author = { Grigore Ro\c{s}u },
title = { Equational Axiomatizability For Coalgebra },
journal = { Theoretical Computer Science },
year = { to appear, 2000 }
}
@Article{Rosu94,
title = { The Institution Of Order-Sorted Equational Logic },
author = { Grigore Ro\c{s}u },
journal = { Bulletin of EATCS },
year = 1994,
volume = 53,
pages = { 250--255 }
}
@Misc{Rosu96,
title = { Axiomatizability In Inclusive Equational Logic },
author = { Grigore Ro\c{s}u },
note = { Submitted to publication },
year = 1996
}
@InProceedings{Rosu98,
title = { A Birkhoff-Like Axiomatizability Result For Hidden
Algebra And Coalgebra },
author = { Grigore Ro\c{s}u },
booktitle = { Proceedings of the First Workshop on Coalgebraic
Methods in Computer Science (CMCS'98), Lisbon,
Portugal, March 1998 },
publisher = { Elsevier Science },
editor = { Bart Jacobs and Larry Moss and Horst Reichel and
Jan Rutten },
pages = { 179-196 },
volume = 11,
series = { Electronic Notes in Theoretical Computer Science },
year = 1998
}
@Misc{Rosu99,
title = { Abstract Semantics For Module Composition },
author = { Grigore Ro\c{s}u },
year = 1999,
note = { In preparation }
}
@InCollection{Rosu99,
title = { Behavioral Coinductive Rewriting },
author = { Grigore Ro\c{s}u },
editor = { Kokichi Futatsugi and Joseph A. Goguen and Jos\'e
Meseguer },
booktitle = { { OBJ }/{ CafeOBJ }/Maude At Formal Methods '99 },
publisher = { Theta },
note = { Proceedings of a workshop held in Toulouse, France,
20th and 22nd September 1999 },
year = 1999,
pages = { 179--196 }
}
@InProceedings{RosuGoguen99,
author = { Grigore Ro\c{s}u and Joseph A. Goguen },
title = { Hidden Congruent Deduction },
booktitle = { First-Order Theorem proving --- FTP'98 },
pages = { 213--223 },
location = { Schloss Wilhelminenberg, Vienna, November 23-25 },
year = 1999,
editor = { Ricardo Caferra and Gernot Salzer },
series = { Springer Lecture Notes on Artificial Intelligence },
note = { Revised version available online. },
url = { https://www-cse.ucsd.edu/users/goguen/ps/cong.ps.gz
},
summary = { This paper extends all the main notions and results
of hidden algebra to operations that may have more
than one hidden argument, and also introduces the
notion of cobasis, gives criteria for operations to
be congruent, and introduces more powerful rules of
deduction. }
}
@Misc{RosuGoguen99,
title = { Circular Coinduction },
author = { Grigore Ro\c{s}u and Joseph A. Goguen },
note = { Submitted to publication },
year = 1999
}
@Book{Rudeanu63,
author = { Sergiu Rudeanu },
title = { Axiomele Laticilor \C{S}I ale algebrelor
booleene\footnote{Lattice and Boolean Algebra
Axioms.} },
year = { 1963 },
publisher = { Romanian Academy Press },
}
@TechReport{Rutten96,
author = { J.J.M.M. Rutten },
title = { Universal Coalgebra: A Theory Of Systems },
year = 1996,
institution = { CWI },
number = { CS-R9652 }
}
@Misc{SalibraScollo91,
title = { A Soft Stairway To Institutions },
author = { Antonino Salibra and Giuseppe Scollo },
year = 1991,
note = { University of Pisa }
}
@InCollection{SannellaTarlecki86,
author = { Donald Sannella and Andrzej Tarlecki },
title = { Extended {ML}: An Institution Independent Framework
For Formal Program Development },
year = 1986,
booktitle = { Proceedings, Summer Workshop on Category Theory and
Computer Programming },
location = { University of Surrey, Guildford, U.K. },
publisher = { Springer },
note = { Lecture Notes in Computer Science, Volume 240 },
pages = { 364--389 },
editor = { David Pitt and Samson Abramsky and Axel Poign\'e
and David Rydeheard }
}
@Article{SannellaTarlecki87,
title = { On Observational Equivalence And Algebraic
Specification },
author = { Donald Sannella and Andrzej Tarlecki },
year = 1987,
journal = { Journal of Computer and System Science },
volume = 34,
pages = { 150--178 }
}
@Article{SannellaTarlecki88,
author = { Donald Sannella and Andrzej Tarlecki },
title = { Specifications In An Arbitrary Institution },
year = 1988,
journal = { Information and Control },
volume = 76,
pages = { 165--210 }
}
@Article{Shutt1989,
author = { Shutt, {R.N.} },
title = { A Rigorous Development Strategy Using The { OBJ }
Specification Language And The Malpas Program
Analysis Tools },
journal = lncs,
volume = { 387 },
year = { 1989 },
pages = { 260--291 }
}
@Book{Sipser96,
author = { Michael Sipser },
title = { Introduction To The Theory Of Computation },
publisher = { PWS },
year = { 1996 },
address = { Boston, MA },
}
@PhdThesis{Socorro93,
author = { Adolfo J Socorro Ramos },
title = { Design, Implementation And Evaluation Of A
Declarative Object-Oriented Programming Language },
school = { Oxford University },
year = { 1993 }
}
@Misc{Stefaneas93,
author = { Petros Stefaneas },
title = { Chartering Some Institutions },
note = { MSc Thesis, Programming Research Group, Oxford
University },
year = 1993
}
@InCollection{Tarlecki84,
title = { Free Constructions In Algebraic Institutions },
author = { Andrzej Tarlecki },
booktitle = { Proceedings, International Symposium on
Mathematical Foundations of Computer Science },
editor = { M.P.\ Chytil and V.\ Koubek },
location = { Prague },
year = 1984,
pages = { 526--534 },
publisher = { Springer }
}
@InCollection{Tarlecki86,
author = { Andrzej Tarlecki },
title = { Bits And Pieces Of The Theory Of Institutions },
year = 1986,
booktitle = { Proceedings, Summer Workshop on Category Theory and
Computer Programming },
location = { University of Surrey, Guildford, U.K. },
publisher = { Springer },
note = { Lecture Notes in Computer Science, Volume 240 },
pages = { 334--360 },
editor = { David Pitt and Samson Abramsky and Axel Poign\'e
and David Rydeheard }
}
@Article{Tarlecki86a,
title = { On The Existence Of Free Models In Abstract
Algebraic Institutions },
author = { Andrzej Tarlecki },
journal = { Theoretical Computer Science },
year = 1986,
volume = 37,
pages = { 269--304 }
}
@Article{Tarlecki86b,
title = { Quasi-Varieties In Abstract Algebraic Institutions
},
author = { Andrzej Tarlecki },
journal = { Journal of Computer and System Sciences },
year = 1986,
volume = 33,
number = 3,
pages = { 333--360 }
}
@Misc{Tarlecki87,
author = { Andrzej Tarlecki },
title = { Institution Representation },
note = { Unpublished note, Dept. of Computer Science,
Univ. of Edinburgh },
year = { 1987 }
}
@InProceedings{Tarlecki96,
title = { Moving Between Logical Systems },
author = { Andrzej Tarlecki },
booktitle = { Recent Trends in Data Type Specification },
editor = { Magne Haveraaen and Olaf Owe and Ole-Johan Dahl },
publisher = { Springer },
series = { Lecture Notes in Computer Science },
volume = 1130,
pages = { 478--502 },
year = 1996,
note = { Proceedings of 11th Workshop on Specification of
Abstract Data Types. Oslo, Norway, September 1995 }
}
@TechReport{Tarlecki96a,
author = { Andrzej Tarlecki },
title = { Structural Properties Of Some Categories Of
Institutions },
institution = { Institute of Informatics, Warsaw University },
year = 1996
}
@TechReport{TarleckiBurstallGoguen89,
author = { Andrzej Tarlecki and Rod Burstall and Joseph Goguen
},
title = { Indexed Categories As A Tool For The Semantics Of
Computation },
institution = { Programming Research Group, Oxford University },
year = 1989,
number = { PRG-77 },
month = aug,
abstract = {This paper presents indexed categories, which model
uniformly defined families of categories, and
suggests that they are a useful tool for the working
computer scientist. An indexed category gives rise
to a single flattened category as a disjoint union
of its component categories plus some additional
morphisms. Similarly, an indexed functor (which is a
uniform family of functors between the component
categories) induces a flattened functor between the
corresponding flattened categories. Under certain
assumptions, flattened categories are (co)complete
if all their components are, and flattened functors
have left adjoints if all their components
do. Several examples are given. Although this paper
is part 3 of the series "Some Fundamental Algebraic
Tools for the Semantics of Computation," it is
entirely independent of parts 1 and 2.}
}
@Article{TarleckiBurstallGoguen91,
title = { Some Fundamental Algebraic Tools For The Semantics
Of Computation, Part 3: Indexed Categories },
author = { Andrzej Tarlecki and Rod Burstall and Joseph
A. Goguen },
journal = { Theoretical Computer Science },
year = 1991,
volume = 91,
pages = { 239--264 }
}
@Article{Tarski44,
title = { The Semantic Conception Of Truth },
author = { Alfred Tarski },
year = 1944,
journal = { Philos. Phenomenological Research },
volume = 4,
pages = { 13--47 }
}
@InProceedings{Tracz93,
author = { William Tracz },
title = { {\Sc Lileanna}: a Parameterized Programming
Language },
booktitle = { Proceedings, Second International Workshop on
Software Reuse },
month = { March },
year = 1993,
note = { Lucca, Italy },
pages = { 66--78 }
}
@TechReport{Veglioni97,
author = { Simon Veglioni },
title = { Classification in Algebraic Specifications of
Abstract Data Types },
institution = { Programming Research Group, Oxford University },
year = 1997,
number = { TR-7-96 },
month = aug,
abstract = { In this paper we describe the role classification
play in algebraic approaches to specification of
Abstract Data Types (ADTs) and show how they
influence expressivity and mechanizability. In the
last two decades many different logic systems for
the algebraic specification of ADTs have been
developed, each one pursuing its own principles and
goals. Since a careful analysis of these logical
systems, taking into account not only their
expressivity, but also their mechanizability, is
important to clarify and organizse a rather rich and
controversial subject - for example overloading is a
topic that needs to be clarified - we believe our
contribution will be useful. Mechanizability of
logical systems is in fact as important as
expressivity, and becomes crucial for those logical
systems which are meant to define the semantics of
declarative and rapid prototyping languages. We have
taken great care to present all arguments in this
paper in as elementary a way as possible, in order
to make the paper accessible to non-expert readers,
even though a minimum knowledge of category theory
and institutions might be of help in few points. }
}
@Misc{Winkler-NewFeatures,
author = { Timothy Winkler },
title = { Introducing { OBJ3 }'s New Features },
howpublished = { Included with OBJ3 distribution. }
}
@Misc{WinklerMeseguer-Builtins,
author = { Timothy Winkler and Jos\'e Meseguer },
title = { { OBJ3 }'s Built-ins },
howpublished = { Included with OBJ3 distribution. }
}
@Misc{Wis2,
title = { Weak Inclusion Systems; Part 2 },
author = { Virgil Emil C\u{a}z\u{a}nescu and Grigore Ro\c{s}u
},
note = { Submitted for publication }
}
@TechReport{Wolfram93,
author = { {D.A.} Wolfram },
title = { An Implementation Of Higher-Order Rewriting
(Extended Abstract) },
institution = { Programming Research Group, Oxford University },
year = 1993,
number = { TR-8-93 },
month = jun,
abstract = { We discuss an implementation of a restricted form
of higher-order rewriting. It is illustrated with
encodings of programs that have been derived using
the functional form of the Bird-Meertens
Formalism. The implementation allows
"leftmost-outermost" and "rightmost-innermost"
rewriting orders to be selected, and conditional
higher-order rewrite rules to be used. The results
are encouraging and suggest that systems which use
rewrite rules can achieve greater conciseness,
applicability, and efficiency. }
}
@Article{WoodwardAllen1998,
author = { Woodward, { M.R. } and Allen, { S.P.}},
title = { Slicing Algebraic Specifications },
journal = { Information And Software Technology },
volume = { 40 },
number = { 2 },
year = { 1998 },
pages = { 105--118 }
}
@TechReport{Worrel97,
author = { James Worrell },
title = { A Topos Of Hidden Algebras },
year = 1997,
institution = { Programming Research Group, Oxford University },
number = { PRG-TR-28-97 }
}
@Misc{Yukawa90,
title = { The Untyped Lambda Calculus As A Logical
Programming Language },
author = { Keitaro Yukawa },
year = 1990,
note = { City University of New York }
}