以下は、説明は全部省略して、単に僕が見ている“景色”を述べるだけです、あしからず。
と書いたのですが、参考になりそうなURLだけ記しておきます。
インスティチューションの中心人物はGoguen（http://www.cs.ucsd.edu/users/goguen/）です。彼のインスティチューション・ページ（http://www.cs.ucsd.edu/~goguen/projs/inst.html）をハブに使えます。
抽象モデル論という発想はバーワイズ（Barwise）が先のようですが、文（sentence、命題、制約）の集合を天下りに“単なる集合SenΣ”にしてしまったところが、Goguen/Burstallの割り切り。バーワイズもGoguenも、分野横断的に精力的な活動をしていて、現代のプチ“ダ・ビンチ”という感じですね。
Maude（http://maude.cs.uiuc.edu/）やCASL（http://www.cofi.info/CASL.html）などの仕様記述言語では、背後にインスティチューションがあります。例えば、CASLをやっているTill Mossakowski（http://www.tzi.de/~till/）はインスティチューションの具体的な使い方をいろいろ書いています。二木スクールによる国産の仕様記述言語（と実行系）CafeOBJもインスティチューションで解釈されますね。CafeOBJのホームページがどこかよくわからないのだけど、http://www.jaist.ac.jp内を探せば資料はイッパイ。
余代数については、Bart Jacobs（http://www.cs.ru.nl/~bart/）とJan Rutten（http://homepages.cwi.nl/~janr/）が解説・啓蒙的な論文も書いています。例えば、Jacobsの"Coalgebras in Specification and Verification for Object-Oriented Languages" (1999) とかはオブジェクト指向言語が話題。JacobsはJavaの形式意味論とかも随分やっています。最近は "Introduction to Coalgebra. Towards Mathematics of States and Observations" という本を執筆中だそうです。余代数の教科書的読み物としてRuttenの"Universal coalgebra: a theory of systems" (2000) がよく引用されます。けっこうな量があるので僕は読んでませんけど(苦笑)。
終余代数のまじめな構成では、Aczelが言い出した、基礎の公理を仮定しない（むしろ積極的に否定する）集合論（ZFC - 基礎の公理 + 反基礎の公理）が使われるようですが、僕はよく分かりません。Lawrence C. Paulson "Final Coalgebras as Greatest Fixed Points in ZF Set Theory" (1999) →http://citeseer.ist.psu.edu/paulson99final.html とか（かな？）。（[追記]日本語で読める資料がありました。http://web.sfc.keio.ac.jp/~mukai/2003-gainen/zfcafa.pdf[/追記]）
マイナーな話ですが、実数を余代数とみなすこともできるそうです。D. Pavlovic, V. Pratt "On Coalgebra of Real Numbers" (1999)→http://citeseer.ist.psu.edu/pavlovic99coalgebra.html、D. Pavlovic, V. Pratt "The Continuum as a Final Coalgebra" (1999)→http://citeseer.ist.psu.edu/pavlovic99continuum.html など。
他に、バーコフ（Birkhoff、Berkoffじゃない）の定理の双対が成立するとか（Steve Awodey, Jesse Hughes "The Coalgebraic Dual Of Birkhoff's Variety Theorem" (2000)→http://citeseer.ist.psu.edu/awodey00coalgebraic.html、Robert Goldblatt "What is the Coalgebraic Analogue of Birkhoff's Variety Theorem?" (2000)→http://citeseer.ist.psu.edu/goldblatt00what.html）、様相論理と相性がいいとか（http://www.cs.le.ac.uk/people/akurz/cml.htmlから色々たどれる）、余代数には良い点がいろいろあります。
隠蔽代数は余代数ほどには盛り上がってないみたいな。とりあえず、Joseph Goguen, Grant Malcolm "A Hidden Agenda" (1997)→http://citeseer.ist.psu.edu/62277.html がハシリでしょうか。隠蔽代数は（僕には）自然に見えますが、余代数に比べると複雑過ぎるのかな？ 両代数（dialgebra）という定式化もありますが、これはよく知らない。
モゴモゴな話
インスティチューションに証明系を付けたものは、entailment systemとかπインスティチューションとか呼ばれるもので既にあります。が、これの“証明”とは仕様記述言語（または制約記述言語）レベルの証明で、古典的な“プログラムの証明”とはどうもストレートに結びつかないのです。
プログラムの証明は、厳密なソースコードレビューみたいなもんだけど、ソースコードに対応するフォーマルな概念が見あたらないのね。だから、ソースレベルの変換とか合成とかを記述すべき場所が分からない。ホーア式のような形でSenΣのなかにソース断片を押し込めるけど、なんか気色悪いよ。
