|
Praktische Semantik von Programmiersprachen (SemProg)7.5 ECTS (englische Bezeichnung: Practical Semantics of Programming Languages)
(Prüfungsordnungsmodul: Praktische Semantik von Programmiersprachen)
Modulverantwortliche/r: Tadeusz Litak Lehrende:
Tadeusz Litak
Startsemester: |
SS 2020 | Dauer: |
1 Semester | Turnus: |
jährlich (SS) |
Präsenzzeit: |
56 Std. | Eigenstudium: |
169 Std. | Sprache: |
Deutsch und Englisch |
Lehrveranstaltungen:
Inhalt:
We study the foundations of the imperative and functional languages, including semantics and type systems. The special feature of this course is that theory is done in a very practical and hands-on way: we not just prove, but program all the results from first-principles. The basic tool used in the course is Coq proof assistant, which can be regarded as a functional programming language in its own right. It has been used, for example, to verify correctness of Java Card technology, C compilers or, more recently, fragments of x86 architecture.
Lernziele und Kompetenzen:
- Wissen
- The students explain the basics of both programming semantics and proof assistants, in particular Coq.
- Verstehen
- The students prove theorems using a proof assistant.
- Anwenden
- The students transfer proofs into programs and programs into proofs.
- Analysieren
- The students examine behaviour of simple programs using formal semantics
- Evaluieren (Beurteilen)
- The students evaluate the role played by logic and type theory in scientific approach to programming.
- Erschaffen
- The students provide formal semantics to a simple programming language.
Literatur:
Online book "Software Foundations" http://www.cis.upenn.edu/~bcpierce/sf/
Online books by Adam Chlipala: "Certified Programming with Dependent Types" http://adam.chlipala.net/cpdt/ and "Formal Reasoning About Programs" http://adam.chlipala.net/frap/
Supplementary reading on the theory of programming: Types and Programming Languages
Benjamin C. Pierce, The MIT Press
Supplementary reading on Coq: Interactive Theorem Proving and Program Development
Coq'Art: The Calculus of Inductive Constructions
Series: Texts in Theoretical Computer Science. An EATCS Series
Bertot, Yves, Casteran, Pierre
Weitere Informationen:
Schlüsselwörter: Theorembeweisen Semantik Programmiersprachen
www: http://www8.cs.fau.de/course:semprog
Verwendbarkeit des Moduls / Einpassung in den Musterstudienplan:
- Informatik (Bachelor of Science)
(Po-Vers. 2009w | TechFak | Informatik (Bachelor of Science) | Gesamtkonto | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsrichtung Theoretische Informatik | Praktische Semantik von Programmiersprachen)
Dieses Modul ist daneben auch in den Studienfächern "Informatik (Bachelor of Arts (2 Fächer))", "Informatik (Master of Science)", "Mathematik (Bachelor of Science)" verwendbar. Details
Studien-/Prüfungsleistungen:
Mündliche Prüfung zu Praktische Semantik von Programmiersprachen (Prüfungsnummer: 599478)
(englischer Titel: Practical Semantics of Programming Languages)
- Prüfungsleistung, mündliche Prüfung, Dauer (in Minuten): 30, benotet, 7.5 ECTS
- Anteil an der Berechnung der Modulnote: 100.0 %
- weitere Erläuterungen:
Die Modulnote setzt sich zu 50% aus dem Ergebnis einer 30-minütigen mündlichen Prüfung am Semesterende und zu 50% aus der Note für die Bearbeitung von regelmäßig gestellten Übungsaufgaben zusammen.
Gemäß Corona-Satzung wird als alternative Prüfungsform zur mündlichen Prüfung festgelegt: mündliche elektronische/digitale Distanzprüfung mit 30 Minuten Dauer.
- Prüfungssprache: Deutsch und Englisch
- Erstablegung: SS 2020, 1. Wdh.: WS 2020/2021 (nur für Wiederholer)
|
|
|
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|