|
Praktische Semantik von Programmiersprachen (SemProg)7.5 ECTS (englische Bezeichnung: Practical Semantics of Programming Languages)
Modulverantwortliche/r: Tadeusz Litak Lehrende:
Tadeusz Litak
Studienfächer/Prüfungsordnungsmodule:
Einfrieren der UnivIS-Modul-Beschreibung: 29.3.2021
Praktische Semantik von Programmiersprachen (112298)
Startsemester: |
SS 2021 | 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:
- Artificial Intelligence (Master of Science)
(Po-Vers. 2021s | TechFak | Artificial Intelligence (Master of Science) | Gesamtkonto | Wahlpflichtmodulbereich | Symbolic Artificial Intelligence | Praktische Semantik von Programmiersprachen)
- Informatik (Bachelor of Arts (2 Fächer))
(Po-Vers. 2010 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Vertiefung Informatik I und II | Vertiefungsmodul Theoretische Informatik | Praktische Semantik von Programmiersprachen)
- Informatik (Bachelor of Arts (2 Fächer))
(Po-Vers. 2013 | TechFak | Informatik (Bachelor of Arts (2 Fächer)) | Vertiefung Informatik I und II | Vertiefungsrichtung Theoretische Informatik | Praktische Semantik von Programmiersprachen)
- Informatik (Bachelor of Science)
(Po-Vers. 2009s | TechFak | Informatik (Bachelor of Science) | Wahlpflichtbereich (5. und 6. Semester) | Wahlpflichtmodule | Vertiefungsrichtung Theoretische Informatik | Praktische Semantik von Programmiersprachen)
- 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)
- Informatik (Master of Science)
(Po-Vers. 2010 | TechFak | Informatik (Master of Science) | Gesamtkonto | Wahlpflichtbereich | Säule der theoretisch orientierten Vertiefungsrichtungen | Vertiefungsrichtung Theoretische Informatik | Praktische Semantik von Programmiersprachen)
- Mathematik (Bachelor of Science)
(Po-Vers. | NatFak | Mathematik (Bachelor of Science) | Module des Nebenfachs | Nebenfach Informatik | Vertiefungsmodule | Vertiefungsrichtung Theoretische Informatik | Praktische Semantik von Programmiersprachen)
- Mathematik (Bachelor of Science)
(Po-Vers. 2019w | NatFak | Mathematik (Bachelor of Science) | weitere Module der Bachelorprüfung | Module des Nebenfachs | Nebenfach Informatik | Vertiefungsmodule | Vertiefungsrichtung Theoretische Informatik | Praktische Semantik von Programmiersprachen)
Studien-/Prüfungsleistungen:
Mündliche Prüfung zu Praktische Semantik von Programmiersprachen (Prüfungsnummer: 599478)
(englischer Titel: Practical Semantics of Programming Languages)
zugeh. "mein campus"-Prüfung: | - 599478 Praktische Semantik von Programmiersprachen (Gewichtung: 100.0 %, Prüfung, Form: mündliche Prüfung, Drittelnoten (mit 4,3), Dauer: -, 7.5 ECTS, Prüfung).
|
- 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 fünf Ü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 2021, 1. Wdh.: WS 2021/2022 (nur für Wiederholer)
1. Prüfer: | Tadeusz Litak (100372) |
|
|
|
|
UnivIS ist ein Produkt der Config eG, Buckenhof |
|
|