Semantyka języków programowania (wykład i ćwiczenia)

Instytut Informatyki UWr
Semestr zimowy 2008/09

Opis przedmiotu

Przedmiot stanowi wprowadzenie do zagadnień związanych z matematycznym opisem semantyki języków programowania, w tym semantyki operacyjnej, denotacyjnej i aksjomatycznej języków imperatywnych, jak również semantyki operacyjnej i denotacyjnej języków funkcyjnych.

Czas i miejsce
  • Wykład: środa 12:15-14:00, sala 140
  • Ćwiczenia: środa 16:15-18:00, sala 141
  • Konsultacje: czwartek 14:30-16:00, pokój 327
Rozkład jazdy

Nr Data Zagadnienia Do poczytania Zadania
1. 08.10.2008 wstęp do wykładu i jego organizacja
modelowy język imperatywny IMP
operacyjna semantyka naturalna (dużych kroków) języka IMP
[NN99]: 1, 2.1
[Kah87]
lista 1
2. 15.10.2008 operacyjna semantyka strukturalna (małych kroków) języka IMP [NN99]: 2.2 - 2.4
[Pit02]: 1.1, 3
lista 2
3. 22.10.2008 modularna semantyka operacyjna
semantyka operacyjna języka IMP w formie maszyny abstrakcyjnej
[NN99]: 3
[Pit02]: 1 - 3
[Mos04]
lista 3
4. 29.10.2008 dobrze ufundowana indukcja
indukcja matematyczna, indukcja strukturalna i indukcja na drzewach wyprowadzeń
definicje przez rekursję strukturalną
definicje indukcyjne i indukcja na regułach wyprowadzenia
[Hen90]: 1.3 - 1.5
[Har08]: 1 - 3
lista 4
5. 05.11.2008 semantyka denotacyjna języka IMP
elementy teorii dziedzin
[NN99]: 4.1 - 4.4
[Gor83]: 2 - 4
lista 5
6. 12.11.2008 obserwacyjna równoważność instrukcji i full abstraction
semantyka kontynuacyjna języka IMP
[NN99]: 4.5
[Gor83]: 5
lista 6
7. 19.11.2008 teoria dziedzin, c.d. (konstrukcje na dziedzinach, konstrukcje funkcji ciągłych, równania dziedzinowe) [Pit99]: 1 - 3
[Plo83]: 1 - 3
[Gor83]: Dodatek
lista 7
8. 26.11.2008 semantyka aksjomatyczna języka IMP (semantyka asercji, reguły Hoare'a, poprawność reguł Hoare'a) [NN99]: 6
[SK95]: 11
lista 8
9. 03.12.2008 względna pełność systemu reguł Hoare'a
warunki weryfikacji
[NN99]: 6
lista 9
10. 10.12.2008 semantyka rekursji (język definicji rekursywnych REC, semantyka operacyjna i denotacyjna języka REC oraz ich równoważność przy ewaluacji przez wartość oraz przez nazwę)
rekursywne definicje lokalne i twierdzenie Bekića
-- lista 10
11. 17.12.2008 indukcja stałopunktowa
semantyka gorliwych języków funkcyjnych z typami wyższymi (semantyka operacyjna i denotacyjna; poprawność semantyki operacyjnej i adekwatność semantyki denotacyjnej; relacje logiczne)
[NN99]: 6.1
[Pit99]: 4
--
12. 14.01.2009
PCF (semantyka operacyjna i denotacyjna; poprawność semantyki operacyjnej i adekwatność semantyki denotacyjnej; full abstraction)
[Pit99]: 5 - 8
[Plo77]
--

Literatura podstawowa
  • [Hen90] Hennessy M., Semantics of Programming Languages, Wiley, 1990
  • [NN99] Nielson H. R., Nielson F., Semantics with Applications: A Formal Introduction, 1999
  • [Pit02] Pitts A., Semantics of Programming Languages, Lecture Notes, University of Cambridge, 2001
  • [Pit99] Pitts A., Denotational Semantics, Lecture Notes, University of Cambridge, 1999
  • [Win93] Winskel G., The Formal Semantics of Programming Languages: An Introduction, MIT Press, 1993
Literatura uzupełniająca
  • [Gor83] Gordon M., Denotacyjny opis języków programowania, WNT, 1983
  • [Gun92] Gunter C., Semantics of Programming Languages: Structures and Techniques, MIT Press, 1992
  • [Har08] Harper R., Practical Foundations for Programming Languages, Working Draft, CMU, 2008
  • [Plo77] Plotkin G. D., LCF Considered as a Programming Language, Theoretical Computer Science , Vol. 5, pp. 223-255, 1977
  • [Plo81] Plotkin G. D., A Structural Approach to Operational Semantics, Lecture Notes, University of Aarhus, 1981
  • [Plo83] Plotkin G. D., Domains, Lecture Notes, University of Edinburgh, 1983
  • [Kah87] Kahn G., Natural semantics, 4th Annual Symposium on Theoretical Aspects of Computer Sciences, 1987
  • [Mos04] Mosses P., Modular Structural Operational Semantics, Journal of Logic and Algebraic Programming, 2004
  • [Rey98] Reynolds J., Theories of Programming Languages, Cambridge University Press, 1998
  • [Sch86] Schmidt D., Denotational Semantics: A Methodology for Language Development, William C. Brown Publishers, 1986
  • [SK95] Slonneger K., Kurtz B., Formal Syntax and Semantics of Programming Languages, Addison-Wesley Publishing Company, 1995
  • [Str06] Streicher T., Domain-Theoretic Foundations of Functional Programming, World Scientific Publishing Corporation, 2006

http://www.ii.uni.wroc.pl/~dabi