Hauptseminar Programmiersprachentheorie

Hauptstudium Informatik und Mathematik
SS 2007
Di 10-12 Uhr, Oettingenstr. 67, Oe .15
Schein: ja
SWS: 2
Dozenten: Andreas Abel, Lennart Beringer, Hans-Wolfgang Loidl

Aktuelles

  • Am 24.04. keine Seminarsitzung!
  • Es sind noch Plätze frei, Anmeldung bis 24.04. per email möglich.
  • Anmeldung an abel@tcs.ifi..., mit Wunschthema.
  • Erster Termin: Di, 17. April 2007. Der im komm. Vorl. Verz. angegebene Vorbesprechungstermin ist ungültig.
Diskussionsforum die-informatiker.net.

Ausarbeitung

Zur Vorbereitung der Präsentation empfehlen wir folgendes Paper, das kurz und prägnant wichtige Techniken zusammenfasst: "How to give a good research talk," S.L. Peyton Jones, J. Hughes, J. Launchbury. Weitere nützliche Links gibt es hier.

Zeitplan

Datum Referent Thema
17.04. A, H-W, L Vorbesprechung
24.04. entfällt
01.05. Tag der Arbeit
08.05. Hai-Lam Predicate Logic as a Programming Language (Kowalski)
15.05. Andrea Natural Semantics (Kahn)
22.05. A, H-W, L Diskussion zu Präsentationstechniken etc
29.05. Pfingsten
05.06. Frank-André Monads in Functional Programming (Wadler)
12.06. Robert Semantics of Multiple Inheritance (Cardelli)
19.06. Hans-Wolfgang Proof-carrying-code (Necula)
26.06. Lennart Separation Logic (Reynolds)
03.07. Andreas Types for Data Abstraction and Polymorphism (Cardelli, Wegener)

Inhalt

Wenige grundlegende Konzepte bilden die Basis moderner Programmiersprachen. Diese Konzepte sind ausschlaggebend für die Implementierung und Analyse bestehender Programmiersprachen und richtungsweisend für die Entwicklung neuer Programmiertechniken und -sprachen. Im Seminar werden klassische und aktuelle Forschungsarbeiten aus der Grundlagentheorie der Programmiersprachen von den Teilnehmern vorgestellt. Themengebiete umfassen Programmierkonzepte, operationelle Semantik, Typinferenz, Typsysteme für objektorientierte Sprachen, Formalismen für verteilte Systeme, Verifikation und Codezertifizierung.

Literatur

Folgende Arbeiten werden besprochen (Liste vorläufig):

Grundlagen

Betreut von Hans-Wolfgang Loidl.
  • Peter J. Landin. The next 700 programming languages. Communications of the ACM, 9(3):157-166, March 1966.
  • Peter Naur et al. Revised report on the algorithmic language ALGOL 60. Communications of the ACM, 6(1):1-17, January 1963.
    oder
    Niklaus Wirth and C. A. R. Hoare. A contribution to the development of ALGOL. Communications of the ACM, 9(6):413-432, June 1966.

Semantik

Betreut von Andreas Abel
  • Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark, September 1981.
  • Gilles Kahn. Natural semantics. In Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing, editors, Proceedings of the Symposium on Theoretical Aspects of Computer Science (STACS), volume 247 of Lecture Notes in Computer Science, pages 22-39. Springer-Verlag, 1987.
  • Olivier Danvy: A Rational Deconstruction of Landin's SECD Machine. IFL 2004: 52-71

Objekt-orientierte Programmierung

Betreut von Lennart Beringer.
  • O. J. Dahl and K. Nygaard. SIMULA-An ALGOL-based simulation language. Communications of the ACM, 9(9):671-678, September 1966.
  • vergeben and Robert Noll Luca Cardelli. A semantics of multiple inheritance. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Semantics of Data Types, volume 173 of Lecture Notes in Computer Science, pages 51-67. Springer-Verlag, 1984. Full version in Information and Computation, 76(2/3):138-164, 1988.
  • Atsushi Igarashi, Benjamin C. Pierce, Philip Wadler: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Program. Lang. Syst. 23(3): 396-450 (2001)
  • Xavier Leroy: Java Bytecode Verification: Algorithms and Formalizations. J. Autom. Reasoning 30(3-4): 235-269 (2003)

Logik-Programmierung

Betreut von Andreas Abel.
  • vergeben am Hai-Lam Bui: Robert Kowalski. Predicate logic as programming language. In IFIP Congress, pages 569-574, 1974. Reprinted in Computers for Artificial Intelligence Applications, (eds. Wah, B. and Li, G.-J.), IEEE Computer Society Press, Los Angeles, 1986, pp. 68-73.

Funktionale Programmierung

Betreut von Hans-Wolfgang Loidl.
  • Philip Wadler: The Essence of Functional Programming. POPL 1992: 1-14
    Sekundärliteratur dazu:
    Philip Wadler: Monads for Functional Programming. Advanced Functional Programming 1995: 24-52
  • Gérard P. Huet: The Zipper. J. Funct. Program. 7(5): 549-554 (1997)
    und
    Michael Abbott, Thorsten Altenkirch, Conor McBride, Neil Ghani: δ for Data: Differentiating Data Structures. Fundam. Inform. 65(1-2): 1-28 (2005)
  • Lennart Augustsson: Cayenne - A Language with Dependent Types. Advanced Functional Programming 1998: 240-267
  • Ralf Hinze: A New Approach to Generic Functional Programming. POPL 2000: 119-132

Verifikation

Betreut von Lennart Beringer.
  • C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576-580 and 583, October 1969.
    und
    C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39-45, January 1971.
  • John C. Reynolds: Separation Logic: A Logic for Shared Mutable Data Structures. LICS 2002: 55-74
  • George C. Necula. Proof-carrying code. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Paris, France, pages 106-119, January 1997.

Typen

Betreut von Andreas Abel.
  • John C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, Paris, France, volume 19 of Lecture Notes in Computer Science, pages 408-425. Springer-Verlag, 1974.
  • Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, August 1978.
  • Luca Cardelli, Peter Wegner: On Understanding Types, Data Abstraction, and Polymorphism. ACM Comput. Surv. 17(4): 471-522 (1985)

Prozesse und Koinduktion

Betreut von Hans-Wolfgang Loidl
  • C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666-677, August 1978. Reprinted in ``Distributed Computing: Concepts and Implementations'' edited by McEntire, O'Reilly and Larson, IEEE, 1984.
  • Robin Milner, Mads Tofte: Co-Induction in Relational Semantics. Theor. Comput. Sci. 87(1): 209-220 (1991)

Valid HTML 4.01!
Andreas Abel
Last modified: Mon Jul 2 18:45:24 CEST 2007 		Valid CSS!