From bu Fri Jan 21 14:12:32 1994 Date: Fri, 21 Jan 94 14:12:30 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik, kreyss@informatik, drewes@informatik Subject: Vortragsankuendigung Content-Length: 424 Status: RO X-Lines: 16 Liebe Leute, Am Dienstag, den 25.1.94 um 15 Uhr wird Dr. Wolfgang Kreutzer, Univ. of Canterbury, Neuseeland, zwei Vortraege halten mit den Themen: 1) Die MODELERS' WORKBENCH - Experimente zum visuell interaktiven Entwurf & Animation von Simulationsmodellen 2) Zum Stellenwert objektorientierter Programmierstile in der Informatikausbildung Alle Interessierten sind herzlich eingeladen. RAUM: 8090 (wie immer). bu From bu Wed Jan 26 16:10:09 1994 Date: Wed, 26 Jan 94 16:10:07 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik, kreyss@informatik, drewes@informatik Subject: Naechstes Treffen Content-Length: 156 Status: RO X-Lines: 12 Liebe Leute, diesen Freitag 15 Uhr, wie immer 8090, wird Zhenyu Qian berichten ueber die "POPL 94" Alle Interessierten sind herzlich eingeladen. bu From bu Wed Feb 2 16:20:54 1994 Date: Wed, 2 Feb 94 16:20:52 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik, kreyss@informatik, drewes@informatik Subject: EXTRA-Extra Content-Length: 251 Status: RO X-Lines: 14 Liebe Leute, Morgen, am Donnerstag den 3.2. 94, 15 Uhr, Raum 8090, wird Harald Ganzinger sprechen ueber: Termersetzungstechniken fuer transitive Relationen Alle Interessierten (insbesondere der Gruppe Kreowski) sind herzlich eingeladen. bu From olis.isc.north.de!oytix!hochkalter!stefan.north.de!stefan@arbi.informatik.uni-oldenburg.de Mon Jan 17 18:37:08 1994 Date: Mon, 17 Jan 94 11:37:50 +0100 From: stefan@stefan.north.de (Stefan Westmeier) To: bu@informatik Subject: Mein Vortrag am 21.1.94 Cc: qian@informatik, ewk@informatik, bkb@informatik Content-Length: 419 Status: RO X-Lines: 13 Hallo Burkhart, ich habe mit Kolyang besprochen, meinen Vortrag vom 21.1. auf den 18.2. zu verschieben. Ich hoffe das passt Dir (und allen anderen Interessierten). Cioa, Stefan. -- Stefan Westmeier stefan@stefan.north.de Schaphuser Str. 24 Voice+Fax: +(49) 421 406472 D-28307 Bremen Germany - Sun attachements are welcome... From bu Thu Feb 17 17:22:13 1994 Date: Thu, 17 Feb 94 17:22:12 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik, kreyss@informatik, drewes@informatik Subject: EXTRA-Treffen Cc: woel@informatik, nake@informatik Content-Length: 224 Status: RO X-Lines: 13 Liebe Leute, morgen, um 15 Uhr, Raum 8090 traegt Stefan Westmeier im Rahmen seiner Diplomarbeit ueber Der PI-Kalkuel als Mittel zur Beschreibung von Interaktion vor. Alle Interessierten sind herzlich eingeladen. bu From bu Thu Mar 3 12:47:14 1994 Date: Thu, 3 Mar 94 12:47:11 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik.uni-Bremen.de., kreyss@informatik.uni-Bremen.de., drewes@informatik.uni-Bremen.de., Juergen.Bohn@arbi..informatik.uni-oldenburg.de Subject: Naechstes Treffen Content-Length: 901 Status: RO X-Lines: 26 Liebe Leute, diesen Freitag, 15 Uhr (ct), Raum 8090, wird Dr. Maritta Heisel in unserem EXTRA-Treffen einen Vortrag halten ueber: Sprachunabhaengige Unterstuetzung von Spezifikationsstilen Inhalt: Das Vorgehen beim Aufstellen formaler Spezifikationen ist haeufig dadurch bestimmt, welche Spezifikationssprache verwendet wird. Spezifikationssprachen repraesentieren implizit also gewisse Spezifikations"stile". Dies ist vor allem dann von Nachteil, wenn eine Spezifikationssprache verwendet werden muss, die auf das zu loesende Problem nicht besonders gut zugeschnitten ist. In dem Vortrag wird erlaeutert, wie es moeglich ist, Spezifikationsdtile explizit und sprachunabhaengig zu repraesentieren und anzuwenden. Damit kann der Spezifikationsprozess am zu loesenden Problem anstatt der zu loesenden Spezifikationssprache ausgerichtet werden. Alle Interessierten sind herzlich eingeladen. bu From bu Tue Mar 15 12:05:36 1994 Date: Tue, 15 Mar 94 12:05:33 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik.uni-Bremen.de., kreyss@informatik.uni-Bremen.de., drewes@informatik.uni-Bremen.de., herwig@informatik..uni-Bremen.de, heger@inform, andreas@informatik.uni-Bremen.de., roefer@informatik.uni-Bremen.de., michaelh@pc-labor.uni-Bremen.de, holly@pc-labor.uni-bremen.de, svh@pc-labor.uni-bremen.de, blecky@pc-labor.uni-bremen.de Subject: EXTRA-TREFFEN Content-Length: 255 Status: O X-Lines: 11 Liebe Leute, naechsten Freitag, 15 Uhr, MZH 8090, werden kolyang (und ich) berichten von der Tagung der entspr. GI-Fachgruppe: "Semantikgestuetzte Analyse, Entwicklung und Generierung von Programmen" Alle Interessierten sind herzlich eingeladen. bu From bu Tue Mar 22 18:25:18 1994 Date: Tue, 22 Mar 94 18:25:10 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik.uni-Bremen.de., kreyss@informatik.uni-Bremen.de., drewes@informatik.uni-Bremen.de., stefan@stefan.north.de Subject: EXTRA-Treffen Content-Length: 552 Status: O X-Lines: 26 Liebe Leute, der Vortrag von kolyang wurde um 1 Woche verschoben, da zuviele Leute auf der CeBit waren. Also: Am 25.3. Wird Kolyang berichten ueber dem GI-Workshop "Semantikgestuetze Analyse, Programmgenerierung ..." . Am 8.4. wird Liu Jun vortragen ueber "Higher Order Narrowing Strategies" Narrowing is a basic technique for equation solving. The question arises, how can first order basic-with-normalization narrowing-strategy be ext- ended to higher order patterns (Miller 92). Alle Interessierten sind herzlich eingeladen. bu From olis.north.de!oytix!hochkalter!stefan.hb.north.de!stefan@arbi.informatik.uni-oldenburg.de Fri Mar 25 18:32:21 1994 Date: Fri, 25 Mar 94 12:34:45 +0100 From: stefan@stefan.hb.north.de (Stefan Westmeier) To: bu@informatik.uni-Bremen.de. Subject: Re: EXTRA-Treffen Content-Length: 1147 Status: RO X-Lines: 43 Hallo Burkhart, > Liebe Leute, > > der Vortrag von kolyang wurde um 1 Woche verschoben, da zuviele Leute auf der CeBit waren. > > Also: > > Am 25.3. > > > Wird Kolyang berichten ueber dem GI-Workshop "Semantikgestuetze Analyse, > Programmgenerierung ..." . > > > Am 8.4. wird Liu Jun vortragen ueber "Higher Order Narrowing Strategies" > > Narrowing is a basic technique for equation solving. The question arises, > how can first order basic-with-normalization narrowing-strategy be ext- > ended to higher order patterns (Miller 92). > > > Alle Interessierten sind herzlich eingeladen. > > > bu > > Ist bei mir am nächsten Morgen in der Post gewesen. Vielen Dank. Schade, daß ich am 25.3. keine Zeit habe. Ciao, Stefan. P.S.: Im Moment arbeite ich gerade an meiner Diagrammsprache und versuche mir der Haken und Ösen der existierenden Diagrammsprachen bewusst zu machen. -- Stefan Westmeier stefan@stefan.hb.north.de Schaphuser Str. 24 Voice+Fax: +(49) 421 406472 D-28307 Bremen Germany - Sun attachements are welcome... From bu Thu Apr 7 16:08:41 1994 Date: Thu, 7 Apr 94 16:08:39 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik.uni-Bremen.de., kreyss@informatik.uni-Bremen.de., drewes@informatik.uni-Bremen.de., stefan@stefan.north.de Subject: EXTRA-Seminar Typ-und Beweissysteme Content-Length: 2088 Status: RO X-Lines: 96 Liebe Leute, waehrend des folgenden Semesters wird es folgende Vortraege in der ueblichen Zeitschiene (Fr. 15-17 Uhr) am ueblichen Ort (MZH 8090) geben: >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> ANKUENDIGUNG FUER SEMINAR "Typ - und Beweissysteme" 1994 (zusammen mit dem EXTRA-Treffen der Gruppe Krieg-Brueckner) Typisierung ist ein zentrales Konzept in modernen Programmiersprachen und ein fundamentales in einer Reihe von Beweissystemen. Im Seminar werden zu- naechst einige angewandte Typkonzepte aus Programmiersprachen vorgestellt. Dann folgt eine Reihe von Vortraegen zum Thema "Beweissysteme", wobei eine Bruecke zur Typtheorie geschlagen werden soll. Bei Interesse koennen Studenten im letzten Abschnitt Vortraege ueber existierende (und z.T. installierte, also "anfassbare") Beweissysteme vortragen. Das Seminar richtet sich an Studenten des Hauptstudiums sowie die ein- (und hoffentlich be-)schlaegigen Doktoranden. Gruppe I: Typsysteme in Programmiersprachen 15.4. Vorbesprechung (+ ev. einen nicht themenbezogenen EXTRA-Vortrag) 22.4. Entfaellt 29.4. Abhaengige Typen (Termpolymorphie) (bernd) 6.5. Untertypenkonzepte (qian) 13.5. Klassen in HASKELL (kolyang) 20.5. Higher order Funktoren (bernd) 27.5. (Freier Vortrag) 3.6. (entfaellt wg. COMPASS) Gruppe II: Beweissysteme 10.6. Grundlagen formaler Logik und Theorembeweisens (bu) (PROBLEM : Pfingstferien, und mir gefaellts auch nicht) 17.6. Grundlagen Typtheoretischer Ansaetze (liu) 24.6. Typtheoretisch basierte Theorembeweiser (COQ) (hui) 1.7. Deduktionsorientierte generische Beweiser (qian+bu) am Beispiel von Isabelle 1 8.7. Deduktionsorientierte generische Beweiser (qian+bu) am Beispiel von Isabelle 2 Gruppe III: Systeme und Beweisumgebungen (fuer Studenten) 15.7. Alternativ: LEGO, ELF, Galf, Otter, Boyer-Moore,(??) 22.7. Alternativ: KIV, Larch, (??) 29.7. Ulmer Erweiterungen von LEGO (ECC++) (kol) ????. DEVA (thomas??) PS: (Zur Erinnerung: 8.4. Narrowing Strategies (jun) From bu Thu Apr 7 17:44:53 1994 Date: Thu, 7 Apr 94 17:44:51 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik.uni-Bremen.de., kreyss@informatik.uni-Bremen.de., drewes@informatik.uni-Bremen.de., stefan@stefan.north.de Subject: Verschiebung Content-Length: 179 Status: RO X-Lines: 8 Liebe Leute, der Vortrag von Liu Jun (Narrowing strategies) wird um eine Woche auf den 15.4. verschoben und im Anschluss an die Vorbesprechung des Seminars gehalten. Gruss bu From bu Tue Sep 13 12:20:32 1994 Return-Path: Received: by Informatik.Uni-Bremen.DE (4.1/SMI-4.1) id AA23794; Tue, 13 Sep 94 12:20:21 +0200 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA03252; Tue, 13 Sep 1994 12:18:40 --100 Date: Tue, 13 Sep 1994 12:18:40 --100 From: bu Message-Id: <9409131018.AA03252@phoenix.Informatik.Uni-Bremen.DE> To: bu, shi, qian, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm@lehre, kol, herwig@Informatik.Uni-Bremen.DE, heger@Informatik.Uni-Bremen.DE, andreas@Informatik.Uni-Bremen.DE, roefer@Informatik.Uni-Bremen.DE, michaelh@pc-labor.uni-Bremen.de, holly@pc-labor.uni-bremen.de, svh@pc-labor.uni-bremen.de, blecky@pc-labor.uni-bremen.de, ruqian@Informatik.Uni-Bremen.DE, wang@pc-labor.uni-Bremen.de, cabo@bettina, bohnebec@Informatik.Uni-Bremen.DE, kreyss@Informatik.Uni-Bremen.DE, drewes@Informatik.Uni-Bremen.DE, stefan@stefan.north.de, damm@Informatik.Uni-Oldenburg.de, olderog@Informatik.Uni-Oldenburg.de, Juergen.Bohn@informatik.uni-oldenburg.de Subject: Vortrag 16.9. X-Sun-Charset: US-ASCII Content-Length: 1173 X-Lines: 30 Status: RO Liebe Leute, diesen Freitag, 15 Uhr(ct), wird Dr. Christoph Kreitz vom Fachgebiet Intellektik, TH Darmstadt einen Vortrag halten ueber: "Ein Fundament fuer Verifizierte Softwareentwicklungssysteme Der Vortrag findet im MZH 8090 statt. Zum Inhalt: We describe a formalization of the meta-mathematics of programming in a higher-order calculus as a means to create verifiably correct implementations of program synthesis tools. Formal definitions and lemmata are used to raise the level of abstraction in formal reasoning to one comprehensible for programmers. Formal meta-theorems make explicit the semantic knowledge contained in program derivation methods and serve as kernel of derived inference rules implementing these methods. By an example formalization of a strategy deriving global search algorithms we demonstrate the advantages of combining formal mathematics with an interactive theorem proving environment to develop powerful, flexible, and reliable systems for knowledge-based software development. Alle Interessierten sind Herzlich eingeladen. bu From bu Thu Sep 22 17:58:06 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/20.9.94m) with SMTP from phoenix.informatik.uni-bremen.de [134.102.204.14] id RAA23727 Thu, 22 Sep 1994 17:56:36 +0200 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA02992; Thu, 22 Sep 1994 17:54:43 --100 Date: Thu, 22 Sep 1994 17:54:43 --100 From: bu Message-Id: <9409221554.AA02992@phoenix.Informatik.Uni-Bremen.DE> To: bu, shi, qian, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm, kol, herwig, heger, andreas, roefer, michaelh@pc-labor.uni-Bremen.de, holly@pc-labor.uni-Bremen.de, svh@pc-labor.uni-Bremen.de, blecky@pc-labor.uni-Bremen.de, ruqian, wang@pc-labor.uni-Bremen.de, cabo, bohnebec, kreyss, drewes, stefan@stefan.north.de, damm@informatik.uni-oldenburg.de, olderog@informatik.uni-oldenburg.de, Juergen.Bohn@informatik.uni-oldenburg.de Subject: Promotionsvortrag liu X-Sun-Charset: US-ASCII Content-Length: 743 X-Lines: 27 Status: RO Liebe Leute, am Montag, 26, um 10 c.t. im Raum MZH 8090, findet der Kolloquiumsvortrag von Liu Junbo unter dem Titel: Higher-Order Structured Presentations in a Logical Framework statt. Abstract Type theories like LF (Edinburgh Logical Framework) are used succefully to represent the semantics of programs and specifications. Their extensions, which happened often, are quite difficult. We suggest a new method of the extension by giving a categorical interpretation of type theories with respect to strucutred representations. In doing so, type theories like LF can be extended easily with structured presentations including parameterizations developed logic-independently. Alle Interessierten sind herzlich eingeladen. bu From bu Fri Oct 21 15:34:10 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from phoenix.informatik.uni-bremen.de [134.102.204.14] id PAA03536 Fri, 21 Oct 1994 15:33:59 +0100 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA15088; Fri, 21 Oct 1994 15:32:58 --100 Date: Fri, 21 Oct 1994 15:32:58 --100 From: bu Message-Id: <9410211432.AA15088@phoenix.Informatik.Uni-Bremen.DE> To: bu, shi, qian, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm, kol, herwig, heger, andreas, roefer, michaelh@pc-labor.uni-Bremen.de, holly@pc-labor.uni-Bremen.de, svh@pc-labor.uni-Bremen.de, blecky@pc-labor.uni-Bremen.de, ruqian, wang@pc-labor.uni-Bremen.de, cabo, bohnebec, kreyss, drewes, stefan@stefan.north.de, damm@informatik.uni-oldenburg.de, olderog@informatik.uni-oldenburg.de, Juergen.Bohn@informatik.uni-oldenburg.de, gogolla Subject: Naechstes Treffen X-Sun-Charset: US-ASCII Content-Length: 853 X-Lines: 29 Status: RO Liebe Leute, am naechsten Freitag, am 28.10.04 findet ein 2-stuendiger Vortrag zum Thema: Design and Specification of a Framework for Large Scale System Development in a Pure Functional Setting. von Einar Karlsen statt. Abstract: The development of more complex and integrated systems require a variety of technology: concurrency, distribution, persistency, transactions, dynamic linking and to some extend dynamic typing. We present the design of such a framework in a pure functional setting and demonstrate its application to a single example - the integration of a repository manager with a file store. A semantic definition of the primitive operations for concurrency, distribution and persistency is then given in terms of a labelled transition system. Alle Interessierten sind herzlich eingeladen. From bu Fri Oct 21 16:09:42 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from phoenix.informatik.uni-bremen.de [134.102.204.14] id QAA03687 Fri, 21 Oct 1994 16:02:34 +0100 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA15105; Fri, 21 Oct 1994 16:01:33 --100 Date: Fri, 21 Oct 1994 16:01:33 --100 From: bu Message-Id: <9410211501.AA15105@phoenix.Informatik.Uni-Bremen.DE> To: bu, shi, qian, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm, kol, herwig, heger, andreas, roefer, michaelh@pc-labor.uni-Bremen.de, holly@pc-labor.uni-Bremen.de, svh@pc-labor.uni-Bremen.de, blecky@pc-labor.uni-Bremen.de, ruqian, wang@pc-labor.uni-Bremen.de, cabo, bohnebec, kreyss, drewes, stefan@stefan.north.de, damm@informatik.uni-oldenburg.de, olderog@informatik.uni-oldenburg.de, Juergen.Bohn@informatik.uni-oldenburg.de Subject: Nachtrag X-Sun-Charset: US-ASCII Content-Length: 57 X-Lines: 4 Status: RO Ich vergass, der Vortrag findet punkt 15 Uhr statt. bu From bu Fri Oct 21 16:51:58 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from phoenix.informatik.uni-bremen.de [134.102.204.14] id QAA03885 Fri, 21 Oct 1994 16:51:48 +0100 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA15123; Fri, 21 Oct 1994 16:50:46 --100 Date: Fri, 21 Oct 1994 16:50:46 --100 From: bu Message-Id: <9410211550.AA15123@phoenix.Informatik.Uni-Bremen.DE> To: bu, shi, qian, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm, kol Subject: EXTRA-Krise X-Sun-Charset: US-ASCII Content-Length: 4509 X-Lines: 116 Status: RO Liebe Leute, es scheint mal wieder, das das EXTRA-Treffen in einer schweren Krise ist. Da ich naechste Woche nicht da bin, aber einige Dinge rasch entschieden werden muessen, und da Kolyang als 2. EXTRA-Treffen-Beauftragter im Krankenhaus ist, habe ich beschlossen, meinen Aerger samt den noetigen Informationen so rumzuschicken und Eurer Disdkussion zu ueberlassen. Lt. Protokoll von Bertold von der letzten Gruppenbesprechung wurde beschlossen: >>>>>>>>>>>>>>>>>> Lt. Protokoll von Berthold Die Zukunft des EXTRA-Treffens wird beraten. Soll wieder ein "ubergreifendes Thema gew"ahlt werden? Das hat sich bew"ahrt! Burkhart schl"agt ``Higher Order Logic, Matching and Unification'' vor, ein Thema, auf dem einige von uns arbeiten. Parallel sollen wie bisher Berichte von Tagungen und "uber eigene Arbeiten (oder auch interessante fremde) gehalten werden. Burkhart stellt eine Liste zusammen. <<<<<<<<<<<<<<<<<<< Die Idee setzt voraus, dass einige Leute auch Ueberblicksvortraege zum Thema halten, und nicht nur Spezialvortraege. Das kann durchaus bedeuten, das jemand auch noch mal in ein Lehrbuch guckt und was vorher liest (also: ARBEIT). Man erinnere sich, dass das Seminar vom Anspruch her auch fuer Studenten offen sein sollte. Meine Ausarbeitung fuer den Vorschlag sieht bisher so aus: Higher-Order-Logic als Spezifikationssprache Geschichte, Motivation - Kalkuel im Vergleich zu PL1 - Beispiel - Semantik - Einige Resultate: Loewenheim-Skolem, Unifikation, Resolution, Unvollstaendigkeitssatz Spezielle automatische Deduktionsaspekte: - HO Unifikation - HO Matching - HO Narrowing - HO Unifikation modulo E Datentyp-und Theoriekonstruktionen in HOL - Das Problem der Konsistenz & Konservative Erweiterungen vs. "Refinement-Methoden" - Mengen, Produkte, Summen, Fixpunkte - Data-types, Inductive Sets - Subtyp-Abstraktionen ... - "Ausfuehrbare Spezifikationen" Beweistechnik ? - Beispielbeweis, - Induktionsnachweis - Korrektheitsbeweise von "Synthesetheoremen" - Diskussion Fallstudie: Verifikation in SPECTRUM? Sabine Dick. Junbo Liu: Martin-Loef - Construktive Typ-theorie??? Dies ist als Gerust fuer einige Spezialvortraege (Etwa: E-Matching, oder: Fallstudie: Verifikation in SPECTRUM (Sabine Dick)) gedacht, die sich geeignet dazwischenmischen. Es stellte sich heraus, dass sich (ausser mir und ev. Thomas) niemand bereit erklaerte, zu irgendeinem Thema oder einer Variation davon einen Vortrag zu halten. Qian erklaerte sich fuer ausserstande, in das Gebiet HO-Unifikation einzufuehren (dito Hui), und immer wieder hoerte ich, dass ein Einfuehrungsvortrag ja soo viel Arbeit mache. Sonstige Themen, die angeboten wurden: Hui E-Matching Berthold ?!?! liu Jun ??? Qian Objektorientierte Programmiersprachen Sather Bernd Monaden in HO-Spezifikationssprachen Kolyang ??? Einar Design and Specification of a Framework for Large Scale System Development in a Pure Functional Setting. (Wie angekuendigt). Michael Graph-Drawing 94 bu FME 94 wolfgang grieskamp traegt anfang oktober vor (sagt einar) Ich frage mich, warum in unserem "Organisationstreffen" Dinge beschlossen werden, fuer die das Interesse einerseits und/oder das Engagement zur Durchfuehrung andererseits dermassen gering ist. Soweit, so schlecht. Ganz besonders deprimierend fand ich aber folgendes: bkb hatte im Vorlesungsverzeichnis sich selbst als Veranstalter fuer eine Veranstaltung "Semantik von Spezifikation- und Programmiersprachen", scheinbar ohne eine DURCHFUEHRUNG des Seminars unter diesem Titel ernsthaft ins Auge zu fassen. Unter diesem Titel, unter dem ich als Student eine Einfuehrung in "operationale, denotationelle, axiomatische und Action-Semantik" verstehen wuerde, fanden sich immerhin etwa 10 Studenten ein, die ich (bkb hatte mich 3 Std. zuvor angerufen) heftig darueber beschwerten, dass die Verschiebung nicht schon seit Tagen auf einem Aushang bekannt gegeben worden war. (Ich hab sie auf 2 Wochen vertroestet). Die Weigerung der Gruppenmitglieder, am EXTRA-Treffen im Sinne eines weiterbildenden Seminars fuer uns Doktoranden mitzuwirken, wirkt in diesem Lichte nun wieder verstaendlich - denn niemand von den Doktoranden versteht sich gern als Ersatz-Lehrveranstalter fuer eine an Studenten im Hauptstudium gerichtete Lehrveranstaltung. Vielleicht faellt Euch ja noch was dazu ein. bu From bernd Fri Oct 21 16:58:03 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from pavo.informatik.uni-bremen.de [134.102.204.23] id QAA03907 for Fri, 21 Oct 1994 16:57:50 +0100 Received: by pavo.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA20841; Fri, 21 Oct 1994 16:56:46 --100 Date: Fri, 21 Oct 1994 16:56:46 --100 From: bernd Message-Id: <9410211556.AA20841@pavo.Informatik.Uni-Bremen.DE> To: bu Subject: Re: EXTRA-Krise X-Sun-Charset: US-ASCII Content-Length: 30 X-Lines: 5 Status: RO Z.B. beim Schwimmen? Bernd From qian Fri Oct 21 17:21:24 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from polaris.informatik.uni-bremen.de [134.102.204.20] id RAA03998 Fri, 21 Oct 1994 17:21:19 +0100 Received: by polaris.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA15587; Fri, 21 Oct 1994 17:21:38 --100 Date: Fri, 21 Oct 1994 17:21:38 --100 From: qian Message-Id: <9410211621.AA15587@polaris.Informatik.Uni-Bremen.DE> To: bu, shi, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm, kol Subject: Re: EXTRA-Krise Cc: qian X-Sun-Charset: US-ASCII Content-Length: 2179 X-Lines: 48 Status: RO > Higher-Order-Logic als Spezifikationssprache > > Geschichte, Motivation > - Kalkuel im Vergleich zu PL1 > - Beispiel > - Semantik > - Einige Resultate: Loewenheim-Skolem, Unifikation, Resolution, > Unvollstaendigkeitssatz > > > Es stellte sich heraus, dass sich (ausser mir und ev. Thomas) niemand bereit > erklaerte, zu irgendeinem Thema oder einer Variation davon einen Vortrag zu > halten. Qian erklaerte sich fuer ausserstande, in das Gebiet HO-Unifikation > einzufuehren (dito Hui), und immer wieder hoerte ich, dass ein > Einfuehrungsvortrag ja soo viel Arbeit mache. > Ich habe nur gesagt, dass ich keinen Vortrag ueber allgemeine HO-Logik und HO- Resolution halten kann. Das ist ein bisschen anders als einen Vortrag ueber HO-Unifikation. > Ich frage mich, warum in unserem "Organisationstreffen" Dinge beschlossen > werden, fuer die das Interesse einerseits und/oder das Engagement zur > Durchfuehrung andererseits dermassen gering ist. Soweit, so schlecht. Wenn man woertlich vom Protokol nimmt, haben wir NICHT BESCHLOSSEN, ``Higher Order Logic, Matching and Unification'' als ein "ubergreifendes Thema zu machen, sondern Bu dies VORGESCHLAGEN hat. Das ist ein Unterschied, oder? > Die Weigerung der Gruppenmitglieder, am EXTRA-Treffen im Sinne eines > weiterbildenden Seminars fuer uns Doktoranden mitzuwirken, wirkt in diesem > Lichte nun wieder verstaendlich - denn niemand von den Doktoranden versteht > sich gern als Ersatz-Lehrveranstalter fuer eine an Studenten im Hauptstudium > gerichtete Lehrveranstaltung. Ich habe nicht geweigert EINEN Vortrag zu halten, sondern ich kann NICHT DEN Vortrag halten. Das ist auch ein Unterschied, oder? Ein Thema kann als ein "ubergreifendes Thema nur dann gemacht werden, wenn manche Leute bereit erklaert haben, die EinfUehrungsvortraege zu halten. Deshalb die logische Folgerung: ``Higher Order Logic, Matching and Unification'' kann jetzt noch nicht zu einem "ubergreifendes Thema gemacht werden. Sonst finde ich sehr nett, dass Bu sich darum kuemert. Wir muessen doch dabei helfen. Nur ueber das Thema soll man sich noch Gedanken darueber machen. Gruss Qian From bu Fri Oct 21 19:47:11 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from phoenix.informatik.uni-bremen.de [134.102.204.14] id TAA04622 Fri, 21 Oct 1994 19:47:06 +0100 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA15176; Fri, 21 Oct 1994 19:46:04 --100 Date: Fri, 21 Oct 1994 19:46:04 --100 From: bu Message-Id: <9410211846.AA15176@phoenix.Informatik.Uni-Bremen.DE> To: qian, bu, shi, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm, kol Subject: Re: EXTRA-Krise X-Sun-Charset: US-ASCII Content-Length: 1303 X-Lines: 33 Status: RO >>Ich habe nur gesagt, dass ich keinen Vortrag ueber allgemeine HO-Logik und HO- >>Resolution halten kann. Oh, sollte es da ein Missverstaendnis gegeben haben? Ich hatte das Geruest in drei Bloecke gegliedert, die jeweils einen Einfuehrungsvortrag darstellen. Ich hatte dabei nicht angenommen, dass Du allgemein etwas ueber HO-Logik sagen wuerdest, sondern den Vortrag: > Spezielle automatische Deduktionsaspekte: > - HO Unifikation > - HO Matching > - HO Narrowing > - HO Unifikation modulo E Dir thematisch so auf den Leib geschneidert ist, dass ich mir kaum auch nur den Schatten einer Verwechslungsgefahr vorstellen konnte. >Ein Thema kann als ein "ubergreifendes Thema nur dann gemacht werden, >wenn manche Leute bereit erklaert haben, die Einfuehrungsvortraege zu halten. >Deshalb die logische Folgerung: ``Higher Order Logic, Matching and Unification'' >kann jetzt noch nicht zu einem "ubergreifendes Thema gemacht werden. Wahr, wahr. Aber falls es ueber diese Absichtserklaerung hinaus irgend einen konkreten Vorschlag gegeben haben sollte, habe ich den wohl ueberhoert. Aus der bisherigen Liste kann ich bestenfalls die Tendenz zur Zersplitterung erkennen. >>Sonst finde ich sehr nett, dass Bu sich darum kuemert ... Ich finde dich auch sehr nett, Qian. bu From qian Mon Oct 24 09:14:29 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from polaris.informatik.uni-bremen.de [134.102.204.20] id JAA12523 for Mon, 24 Oct 1994 09:14:28 +0100 Received: by polaris.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA16860; Mon, 24 Oct 1994 09:14:47 --100 Date: Mon, 24 Oct 1994 09:14:47 --100 From: qian Message-Id: <9410240814.AA16860@polaris.Informatik.Uni-Bremen.DE> To: bu Subject: Re: EXTRA-Krise X-Sun-Charset: US-ASCII Content-Length: 496 X-Lines: 16 Status: RO > Oh, sollte es da ein Missverstaendnis gegeben haben? > > Ich hatte das Geruest in drei Bloecke gegliedert, die jeweils einen Einfuehrungsvortrag darstellen. Ich hatte dabei nicht angenommen, dass Du allgemein etwas ueber HO-Logik sagen wuerdest, sondern den Vortrag: > > > > Spezielle automatische Deduktionsaspekte: > > - HO Unifikation > > - HO Matching > > - HO Narrowing > > - HO Unifikation modulo E > Das ist was anderes. Das kann ich natuerlich machen. Gruss Qian From ewk Mon Oct 24 14:12:09 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from lynx.informatik.uni-bremen.de [134.102.204.22] id OAA15342 Mon, 24 Oct 1994 14:12:08 +0100 Received: by lynx.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA17676; Mon, 24 Oct 1994 14:12:09 --100 Date: Mon, 24 Oct 1994 14:12:09 --100 From: ewk Message-Id: <9410241312.AA17676@lynx.Informatik.Uni-Bremen.DE> To: bu Subject: Talk by Wolfgang Cc: ewk X-Sun-Charset: US-ASCII Content-Length: 207 X-Lines: 9 Status: O Burkhart, I have got a mail from Wolfgang saying that his visit here in Bremen will be app 1 month delayed (he is actually here on private purpose, and is kind to pop by and give the talk). Cheers, Einar From bu Tue Nov 1 15:28:21 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from phoenix.informatik.uni-bremen.de [134.102.204.14] id PAA17523 Tue, 1 Nov 1994 15:21:27 +0100 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA00975; Tue, 1 Nov 1994 15:20:15 --100 Date: Tue, 1 Nov 1994 15:20:15 --100 From: bu Message-Id: <9411011420.AA00975@phoenix.Informatik.Uni-Bremen.DE> To: bu, shi, qian, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm, kol, herwig, heger, andreas, roefer, michaelh@pc-labor.uni-Bremen.de, holly@pc-labor.uni-Bremen.de, svh@pc-labor.uni-Bremen.de, blecky@pc-labor.uni-Bremen.de, ruqian, wang@pc-labor.uni-Bremen.de, cabo, bohnebec, kreyss, drewes, stefan@stefan.north.de, damm@informatik.uni-oldenburg.de, olderog@informatik.uni-oldenburg.de, Juergen.Bohn@informatik.uni-oldenburg.de Subject: EXTRA-Treffen X-Sun-Charset: US-ASCII Content-Length: 477 X-Lines: 14 Status: RO Liebe Leute, diesen Freitag, den 7.11., gegen 15 Uhr 30 (nach einer Organisationsbesprechung mit Studenten) werde ich ueber die FME 94 : Industrial Benefits of Formal Methods vortragen. Die Tagung bestand aus Tutorials ueber VDM, RAISE und CSP, aus einer Schiene "Systemvorfuehrungen", aus Berichten von Praktikern in der Industrie und aus Vortraegen ueber (oft eher theoretische) Beitraege. Ich werde mich in meinem Vortrag auf die letzten 3 Aspekte konzentrieren. bu From bernd Tue Nov 1 15:47:23 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from pavo.informatik.uni-bremen.de [134.102.204.23] id PAA17761 for Tue, 1 Nov 1994 15:47:21 +0100 Received: by pavo.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA02733; Tue, 1 Nov 1994 15:46:04 --100 Date: Tue, 1 Nov 1994 15:46:04 --100 From: bernd Message-Id: <9411011446.AA02733@pavo.Informatik.Uni-Bremen.DE> To: bu Subject: Re: EXTRA-Treffen X-Sun-Charset: US-ASCII Content-Length: 77 X-Lines: 4 Status: RO ...ach ja. Einars Vortrag wurde von BKB verschoben (um eine Woche?) Bernd From tm Tue Nov 1 16:18:43 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from [134.102.204.26] id QAA18003 for Tue, 1 Nov 1994 16:18:42 +0100 Received: by taurus.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA01499; Tue, 1 Nov 1994 16:18:42 --100 Date: Tue, 1 Nov 1994 16:18:42 --100 From: tm Message-Id: <9411011518.AA01499@taurus.Informatik.Uni-Bremen.DE> To: bu Subject: Re: EXTRA-Treffen X-Sun-Charset: US-ASCII Content-Length: 69 X-Lines: 4 Status: RO Du hast Dich im Datum versehen. Freitag ist der 4.11. Gruss Thomas From bu Tue Nov 1 17:13:31 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from phoenix.informatik.uni-bremen.de [134.102.204.14] id RAA18428 Tue, 1 Nov 1994 17:13:30 +0100 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA01021; Tue, 1 Nov 1994 17:12:15 --100 Date: Tue, 1 Nov 1994 17:12:15 --100 From: bu Message-Id: <9411011612.AA01021@phoenix.Informatik.Uni-Bremen.DE> To: liu, kol, shi Subject: EXTRA-Planung Cc: bu X-Sun-Charset: US-ASCII Content-Length: 2826 X-Lines: 133 Status: RO Bisheriger Diskussionsstand Habt Ihr noch Ideen fuer 3. und 4. ??? Ich habe mit den betreffenden noch nicht gesprochen - die Vorschlaege sind vielleicht noch n bisschen abstrus und unpraezis... Tendentiell ist Punkt 1.3 n bisschen fett und koennte weiter aufgeteilt werden... bu >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 1)Higher-Order-Logic als Spezifikationssprache X Geschichte, Motivation - Kalkuel im Vergleich zu PL1 - Beispiel - Semantik - Einige Resultate: Loewenheim-Skolem, Unifikation, Resolution, Unvollstaendigkeitssatz - Systeme (kolyang?, bu) X Spezielle automatische Deduktionsaspekte: - HO Unifikation - HO Matching - HO Narrowing - HO Unifikation modulo E ( Ev. zwei Vortraege? qian, (jun, hui ???)) X Datentyp-und Theoriekonstruktionen in HOL - Das Problem der Konsistenz & Konservative Erweiterungen vs. "Refinement-Methoden" - Mengen, Produkte, Summen, Fixpunkte - Data-types, Inductive Sets - Subtyp-Abstraktionen ... - Implementierung via Abtraktionsmorphismus - "Ausfuehrbare Spezifikationen" (thomas, kolyang ???) 2)Anwendungen: X Beweistechnik - Beispielbeweis, - Induktionsnachweis - Korrektheitsbeweise von Programmtransformationen - Diskussion (liu & bu) X HOL als Meta-Sprache (I): Encoding von CSP (hui) - Zustaende, - Prozesse, - Beweisprinzipien X HOL als Meta-Sprache (II): CTT in Isabelle (Liu) - Typen, Typen Typen X Fallstudien: Mikroprozessor-Verifikation, Prozess-Protokolle & & & (Bernd ???) X ??? Fallstudie: Verifikation in SPECTRUM? (Sabine Dick). - Formale Programmentwicklung eines Gepaeck-Schedulers - nach Doug Smith 3)Vortraege fuer Studenten (Ueber Programmiersprachen-Semantik allgemein): Operational: Hennessy : The Semantics of Programming Languages Plotkin : Structural Operational Semantics (Mosses : Action Semantics ( Really ??? )) Denotationell: Harrison Field: Denotational Semantics Schmidt : Denotational Semantics Stoy : ??? Axiomatisch: Loechx/Sieber : Foundations of Prog/Verification (Irgend jemand sollte was ueber die Axiomatische Methode erzaehlen) Algebraisch: ??? (kleine herausforderung) Spec-Sprachen: VDM, Z, B , RC, RAISE 4)Vorschlaege fuer noch nicht Beruecksichtigte: Berthold: "Formalisierung einer Graph-Theorie in HOL" (Nach Simon) Mawe, Mfr: Spezifikationen von GUI's ??? Bernd: ?????? (Irgendwas mit Zustandsorientierter Spezifikation, Prozess-specs wie Unity?, Subtyping a la IMPS? Kolyang ????? Was mit SPECTRUM? Was Grundlegenderes? Vielleicht einen Teil der Einleitung? Einar ????? Jun ????? From bu Thu Nov 3 16:17:07 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from phoenix.informatik.uni-bremen.de [134.102.204.14] id QAA02232 Thu, 3 Nov 1994 16:16:59 +0100 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA01968; Thu, 3 Nov 1994 16:15:45 --100 Date: Thu, 3 Nov 1994 16:15:45 --100 From: bu Message-Id: <9411031515.AA01968@phoenix.Informatik.Uni-Bremen.DE> To: bu, shi, qian, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm, kol Subject: EXTRA-Planung X-Sun-Charset: US-ASCII Content-Length: 3951 X-Lines: 156 Status: RO Liebe Leute, anbei die Vorschlagsliste mit Vortraegen im "Rahmenprogramm". Das Extra-Treffen wird zeitgleich mit dem studentischen Seminar "Semantik von Spezifikations-und Programmiersprachen" stattfinden, zu dem beim letzten Mal (zur Erinnerung) immerhin SIEBEN bis ZEHN Studenten gekommen waren - es koennte also sein, dass hierfuer erheblich Zeit allokiert werden muss: In der nachfolgenden Liste sind Literaturvorschlaege fuer "Studentische Seminarbeitraege" zum versprochenen Seminarthema, die man ihnen fuer einen ev. Seminarschein vorschlagen koennte. Da das im Moment nicht abzuschaetzen ist, habe ich auf eine genaue zeitliche Festsetzung der Vortraege verzichtet, dies wird evtl. "on the fly" entschieden. Wohin Einars Vortrag verschoben werden soll, der zu meiner Ueberaschung ausgefallen ist, ist mir auch nicht klar. Fuer weitere Vorschlaege, sei es fuer Abaenderungen und weitere Vortraege in und ausserhalb des Rahmenprogramms bin ich offen. bu PS: Ich gehe davon aus, dass sich jeder einen Ausdruck von diesem Papier mitbringt, damit wir es gemeinsam im Anschluss an daws morgige EXTRA-Treffen diskutieren koennen. >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Tendentiell ist Punkt 1.3 n bisschen fett und koennte weiter aufgeteilt werden... bu >>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> 1)Higher-Order-Logic als Spezifikationssprache X Geschichte, Motivation - Kalkuel im Vergleich zu PL1 - Beispiel - Semantik - Einige Resultate: Loewenheim-Skolem, Unifikation, Resolution, Unvollstaendigkeitssatz - Systeme (kolyang, bu) X Spezielle automatische Deduktionsaspekte: - HO Unifikation - HO Matching - HO Narrowing - HO Unifikation modulo E ( Ev. zwei Vortraege? qian, (jun, hui ???)) X Datentyp-und Theoriekonstruktionen in HOL - Das Problem der Konsistenz & Konservative Erweiterungen vs. "Refinement-Methoden" - Mengen, Produkte, Summen, Fixpunkte - Data-types, Inductive Sets - Subtyp-Abstraktionen ... - Implementierung via Abtraktionsmorphismus - "Ausfuehrbare Spezifikationen" (thomas, kolyang?) 2)Anwendungen: X Beweistechnik - Beispielbeweis, - Induktionsnachweis - Korrektheitsbeweise von Programmtransformationen - Diskussion (liu & bu) X HOL als Meta-Sprache (I): Encoding von CSP (hui) - Zustaende, - Prozesse, - Beweisprinzipien X HOL als Meta-Sprache (II): CTT in Isabelle (Liu) - Typen, Typen Typen X Fallstudien: Mikroprozessor-Verifikation, Prozess-Protokolle & & & (Bernd ???) X ??? Fallstudie: Verifikation in SPECTRUM? (Sabine Dick). - Formale Programmentwicklung eines Gepaeck-Schedulers - nach Doug Smith 3)Vortraege fuer Studenten (Ueber Programmiersprachen-Semantik allgemein): Operational: Hennessy : The Semantics of Programming Languages Plotkin : Structural Operational Semantics Kahn : Natural Semantics (Mosses : Action Semantics ( Really ??? )) Denotationell: Harrison Field: Functional Programming (Denotational Semantics) Schmidt : Denotational Semantics Stoy : ??? Fehr : Semantik von Programmiersprachen Loeckx/Sieber : Foundation of Programm Verification Axiomatisch: Loechx/Sieber : Foundations of Prog/Verification (Irgend jemand sollte was ueber die Axiomatische Methode erzaehlen) Algebraisch: Ehrig/Mahr : Fundamentals of AlgSprec Gogolla/Lippeck: Algebraische Spezifikation Spec-Sprachen: VDM, Z, B , Refine Calculus, RAISE, HOL 4)Vorschlaege fuer noch nicht Beruecksichtigte: Berthold: "Formalisierung einer Graph-Theorie in HOL" (Nach Simon) Mawe, Mfr: Spezifikationen von GUI's ??? Bernd: ?????? (Irgendwas mit Zustandsorientierter Spezifikation, Prozess-specs wie Unity?, Subtyping a la IMPS? Einar ????? Jun ????? From qian Thu Nov 3 16:30:55 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from polaris.informatik.uni-bremen.de [134.102.204.20] id QAA02582 for Thu, 3 Nov 1994 16:30:54 +0100 Received: by polaris.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA04328; Thu, 3 Nov 1994 16:31:14 --100 Date: Thu, 3 Nov 1994 16:31:14 --100 From: qian Message-Id: <9411031531.AA04328@polaris.Informatik.Uni-Bremen.DE> To: bu Subject: EXTRA Treffen X-Sun-Charset: US-ASCII Content-Length: 191 X-Lines: 8 Status: RO Es gibt einen Vorschlag dass ich ueber OO Konzepte in Sather erz"ahle. Ausserdem schlage ich vor, dass Kolyang die OO Konzepte in Oz erz"ahlt (Er ist auch bereit das zu tun). Gruss Qian From bu Thu Nov 10 17:14:49 1994 Received: by bettina.informatik.uni-Bremen.de (8.6.9/3.10.94m) with SMTP from phoenix.informatik.uni-bremen.de [134.102.204.14] id RAA16358 Thu, 10 Nov 1994 17:12:09 +0100 Received: by phoenix.Informatik.Uni-Bremen.DE (5.0/SMI-SVR4) id AA06653; Thu, 10 Nov 1994 17:10:45 --100 Date: Thu, 10 Nov 1994 17:10:45 --100 From: bu Message-Id: <9411101610.AA06653@phoenix.Informatik.Uni-Bremen.DE> To: bu, shi, qian, wu, liu, bernd, bkb, hof, ewk, mfr, mawe, jun, tm, kol, herwig, heger, andreas, roefer, michaelh@pc-labor.uni-Bremen.de, holly@pc-labor.uni-Bremen.de, svh@pc-labor.uni-Bremen.de, blecky@pc-labor.uni-Bremen.de, ruqian, wang@pc-labor.uni-Bremen.de, cabo, bohnebec, kreyss, drewes, stefan@stefan.north.de, damm@informatik.uni-oldenburg.de, olderog@informatik.uni-oldenburg.de, Juergen.Bohn@informatik.uni-oldenburg.de, jk@zarniwoop.pc-labor.uni-bremen.de Subject: Naechste Meetings X-Sun-Charset: US-ASCII Content-Length: 1381 X-Lines: 49 Status: RO Liebe Leute, der urspruenglich fuer diesen Freitag vorgesehene Vortrag von Einar Karlsen "Design and Specification of a Framework for Large Scale System Development in a Pure Functional Setting" Ist auf Dienstag Nachmittag 15 Uhr verschoben worden. Abstract: The development of more complex and integrated systems require a variety of technology: concurrency, distribution, persistency, transactions, dynamic linking and to some extend dynamic typing. We present the design of such a framework in a pure functional setting and demonstrate its application to a single example - the integration of a repository manager with a file store. A semantic definition of the primitive operations for concurrency, distribution and persistency is then given in terms of a labelled transition system. Am darauffolgenden Freitag, den 18.11. faellts aus. Am darauffolgenden Freitag, den 25.11. findet dann der erste Vortrag aus unserer Reihe "Higher-Order-Logic als Spezifikationssprache" statt. Vortragende: kol & bu Thema: "Einfuehrung in Higher Order Logic" Inhaltsuebersicht: - Motivation, Geschichte - Kalkuel im Vergleich zu PL1 - Beispiel - Semantik - Einige Resultate: Loewenheim-Skolem, Unifikation, Resolution, Unvollstaendigkeitssatz - Systeme Alle Interessierten sind herzlich eingeladen. bu From bu Wed Oct 7 15:11:44 1992 Date: Wed, 7 Oct 92 15:11:39 +0100 From: bu (Burkhart Wolff) To: bernd, bkb, det, ejs, ewk, hof, jvh, liu, mawe, mfr, qian, ric, shi, wang@pc-labor.uni-Bremen.de Subject: next EXTRA-talks Cc: bu Status: RO Content-Length: 657 X-Lines: 34 Dear Extrafans, the following talks will be given in the next time: 1) 9.10. 15.00 Bu: Report from the STOP-Summerschool on Ameland. New Squiggols, Relational Calculi and Monads. 2) 16.10. 14.00-15.00 Richard: Termination-Proofs for TRS. Integration of RPO's and pol. Interpretations. 3) 16.10. 15.00-16.00 Liu: Timed Process Algebras. 4) 23.10. 15.00 Guest Liu Zhiming (Warwick): Fault Tolerance in tranformational developments 30.10. No meeting because of COMPASS. 5) 6.11. 15.00 Joern: Monads and Inheritance: Differences. 6) 13.11. 15.00 Liu: Refinement Calculus in HOL. So far for the moment, bu From bu Wed May 12 19:54:37 1993 Date: Wed, 12 May 93 19:54:35 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, tm@p111, jvh, ric, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de Subject: Naechstes Extratreffen Content-Length: 285 Status: RO X-Lines: 14 Liebe Leute, nach langer Pause ist wieder ein Extratreffen anzukuendigen: Fr. 14.5 15.00 B. Gersdorff: Praktische Erfahrungen mit den Sprachen ASPECT und OPAL Weitere Vortraege sind in Vorbereitung (von Kolyang und von mir selbst) und werden bald nachgereicht. Gruss bu From bu Thu May 20 16:41:29 1993 Date: Thu, 20 May 93 16:41:27 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, tm@p111, jvh, ric, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de Subject: naechstes Extratreffen Content-Length: 144 Status: O X-Lines: 10 Liebe Leute, morgen um 15 Uhr wird Kolyang ueber seine Diplomarbeit berichten. Thema: Typinferenz fuer Subtypen und Polymorphie. Gruss bu From bu Mon Jun 14 11:57:54 1993 Date: Mon, 14 Jun 93 11:57:51 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, tm@p111, jvh, ric, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de Subject: protokoll 11.6.93 Content-Type: X-sun-attachment Status: RO X-Lines: 117 Content-Length: 5611 ---------- X-Sun-Data-Type: text X-Sun-Data-Description: text X-Sun-Data-Name: text X-Sun-Content-Lines: 0 X-Sun-Content-Length: 0 ---------- X-Sun-Data-Type: default X-Sun-Data-Name: Protokoll.Extra X-Sun-Content-Lines: 106 X-Sun-Content-Length: 5357 Protokoll vom Extra-Treffen 11.6.93 Thema: Sinn, Probleme und Verbesserung des Extra-treffens Protokollant: bu Kritik(bu): Es scheint eine Art Sinnkrise des Extratreffens zu geben. Die Motivation, einen Vortrag zu halten, ist kleiner und kleiner geworden; den "Profis" in unserer Gruppe ist das Treffen womoeglich nicht wissenschaftlich genug, den anderen sind die Themen zu speziell und zuweit hergeholt. Als Folge bin ich mehrfach hinter Vortragenden lange hergerannt, wobei der Vortrag dann letztlich doch nicht zustande kam. Dies ist natuerlich auch eine Folge der Groesse unserer Gruppe; hierbei wird es immer schwieriger, ueber die Arbeiten und Interessen der Einzelnen einen Ueberblick zu behalten. Ausserdem ist die Teilnahmedisziplin und Puenktlichkeit bisher nicht gerade hervorragend gewesen. Kritik(hui&kol): Die Motivation, einen Vortrag zu halten, ist nicht gut, wenn alle nach und nach `raus gehen und zum Schluss nur die 4 ueberbleiben, mit denen man sowieso immer ueber das Thema diskutiert. Es fehlt sowas wie ein zentrales Forum unserer Gruppe. Im Laufe der Diskussion (Einige ging schon nach 10 Minuten) wurden folgende Konsequenzen gezogen: 1). Funktion des Extra-Treffens wird entzerrt. a) Es wird der organisatorische Teil (Besprechungen, Institusinterna, Personalia etc) abgetrennt. Der findet jetzt Mittwoch 2 Uhr regelmaessig statt. Organisator ist Bert. An den sind auch Tagungspunkte einzureichen. b) Weiterhin soll eine informelle Teestunde (Anwesenheit fakultativ) eingerichtet werden, das einfach dem allgemeinen Kloenen dienen soll. Der Zeitraum fuer die Teerunde ist 1 - 1Uhr 30. Treffpunkt ist der Besprechungsraum ... Der Raum ist fuer diesen Zeitraum von Lehrveranstaltungen und sonstigem grundsaetzlich freizuhalten. c) Darueberhinaus findet das Extratreffen weiterhin im Regelfall um 15 Uhr 15 bis 16 Uhr 45 statt. Das Extratreffen IST das Doktorandenseminar unserer Gruppe und hat den formalen Titel: "Formale Methoden der Softwaretechnik". Organisatoren sind bu und kolyang. Alle Mitglieder unserer Gruppe sind grundsaetzlich moralisch verpflichtet, daran teilzunehmen. Ausserdem sollte jeder regelmaessig Vortraege halten. (Ueber Ausnahmen und moegliche Formen der Vortraege siehe Punkt 3). 2.) Verbesserung der Planung und der Information. Fuer die Gruppenkoordination werden Ausgangsbretter eingerichtet. Diese werden von den jeweiligen Koordinatoren verwaltet. Darueberhinaus gibt es im Sekretariat ein Brett wo die Urlaubs - und Tagungsaufenthalte kuenftig eingetragen werden sollen, um die Planung des Extra-Treffens zu erleichtern und um es der kuenftigen Sekretaerin zu erleichtern, auf fernmuendliche Anfragen reagieren zu koennen. 3.) Durchfuehrung der Extra-Treffen Vortraege richten sich (vom Ton, vom Niveau) grundsaetzlich an die Fachoeffentlichkeit unserer Gruppe. (Ausnahmen siehe Unten). Sie sollten mit einer hinreichend allgemeinen Einleitung und Motivation beginnen. Es wird davon ausgegangen, das jeder Grundsaetzlich auch entsprechende Zeit fuer die Vorbereitung des Vortrages aufbringt. Zwischenfragen sind nach wie vor erwuenscht. Um sich ergebende Zwischen-Diskussionen kuenftig staerker zu strukturieren (=abzuwuergen), wird die Institution eines "Chairmans" eingesetzt. (bkb oder bu); falls die selbst zusehr beteiligt sind und in dieser Funktion voruebergehend ausfallen, sollen andere eingreifen). Der chairman sorgt auch dafuer, das der offizielle Teil des Treffens kuenftig auf 16.45 begrenzt wird. Schon bisher hatte das Treffen den Charakter eines Informations-, und Diskussions-Forums sowie auch als Moeglichkeit zum Vortrags-Trainings (fuer Vortraege nach aussen). Es folgt eine Uebersicht ueber den moeglichen Charakter von Vortraegen: A) Berichte von Tagungen (wie bisher Pflicht.) B) Technischer Forschungsvortrag. (Auch Vortrag ueber andere Arbeiten, die man gelesen hat oder aehnliches; Wendet sich am ehesten an eine Teilgruppe; ) C) Probevortrag, Externvortrag (kuenftig Pflicht). Wer immer draussen einen Vortrag haelt, soll es auch drinnen tun. Das Ganze hat auch die Funktion eines Vortrags-Trainings. (Hierbei sind u.U. eher die Hoerer gefordert, wenn sich der Vortrag an ein externes Fachpublikum wendet...) D) Diskussion Eine strittige weltanschauliche Frage wird aufs Tapet gebracht. Oder eine noch unausgegorene fachliche Idee ... E) Werkvortrag Ueberblick ueber den Stand laufender oder abgeschlossener Arbeiten (z.B. auch Diplomarbeiten, technische Berichte). F) Diskussion ueber Lehrveranstaltungskonzeptionen (Berthold z.B. hat eine neue Lehrveranstaltung geplant und moechte die Konzeption zur Diskussion stellen) G) Tutorien (Elemente von Vortragsreihen). Diese (neue) Form sieht vor, das einer oder mehrere eine Folge von aufeinander aufbauenden Vortraegen halten, um so vielleicht etwas tiefer in ein gewisses Gebiet einzufuehren. Vortraege sollten kuenftig etwas besser beim Koordinator angemeldet werden. Ich haette gern eine mail, wo Titel, ein mini-abstract und eine Klassifikation (im Sinne der obigen Liste z.B.) drinsteht, damit die Hoerer sich kuenftig besser darauf einstellen koennen, was in dem Vortrag passieren soll. Ev. Dokumente (Fotokopien von Folien, handouts, ...) von Vortragen werden weiterhin von bu gesammelt. bu From bu Mon Jun 14 16:22:24 1993 Date: Mon, 14 Jun 93 16:22:21 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, tm@p111, jvh, ric, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, det, kreo@informatik, drewes@informatik Subject: extratreffen Content-Length: 1177 Status: RO X-Lines: 39 Liebe Leute, fuer den folgenden Freitag habe ich gleich eine ganze Reihe von Vortraegen anzukuendigen: 1.) 10 Uhr: A. Borzyskowski: Verifying parametric algebras against parametric specifications. (Forschungsvortrag; Eigentliches Extra-Treffen) "In my talk I will recall that alg. specifications can be considered as Sigma-types while algebras as their elements; Iwill argue in favor of treating parametric specifications as function types including higher or der functions too; I will present a set of rules together defining a judgement 'an algebra satisfies a specification' ". 2.) 13 Uhr: F. Cornelius: "Semantisches Ausbaustufenkonzept, HDMS-A, und div. Themen" (Offene Diskussion, und, lt. Author, "Eigenwerbung"; richtet sich an unsere und Kreos Gruppe) "Semantisches Ausbaustufenkonzept fuer alg. Spezifikationssprachen, orientiert an SPECTRUM. Ausserdem Bericht ueber die Aktivitaeten im Rahmen vom KORSO-Subprojekt: HDMS-A." 3.) 15 Uhr 15: B Borzyskowski: (Offene Diskussion) Alle drei Termine sollen im Besprechungsraum stattfinden. Verlegungen werden bei uns an der Tafel angeschrieben. bu From bu Tue Jun 22 19:15:35 1993 Date: Tue, 22 Jun 93 19:15:33 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, tm@p111, jvh, ric, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de Subject: naechstes Extra-Treffen Content-Length: 923 Status: RO X-Lines: 34 Liebe Leute, das naechste Extra-Treffen findet ausnahmsweise morgen, Mittwoch, 15 ct statt. Joern v. holten wird ueber seine Dissertation vortragen: (Objekt-orientiert + Funktional == OF) == DISSERTATION Ein Extra-Vortrag mit Extra-Diskussion "Es geht um die im Titel genannte Gleichung, wobei nur der in Klammern gesetzte Ausdruck wirklich zur Diskussion steht. OF ist dabei die Sprache, die ich mir waehrend meiner Arbeit ausgedacht habe. Sie ist NICHT kompatibel zu ASpecT und enthaelt Konzepte, die Euch wahrscheinlich zu denken geben werden. Na denn bis denn... Joern" Die naechsten Wochen werden einige Leute im Urlaub sein. Insbesondere bkb. Das koennte man ja auch nutzen fuer Diskussionen, bei denen es etwas techinscher zugeht. Eine Idee waere eine Diskussion um Funktoren und Klassen-Typsysteme, oder um einen Schnellhack fuer ein Trafo-System. Wenn ihr Vorschlaege habt, bitte an mich. bu From bu Thu Jul 1 14:00:03 1993 Date: Thu, 1 Jul 93 14:00:01 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, tm@p111, jvh, ric, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de Subject: extratreffen morgen Content-Length: 576 X-Lines: 18 Status: RO Liebe Leute, an diesem freitag um 15.00 wird Kolyang einen Vortrag im Extra-Treffen halten. Gruss bu TITEL: Specification Language Z: Overview and Discussion ABSTRACT: The discussion is intended to be a short summary of the one week workshop organized by DST (Deutsche System-Technik) in Kiel. An overview of the language Z will by given through an example. A specification of a lift system will be shown and the schema caulus, the relationship between specification and test classes will be stressed. It is not an "extra Treffen" to learn the language Z. Kolyang From bu Wed Jul 7 17:11:11 1993 Date: Wed, 7 Jul 93 17:11:08 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, tm@p111, jvh, ric, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de Subject: naechstes Treffen Content-Length: 194 Status: RO X-Lines: 8 Liebe Leute, am den kommenden Freitag haben wir noch nix vor; wenn jemand also noch etwas vortragen will oder diskutieren moechte, nur zu !!! Bitte moeglichst bald bei mir melden. gruss bu From bu Tue Aug 3 16:21:09 1993 Date: Tue, 3 Aug 93 16:21:07 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: naechstes treffen Content-Length: 628 Status: RO X-Lines: 14 Liebe Leute, diesen Freitag (6.8.) werde ich zum ueblichen Termin (15 Uhr 15) einen Ueberblicksvortag ueber die Vorlesungen auf der Marktoberdorf - Sommerschule (20.7. - 1.8.93) geben. Themengebiete waren: Lineare Logik (Girard, Scedrow), Programmtransformation durch Beweistransformation (Wainer, Schwichtenberg), Beweis-Reflexion in Nuprl (Constable), Termersetzung (Jouannaud), Beobachtungsorientierte Spezifikationen (Wirsing), Petri-Netze (Brauer), Pi-Calcuel und Action-Structures (Milner), (Wieder mal:) Asynchrone Kommunikation in Prozessnetzen (Broy). Alle Interessierten sind herzlich eingeladen. bu From bu Thu Sep 2 15:40:38 1993 Date: Thu, 2 Sep 93 15:40:33 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: treffen Content-Length: 735 Status: RO X-Lines: 28 Liebe Leute, morgen werde ich um 1 Uhr (Punkt!) bis 14 Uhr 30 einen Vortrag zum Thema: "Eine Deduktionssemantik fuer die Kern-Transformationssprache TL" halten. Diesen Vortrag habe ich diesen Mittwoch in Oldenburg in 110 min. gehalten. Da der Diskussionsbedarf bei uns aber vielleicht groesser ist als dort und wir weniger Zeit haben, kann der Vortrag ggf. in zwei Teile aufgesplittet werden (Der zweite wird dann naechste Woche nachgeholt). Der erste wird dann eher den Schwerpunkt: "Konzepte und Sprachdefinition von TL" der zweite den Schwerpunkt: "Semantische Definition von TL und resultierende Eigenschaften" haben. Der Vortrag berichtet und diskutiert ein Papier, an dem Hui und ich gerade arbeiten. Gruss bu From ewk Fri Sep 3 15:41:40 1993 Date: Fri, 3 Sep 93 15:41:37 +0200 From: ewk (Einar Wolfgang Karlsen) To: bu, shi, qian, tm@p111, jvh, ric, liu, bernd, bkb, hof, ewk, ejs, mfr, herwig, jun, kol, mawe, quin, wu Subject: Visit from Jian Chen, Software Verification Research Center X-Sun-Charset: US-ASCII Content-Length: 1013 Status: RO X-Lines: 33 Dear folks, Jian Chen from the Software Verification Research Center, will make a talk monday, 17.00. Subject enclosed. Einar ---- DEFINING SOFT SORTEDNESS BY ABSTRACT INTERPRETATION Jian Chen Software Verification Research Centre The University of Queensland Brisbane, Australia 4072 ABSTRACT Sorted languages can improve the expressiveness and efficiency of reasoning. A conventional sorted language typically includes well-sortedness rules amongst the rules for well-formedness. A major disadvantage of this approach is that many intuitively meaningful expressions are ill-sorted and hence not part of the language. To overcome this limitation, soft sorting regards as well-formed, all first-order expressions of the corresponding unsorted language, and lets the semantics be the basis for defining the significance of the sort syntax. In this paper we show how soft sortedness can be defined by abstract interpretations which characterise semantic properties of softly sorted expressions. From bu Fri Sep 3 17:01:19 1993 Date: Fri, 3 Sep 93 17:01:16 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: Ankuendigung von zwei Vortraege Content-Length: 253 Status: RO X-Lines: 9 Liebe Leute, Am 6.9.1993, um 17 Uhr tragt Jian Chen vor: "Defining Soft Sortedness by Abstract Interpretation", im Raum 8090. Am 7.9.1993, um 14:30 Uhr tragt L. Zhou vor: "CBD/M- A Heterogeneous Distributed Multimedia DBMS", im Raum 8090. Gruss, Shi From bu Thu Sep 9 14:20:34 1993 Date: Thu, 9 Sep 93 14:20:31 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: treffen Content-Length: 181 Status: RO X-Lines: 11 Liebe Leute, ich wollte noch mal daran erinnern, dass ich morgen, 15 Uhr (ct) den zweiten teil meines Vortrages "Semantik einer Transformations-Kernsprache" halten werde. bu From bu Fri Sep 10 17:04:25 1993 Date: Fri, 10 Sep 93 17:04:23 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: Sondertreffen Content-Length: 232 Status: RO X-Lines: 16 Liebe Leute, diesen Montag, 16 Uhr, traegt Prof. Luo Ruqian ueber: 19th. Int. Conf. of Very Large Data Bases sowie 13th. Int. Joint Conf. of artificial intelligence vor. Alle Interessierten sind herzlich eingeladen. bu From bu Tue Oct 5 17:37:41 1993 Date: Tue, 5 Oct 93 17:37:38 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: Freitag Content-Length: 168 Status: RO X-Lines: 11 Liebe Leute, diesen Freitag, 15.00 ct, wird es zwei Kurzvortraege geben: B. Gersdorf: Monads M. Froehlich: Bericht von der Konferenz "Graph Drawing 93" Gruss bu From bu Mon Oct 11 10:12:15 1993 Date: Mon, 11 Oct 93 10:12:12 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: SONDER-Extratreffen Content-Length: 422 Status: RO X-Lines: 17 Liebe Leute, heute mittag werde ich einen Probevortrag ueber "Synthese-orientierte Transformationen von LEX" halten. Es handelt sich um eine formale Entwicklung der UNIX-LEX-Funktion, die Kolyang, Liu und ich im Rahmen von KORSO gemacht haben. Der Vortrag muss aus Termingruenden um 12 Uhr stattfinden (Punkt) und sollte nicht laenger als eine halbe Stunde dauern. Alle Interessierten sind herzlich eingeladen. From bu Tue Jul 13 11:46:49 1993 Date: Tue, 13 Jul 93 11:46:47 +0200 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: yellow submarine Content-Length: 322 Status: RO X-Lines: 7 Liebe Leute, diesen Freitag um 15.15 wird die Yellow Submarine Gruppe ueber den Stand ihrer Arbeit berichten. Es sieht ganz gut aus, aber verschiedene Dinge werden ganz anders werden als gewohnt. Das Treffen dient dazu, Aenderungen vorzustellen und zu diskutieren. BETROFFEN ist jedenfalls jeder in unserer Gruppe. bu From bu Thu Oct 21 11:37:43 1993 Date: Thu, 21 Oct 93 11:37:41 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: naechstes Treffen Content-Length: 159 Status: RO X-Lines: 13 Liebe Leute, diesen Freitag, 15 uhr (ct) wird B. Gersdorf ueber: Monaden und ihre Anwendungen in funktionalen Programmiersprachen berichten. gruss bu From bu Wed Oct 27 15:05:04 1993 Date: Wed, 27 Oct 93 15:04:59 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, tm@p111, kol@p111 Subject: naechstes treffen Content-Length: 870 Status: RO X-Lines: 17 Liebe Leute, diesen Freitag steht noch kein Gespraechsthema fest. bkb wird nicht dabei sein koennen, aber vielleicht hat einer ja Lust, irgendeines seiner Kinder zur Diskussion zu stellen (hier ist nicht Paul o.ae. gemeint...). Falls nicht, faellt es diese Woche aus. Naechste Woche Freitag, 15 (ct) werden Kolyang und ich einen Vortrag ueber: "Transformationen und Synthese-Theoreme" halten. Es geht dabei um die Tatsache, dass man viele der (vor allem komplexeren) Trafos zerlegen kann in einen "logischen Kern", gen. ein Synthese-Theorem, und "taktischen Zucker". Diese Darstellung wirft ein neues Licht auf Korrektheitsfragen von Trafos, auf Designfragen von Trafo-Regelsaetzen (braucht man wirklich eine "lokale Theorie"?) und systematische Fragen (wie kann man "Split of Postcondition" aus PROSPECTRA mit Smiths "divide & conquer" vergleichen?) gruss bu From bu Tue Nov 9 11:42:11 1993 Date: Tue, 9 Nov 93 11:42:08 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik, kreyss@informatik Subject: naechstes EXTRA-Treffen Content-Length: 647 Status: RO X-Lines: 14 Liebe Leute, diesen Freitag, 15 Uhr, wird auf bkb's und Hr. Herzogs Anregung ein informelles Treffen und Sich-Vorstellen unserer Arbeitsgruppen stattfinden. Von unserer Seite ist geplant, dass vier Themenbereichen unserer Gruppe (Higher-Order Unifikation, Funktional-Logische Sprachen, Transformations-System & Korrekte Software, Visualisierung) KURZ vorgestellt werden. Aehnliches haben die beiden Mitarbeiterinnen Uta Bohnebeck und Jutta Kreyss fuer ihre Fachgebiete (Expertensysteme, Wissensrepraesentation und und Sprachverarbeitung) vor. gruss bu PS: Ute und Carsten Bormann waren auch eingeladen, werden aber nicht kommen koennen. From bu Fri Nov 12 15:05:05 1993 Date: Fri, 12 Nov 93 15:05:02 +0100 From: bu (Burkhart Wolff) To: bu, shi, qian, jvh, ric, wu, liu, bernd, bkb, hof, ewk, ejs, mfr, mawe, wang@pc-labor.uni-Bremen.de, jun, reiner, kol, cabo@bettina, bohnebec@informatik, kreyss@informatik Subject: naechste EXTRA-Vortraege Status: RO Content-Length: 1186 X-Lines: 48 Liebe Leute, fuer den Winter sind folgende Vortraege in unserem Forschungskolloquium ("EXTRA-Treffen", unregelmaessig am Freitag nachmittag 15 (ct), Raum 8090) vorgesehen: 19. 11. Thomas Meyer: Ein l-ordered Evaluator-Generator fuer den Attributierungsformalismus SPEC. Bericht vom Stand einer Diplomarbeit. 26. 11. Bernd Gersdorf: Autom. Typinferenz fuer abhaengige polymorphe Typen ("Term-Polymorphism"). Vortrag und Diskussion. 3. 12. Hui Shi: Extended Pattern Matching in Programm Transformation. Bericht vom Stand der Arbeiten (und eines Papiers). 10. 12. Junbo Liu: Logik Unabhaengigkeit durch Folgerungsrelationen. Promotionsnaher Vortrag und Diskussion. 17. 12. Zhenyu Qian: Funktional-logische Programmierung hoeherer Ordnung. Vortrag und Diskussion. Weihnachtspause. 14.1. 94. Berthold Hoffmann: Berichte von GraGra-Tagungen. 21.1. 94. Stefan Westmeier: Ein Interpreter fuer den PI-Calcuel und seine Anwendung fuer die Modellierung von Interaktiven Systemen. Bericht vom Stand einer Diplomarbeit. In der Zeit vom 30. 11. bis Mitte Januar werde ich nicht an der Uni sein. Organisator des EXTRA-Treffens ist in dieser Zeit Kolyang. bu