|
Praktische Semantik von Programmiersprachen (SemProg)7.5 ECTS (englische Bezeichnung: Practical Semantics of Programming Languages)
Modulverantwortliche/r: Tadeusz Litak Lehrende:
Tadeusz Litak
Startsemester: |
SS 2017 | 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: Das Modul ist im Kontext der folgenden Studienfächer/Vertiefungsrichtungen verwendbar:
- Informatik (Bachelor of Science)
(Po-Vers. 2009w | TechFak | Informatik (Bachelor of Science) | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsmodul Theoretische Informatik)
Studien-/Prüfungsleistungen:
Mündliche Prüfung zu Praktische Semantik von Programmiersprachen (Prüfungsnummer: 599478)
- Prüfungsleistung, mehrteilige Prüfung, Dauer (in Minuten): 30, benotet, 7.5 ECTS
- Anteil an der Berechnung der Modulnote: 100.0 %
- weitere Erläuterungen:
In die Prüfungsnote gehen zu 50% die Leistungen aus der Bearbeitung von Übungsaufgaben ein.
- Erstablegung: SS 2017, 1. Wdh.: WS 2017/2018 (nur für Wiederholer)
|
![](/img/anew/void.gif) |
![](/img/anew/void.gif) |
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|