In die­ser Lehr­ver­an­stal­tung un­ter­su­chen wir fort­ge­schrit­te­ne Kon­zep­te von Pro­gram­mier­spra­chen. Wir wer­den un­ter­schied­li­che Me­tho­den ken­nen­ler­nen die Se­man­tik von Pro­gram­mier­spra­chen zu de­fi­nie­ren (ope­ra­tio­nel­le Se­man­tik, de­no­ta­tio­nel­le Se­man­tik) und for­mal Ei­gen­schaf­ten von Pro­gram­mier­spra­chen zu be­wei­sen. Ein be­son­de­rer Schwer­punkt der Lehr­ver­an­stal­tung ist die De­fi­ni­ti­on und Ana­ly­se von sta­ti­schen Typ­sys­te­men. Das Ziel die­ser Lehr­ver­an­stal­tung ist ein tie­fe­res Ver­ständ­nis von mo­der­nen Pro­gram­mier­spra­chen und eine Vor­be­rei­tung dar­auf, ak­tu­el­le For­schungs­ar­bei­ten in dem Be­reich zu ver­ste­hen.

Do­zen­ten

• Klaus Os­ter­mann
  HeadKlaus Os­ter­mann
• Phil­ipp Schus­ter
  Alum­niPhil­ipp Schus­ter

Klau­sur

Die Klau­sur fin­det am 16.02. von 10.15-11.45 Uhr im ge­wohn­ten Vor­le­sungs­raum C215, Sand 14 statt.

Zeit und Ort

Vor­le­sung: Don­ners­tag, 10 c.t. bis 12 Uhr im Se­mi­nar­raum C215, Sand 14.

Übung: Don­ners­tag, 12 s.t. bis 14 Uhr im Se­mi­nar­raum C215, Sand 14.

Un­ter­la­gen

• SOS Coq Demo
• STLC
• Sub­typ­ing and Sys­tem F
• Type In­fe­rence and Cur­ry-Howard
• Fea­ther­weight Java
• Exis­ten­ti­al Types
• Hig­her-Or­der Types

Haus­auf­ga­ben

• Haus­auf­ga­be 1
• Haus­auf­ga­be 2
• Haus­auf­ga­be 3
• Haus­auf­ga­be 4
• Haus­auf­ga­be 5
• Haus­auf­ga­be 6
• Haus­auf­ga­be 7 Ja­va­Ex­amp­le Has­kel­lEx­amp­le
• Haus­auf­ga­be 8 Ja­va­Ex­amp­le Has­kel­lEx­amp­le
• Haus­auf­ga­be 9
• Haus­auf­ga­be 10 Ja­va­Ex­amp­le Has­kel­lEx­amp­le
• Haus­auf­ga­be 11
• Haus­auf­ga­be 12

Zu­satz­ma­te­ri­al

• Lö­sung 1
• Lö­sung 2
• Lö­sung 4
• Lö­sung 5

Li­te­ra­tur­emp­feh­lung

• B.C. Pier­ce, Types and Pro­gramming Lan­gua­ges, MIT Press
• R. Har­per, Prac­tical Foun­da­ti­ons for Pro­gramming Lan­gua­ges, Cam­bridge Uni­ver­si­ty Press, 2013. Eine kos­ten­lo­se On­line-Aus­ga­be fin­det sich auf der Home­page des Au­tors.