Some personal choices of What's Cool on
the web
Contents
- In Computer Science
- In Semiotics, Sociology, Science Studies, Music,
etc.
- From this Website
1. In Computer Science
1.1 Hidden Algebra, Behavioral Logic,
Coalgebra, etc.
- There is a Behavioral Discussion List, to facilitate progress on
behavioral aspects of computer science and mathematics, including but not
limited to, versions of hidden algebra and behavioral equational logic,
observational logic, and coalgebra, as well as systems that support them,
such as BOBJ, CafeOBJ and Kumo.
- The Behavioral Homepage
lists all members of the Behavior Discussion List, with links to their
homepages whenever we could find them; this is maintained by Grigore Rosu.
- UCSD mirror site for
Japan Advanced Institute of Science and Technology (JAIST) CafeOBJ homepage. CafeOBJ is a
successor to OBJ3 based on hidden algebra and rewriting logic, implemented
under the direction of Prof. Kokichi Futatsugi at JAIST.
- Website of Grigore Rosu at
University of Illinois, Champaign-Urbana; much material on hidden algebra,
behavioral logic, formal methods, and their applications.
- Website of Razvan Diaconescu at
Institute of Mathematics of the Romanian Academy; neat stuff on the constraint
paradigm, behavioral rewriting logic, CafeOBJ and more, including notes on the
First Romanian-Japanese
Algebraic Specification Meeting.
- Website of Horst Reichel
at Dresden; neat stuff on coalgebraic semantics, with applications to the
object paradigm.
- Website of Grant Malcolm
at University of Liverpool; neat stuff on hidden algebra, sheaf semantics,
ontologies, term rewriting, biology, ...
- Website of Peter Padawitz at
Universitaet Dortmund, Germany; behavioral deduction and declarative
programming in his "swinging
types" framework.
- Website of Rolf
Hennicker at the University of Munich; good stuff on coalgebra, etc.
- Website of Bart Jacobs at
Nijmegen, the Netherlands (formerly CWI, Amsterdam); more neat stuff on
coalgebraic semantics for the object paradigm, and also for hybrid systems.
- FLIRTS - Formalism
Logic Institution: Relating, Translating and Structuring; group working
on translations among institutions and related matters; this website includes
listings of people, conferences, and papers.
- IFIP WG 1.3, on
Foundations of System Specification.
- European Common Framework Initiative
(CoFI), a project to build a Common Framework for Algebraic Specification,
especially a specification language called CASL.
- Maude homepage at the Computer
Science Lab of SRI. Maude incorporates most features of OBJ3, sometimes with
small syntactic changes, and adds an implementation of rewriting logic, a powerful new
rewriting engine, and the membership equational logic version of order sorted
equational logic.
- Website of AMAST
(Algebraic Methodology and Software Technology, an organization devloted
to the promotion of algebra in computer science.
- Declarative group website on algebraic
semantics at Oxford, including links to Grant Malcolm, Corina Cirstea,
James Worrell, Simone Veglioni, Sula Ma, and Andrew Stevens. Note: Grant Malcolm is now at the
University of Liverpool.
- Homepage of the Kestrel Institute,
whose SpecWare product is to a large degree based on ideas from Clear, OBJ,
etc., including an explicit command for taking the colimit of a diagram of
theories.
- Website of Razvan Diaconescu at
Institute of Mathematics of the Romanian Academy; neat stuff on the constraint
paradigm, behavioral rewriting logic, CafeOBJ and more, including notes on the
First Romanian-Japanese
Algebraic Specification Meeting.
- Website of Amilcar
Sernadas at Technical University of Lisbon, Portugal; theory and
applications of institutions, object paradigm, fibring, modal logic, and more.
- Frank Pfennig's website on logical frameworks, at CMU
(but not updated very recently).
- A term rewriting homepage at
Loria (Laboratoire Lorrain de Recherche en Informatique et ses Applications),
Nancy, France; maintained by Nachum Dershowitz and Laurent Vigneron.
- Homepage of the Rewriting
Techniques and Applications (RTA) Conference.
- An online textbook, Tree
Automata Techniques and Applications, by Herbert Comon, Max Dauchet, Remi
Gilleron, Denis Lugiez, Sophie Tison and Marc Tommasi; still under
construction.
- Website of Jean-Pierre
Jouannaud in Paris; term rewriting theory, especially higher order term
rewriting, and more.
- Homepage of Neil Ghani at
the University of Birmingham; categorical term rewriting; links to the Fall
homepage and other great pop groups.
- Homepage of Don
Pigozzi at University of Iowa: algebraic logic, algebraic theory of
abstract data types.
- Rippling
FAQ, by Alan Bundy; rippling is a generalization of term rewriting that
seems to apply well to inductive proofs.
1.4 Theorem Proving
- Website of the LEGO
group at the University of Edinburgh.
- Homepage of the PVS
theorem proving project at SRI.
- Website of Alexander
Leitsch at the Technical University of Vienna; neat stuff on resolution
theorem proving, including model building.
1.5 Interface Design, HCI, etc.
- Homepage of User Interfaces for
Theorem Provers interest group and conferences.
- Best website I know on graphical design for the web, the Yale Style
Manuual.
- Putting People First, a blog
on experience design, user experience, etc., by Mark Vanderbeeken.
- del.icio.us, a social bookmark
manager.
- Flickr map tags
for "memory maps".
- www.metafilter.com, a communal blog
that supports tagging.
- You're It, a blog on tagging.
- Interactive applet proof of Pythagorean Theorem by Robert
Morey; grand prize winner of 1995 Sun Java contest; much improved since.
- Gallery of Interactive Geometry at
University of Minnesota; pinball in negatively curved space; also ftp site for
WebEQ, a Java enabled math notation.
- Current Issues in Web
Usability, short articles on linkrot, etc. by Jakob Nielsen.
- Homepage of Michiaki Yasumura at
Keio University; research on human computer interfaces, design, multimodal
interaction, etc.
-
Towards a Theory of Ethical Linking, an extreme example of the hypertext
medium; lots of links, less content; amusing if you don't spend too much time
on it.
1.6 Miscellaneous
- Website of Phil
Bernstein, at Microsoft Research; work on databases, especially data
integration using meta-data, called "model management."
- Website of Minciu Sodas Lab, in Vilnius
Lithuania; work on import/export standards for handheld devices; directed by
Andrius Kulikauskas.
- Homepage of Sony Computer Science
Lab, Tokyo Japan.
- An amusing page on the Axiom of Choice,
with interesting links to related topics, e.g., in mechanical theorem proving.
- Homepage of the Bootstrap Institute
which honors and continues work of Doug Engelbart, who is many ways should be
considered the father of the PC.
- CiteSeer, an online publication
indexing service for computer science; see also their Most Cited Authors in Computer
Science list.
- Homepage of ACM TechNews
homepage, a selection of current IT news items.
- Search
Tickler.
- Many Computer
Science Education Links to various sites; see also the site of ACM special interest group SIGCSE.
- The Erdos Number
Project. What is your Erdos number?
- Website of DaliLab, a cool startup,
from Joe Kiniry.
- Risks Forum homepage;
information on computer system risks, failures, etc.
- UCSD Women in Computing site.
- Website of Oscar Nierstrasz
at Bern, Switzerland (formerly Geneva); interesting information and many links
on object oriented systems and software composition.
2. In Semiotics, Sociology, Science Studies, Human Computer
Interface, Music, etc.
2.1 Semiotics, Metaphor, etc.
- Bibliography on semiotics and
information at Aalborg University, Denmark, maintained by Peter Bogh Andersen, who has done some
fascinating work on phase space driven multimedia systems.
- Homepage of International Cognitive
Linguistics Association; links to researcher's homepages, recent papers,
conferences, etc.
- Homepage of John
Pickering; interesting things on semiotics, consciousness, and
psychology.
- Extensive semiotics index
at University of Colorado at Denver; many interesting links.
- Website on semiotics at
National Institute of Standards and Technology; emphasizes practical
applications.
- Semiotics for
Beginners, by Daniel Chandler, University of Wales, Aberystwyth; a good
place to begin. There is a US
mirror site.
- An
Introduction to Semiotics for HCI, by Mihai Nadin, University of
Wuppertal, Germany; motivation and some interesting historical background, for
applying semiotics to interface design.
- Website on blending (and
metaphor), work of Mark
Turner, Gilles
Fauconnier, and others, in an exciting area of cognitive linguistics.
(Blends are related to pushouts - see Introduction to
Algebraic Semiotics).
- Bakhtin
Centre homepage at Sheffield University (UK).
- Ray Paton's
Metaphor in Scientific Thinking Page at Liverpool University, England; see
especially his paper Glue, Verb and Text
Metaphors in Biology, from Acta Biotheoretica.
2.2 Art, Music, etc.
- Music
Structure.com, uses a hidden Markov model to analyze structure of music,
and puts it into MPEG-7.
- Steve's Coleman's M-Base, including
loads of cool MP3 files.
- Interesting overview of art
schools in Japan, via NY Museum of Modern Art.
- Homepage of Vernon
Vinge, interesting science fiction material, especially his essay, The Coming Technological Singularity.
- Digital Art Source, a
resource for digital media news, events, books, etc.
- Bodies
Incorporated, internet art project by Victoria Vesna; many interesting and unusual
links are on her homepage.
- Cool image sites ipix and dream (use your mouse).
- Ruth Wallen's cool ecology-art frog site; see also
her ecoart site and her View Points site.
- Website of Adelheid Mers, an
interesting Chicago-based conceptual artist. There are also many interesting
links on this site, e.g., to George Lakoff's ideas on the current political
dabate from his book Moral Politics.
- Mirror of the original Laurie
Anderson Home of the Brave tour site; the green room has an amazing recipe
for electric hotel hotdogs; also a complete index
to all webed information on Laurie Anderson, and an interview.
- Some wonderful artistic
graphics with a mathematical flavor.
- Some wonderfully mysterious artistic
graphics.
2.3 People
- Information about
Geoff Bowker and Leigh Star, who are at
Santa Clara University Center for Science, Technology & Society; they
have done interesting work on information systems, biodiversity, information
infrastructure, classification systems, medical records, and more.
- Homepage of Phil Agre,
lots of interesting stuff on communication, media, privacy, politics,
libraries, the net, and life.
- Homepage of Andrew Odlyzko,
fascinating material on networks, privacy, electronic publishing, electronic
commerce, etc.
- Homepage of Mark Ackerman,
at UC Irvine; great stuff on electronic media.
- Homepage of Chrystopher Nehaniv,
interesting work on interaction, imitation, semigroups, evolvability, and
automata.
- Homepage of Walter Freeman, lots
of interesting stuff on neuroscience.
- Homepage of Wesley
Phoa, interesting material on Heidegger and art, and on financial
planning.
- Homepage of Richard Boland;
interesting material on management and design.
2.4 Other Topics
- Journal of
Consciousness Studies homepage - winner of Key Resource Award from
links2go.
- Science and Consciousness
Review.
- Center for Computing & the
Arts.
- BBC Radio 3, probably the
best classical music station in the world; see also BBC Radio 1, which sometimes has great
emerging pop, world music, etc. shows (John Peel, alas, is gone but you can
still download some old shows).
- Benetech, a non-profit
organization seeking to apply Silicon Valley thinking to help disadvantaged
communities through technology.
- Managing as Design Workshop, 14-15
June 2002 at the Weatherhead School of Management of Case Western Reserve
University, organized by Richard Boland.
Many other interesting
papers can be found on the workshop website, including those by Richard Boland
(the organizer), Geoffrey Bowker, Yjro Engestrom, Frank Gehry (the architect
of the building where it was held), Leigh Star, Lucy Suchman, and Ina Wagner.
See also the original "provocations" on the workshop's ideas page.
- Distributed Collective
Practices conference, hold 6-9 February 2002 at UCSD.
- Homepage of the UCSD Science
Studies Program, courses, degrees, people, colloquium series, and many
links to other resources on science studies.
- Activity theory
homepage: links to pages on the work of Vygotsky, Luria, Leontiev and
their followers.
- Optical illusions, puzzles, and
art, showing how the eye can be tricked, by Al Seckel and Christoph Koch,
Cal Tech.
- Historical Spam Museum and
Archive.
-
Requirements Engineering Bulletin Board at the Oxford Centre for
Requirements and Foundations, maintained by Richard Tolcher.
- The Dead Media websites are www.well.com/user/jonl/deadmedia,
www.islandnet.com/~ianc/dm/dm.html, and griffin.multimedia.edu/~deadmedia.
Archives containing many strange and interesting media that are now deceased;
the last site is a sound archive.
- The Edge, a strange but interesting
on-line magazine.
- The San Jose Mercury News tends
to put up well designed journalistic subsites, with good applet maps, etc.
- The subgenius site; good graphics
design but a bit distracting; a new religion invented as a joke.
- Timothy Leary's home, great
organization (moving through rooms of his house, views of each wall, with "hot
objects"), and links to interesting cultural sites (if you ignore the plugs
for psychedelic drugs); received award for best personal homepage in 1996
(despite the "person" being deceased!).
- The original Heaven's Gate site;
good graphic design but lots of advertising added, so you might prefer one of
the mirror sites.
- Virtual
Frog Dissection Kit.
- A strange but
elegant clock.
- Shambhala, a Tibetan Buddhist
organization, with many teaching and meditation centers worldwide; see also
the San Diego center
website.
- Dharmaling, an interesting and
colorful site on Tibetan Buddhism, with a European focus.
- An amusing Zen site do-not-zzz.
- Website of the emerging UCSD
Management School.
3. From this Website
- The homepage of the tatami project gives a
general introduction to the project, and includes links to the following
online interactive examples listed below. Although not all these websites
illustrate hidden algebra, it is advisable to visit them in the order given,
as they were assembled as an integrated sequence for pedagogical purposes;
these examples are linked with an online tutorial on hidden algebra, which is also
linked to background tutorials on first order logic and proof planning.
- An inductive proof that 1+...+
n = n(n+1) / 2. This will give you a chance to explore Kumo's
navigation and display conventions on a simple example.
- A coinductive proof of a
behavioral property of a simple flag object. This illustrates some basics
of the hidden algebra approach on a very simple example; it gives an
especially clear explanation of the need for behavioral properties.
- Two proofwebs are given for some familiar inductive properties of lists.
The first was generated by a duck score written at the beginning of this
effort; it is striking that the lemmas needed to complete the proof can be
deduced from the way that successive proof attempts fail. The second proofweb
succeeds, and was generated by a duck score derived from the first just by
reordering its goals so that the lemmas that were found necessary are proved
first.
- This early attempt at
proving that the reverse of the reverse of a list is the list, takes a direct
approach, and its explanations emphasize the way that the two lemmas that are
needed to complete the proof can be deduced from the output produced by
unsuccessful proof attempts; one of these lemmas is the associativity of
append.
- Here are the complete proofs
for all three inductive properties of lists, including the two lemmas
that are needed to establish the main goal.
- A coinductive proof of the behavioral correctness of the
array-with-pointer implementation of stack. This behavioral refinement
proof requires introducing a non-trivial lemma, which can also be inferred
from a prior proof attempt that fails without it.
- A behavioral refinement proof of the correctness of implementing sets with
lists, using attribute coinduction.
Note: This is still under
construction; some explanations are missing.
- A simple inductive proof of a formula for the sum of the squares of the first n natural numbers. This example is deliberately very
spare, and in particular has no explanations, in order to illustrate the
default conventions that Kumo uses when a user supplies only the absolute
minimum input.
- A somewhat detailed proof that the square root of 2 is
irrational, illustrating the first order capabilities of Kumo. Note that
this uses and proves many auxiliary lemmas; see the directory listing. Note: no
explanations have as yet been provided for any of the proofs.
- A coinductive correctness proof for the tatami protocol, which maintains the
consistency of distributed cooperative proofs that are built using the tatami
system.
All these except the last were generated by version 4 of Kumo,
implemented by Kai Lin; Netscape 3.0 or later and
some knowledge of hidden algebra are needed. Eventually the Java source code
will also be available for downloading via the Kumo homepage. Kumo is both a proof assistant and
a proof website generator, though users must supply the specifications,
explanations (if any), and goals. Using Kumo guarantees that the proofs are
completely formally correct. Several of these examples also have illustrative
Java applets, and there is live proof execution via a BOBJ server. Initial
work on Kumo was supported by the large international CafeOBJ Project (see the CafeOBJ Press Release).
- Visit the "world-famous" San Diego Semiotic
Zoo for an astonishing collection of exotic semiotic morphisms, each
an example of bad design arising through failure to preserve some relevant
structure. (Notes: (1) This is a new location for the zoo, which is
still under construction,and currently lacks explanations for some exhibits;
(2) the zoo won a "Creativity Award" from Art & Technology.)
- There are now homepages for each of the following major areas of my
research: See also the Meaning and Computation Lab homepage.
- Final version of Introduction to Algebraic
Semiotics, with Applications to User Interface Design, Joseph Goguen,
in Computation for Metaphor, Analogy and Agents, edited by Chrystopher
Nehaniv, Springer Lecture Notes in Artificial Intelligence, volume 1562, 1999,
pages 242-291. This is the basic paper on algebraic semiotics, with
3/2-categories, 3/2-colimits, and many examples, especially from user
interface design; completed 28 December 1998. A preliminary version appeared
in Proceedings, Conf. on Computation for Metaphor, Analogy and Agents
(Aizu-Wakamatsu, Japan, 6-10 April 1998) pages 54-79, an earlier version of
which is Semiotic Morphisms, Technical Report CS97-553, August 1997.
A now obsolete extended abstract appeared in Proceedings, Conference on
Intelligent Systems: A Semiotic Perspective, Volume II (National Institute of
Standards and Technology, Gaithersberg MD, 20-23 Oct 1996) pages 26-31.
- CSE 175: Social and Ethical Issues in
Information Technology, Winter 2001. An undergraduate course on the
pervasive social and ethical issues that arise in the actual practice of
computer science work. (Formerly CSE 190B.)
- CSE 230: Principles of Programming
Languages, Winter 2002. UCSD CSE core graduate course on the
principles that underlie the various types of programming langauges; includes
some introductory material on algebraic semantics.
- CSE 130: Principles of Programming
Languages, Winter 2002. UCSD CSE undergraduate course on the
principles that underlie the various types of programming langauges.
- CSE 171: User Interface Design: Social and
Technical Issues, Spring 2002. An undergraduate introduction to user
interface design, semiotics, etc..
- CSE 271: User Interface Design: Social and
Technical Issues, Spring 2002. A graduate level introduction to user
interface design, algebraic semiotics and more.
- CSE 275: Social Aspects of Technology and
Science, Fall 2000. Relations between society, technology and
science, with emphasis on information technology.
- Algebraic Semantics of Imperative
Programs, by Joseph Goguen and Grant Malcolm (MIT Press, 1996). ISBN
0-262-07172-X. Covers most features of imperative language using algebraic
semantics; many exercises that can be done using OBJ3; also contains entry
level introductions to universal algebra and OBJ3. [The paper An Executable Course in the Algebraic Semantics of
Imperative Programs discusses some pedagogical innovations of this
book.]
- Software Engineering with OBJ: algebraic specification in action,
edited by Joseph Goguen and Grant Malcolm, Kluwer, April 2000; ISBN
0-7923-7757-5. A book on OBJ3 and its applications. The paper Introducing OBJ, which is essentially a user manual
for OBJ3, was revised and extended in August 1999. The Introduction with a table of contents, and the
paper More Higher Order Programming with
OBJ3, are also available.
- Two chapters from Theorem proving and Algebra, by Joseph Goguen, to be published by MIT Press, someday: Chapter 1, Introduction and Chapter 8, First Order Logic, plus the References and the Table of
Contents. Chapter 8, an elegant algebraic exposition of first order
logic, proof planning and induction, was finished 15 September 1998; the
approach to induction is unusually general, and there are many examples.
- Art and the Brain, Part 3, edited by
Joseph Goguen and Erik Myin, Imprint Academic, ISBN 0-907-84598-3; also in Journal of Consciousness
Studies, vol. 11, no. 3/4, pages 5-8, 2004; a special issue with a
focus on music. The Editorial Introduction
is available.
- Art and the Brain, Part 2, edited by Joseph Goguen and Eric Myin;
special issue of Journal
of Consciousness Studies, volume 7, no. 8/9, 2000. Joseph Goguen's
introduction on pages 7-15, What is
Art? is available, as is his review
on pages 157-160 of Visual Space Perception: A Primer, by Maurice
Hershenson (MIT 1998).
- Art and the
Brain, Part 1, edited by Joseph Goguen, Imprint Academic, October
1999; ISBN 0-907-84545-2; also appeared as Journal of Consciousness
Studies, volume 6, No. 6/7, June/July 1999. Joseph Goguen's Editorial Introduction, on pages 5-14, is
available.
- Editorial Introduction to Art and the Brain, Part III , with Erik
Myin, Imprint Academic, ISBN 0-907-84598-3; also in Journal of Consciousness
Studies, vol. 11, no. 3/4, pages 5-8, 2004; a special issue with a
focus on music.
4. Some Software Used in the Kumo System
See also my What's New page.
Maintained by Joseph Goguen
Last modified: Sat Sep 3 08:47:55 PDT 2005