Zur Seitennavigation oder mit Tastenkombination für den accesskey-Taste und Taste 1 
Zum Seiteninhalt oder mit Tastenkombination für den accesskey und Taste 2 
Hochschul-Informations-System eG
Startseite    Anmelden    WiSe 2020/21      Umschalten in deutsche Sprache / Switch to english language      Sitemap

Constructive Theory of Computation - Einzelansicht

Zurück
  • Funktionen:
Grunddaten
Veranstaltungsart Weiterführende Vorlesung Langtext
Veranstaltungsnummer 123591 Kurztext
Semester SoSe 2020 SWS
Erwartete Teilnehmer/-innen Max. Teilnehmer/-innen
Turnus Veranstaltungsanmeldung Keine Veranstaltungsbelegung im LSF
Credits
Weitere Links https://courses.ps.uni-saarland.de/ctc_20/
Sprache englisch
Termine Gruppe: iCalendar Export für Outlook
  Tag Zeit Turnus Dauer Raum Raum-
plan
Lehrperson Status Bemerkung fällt aus am Max. Teilnehmer/-innen
Einzeltermine anzeigen
iCalendar Export für Outlook
Di. 16:00 bis 18:00 woch Gebäude E1 3 - Hörsaal III (0.03.1)        
Gruppe :
 
 


Zugeordnete Person
Zugeordnete Person Zuständigkeit
Dudenhefner, Andrej , Dr.
Studiengänge
Abschluss Studiengang Semester Prüfungsversion Kommentar LP BP ECTS
Master (KB) Informatik - 20151 6 6
Bachelor (KB) Medieninformatik - 20131 6 6
Master (KB) Comp.-Komm-Tech - 20071 6 6
LA Sekundarstufe I und II Informatik - 20121 6 6
LA beruf.Schulen Informatik - 20121 6 6
Master (KB) Medieninformatik - 20131 6 6
Bachelor (KB) Informatik - 20151 6 6
Bachelor (KB) Mathematik und Informatik - 20161 6 6
Master (KB) Mathematik und Informatik - 20161 6 6
Master (KB) Embedded Systems - 20161 6 6
Master (KB) Entrep. Cybersecurity - 20181 6 6
Zuordnung zu Einrichtungen
Informatik
Inhalt
Kurzkommentar

This course consists of two parts.
The first part gives an overview over traditional computability theory with the focus on undecidable problems.
The second part introduces a modern, synthetic, approach to computability theory supported by the Coq proof assistant.

Kommentar

One of the most fundamental insights of computer science is the existence of mathematical problems that can be very simply and precisely stated, yet cannot be solved algorithmically.
This insight is part of a larger theory of computability, which is based upon the notion of recursive functions, or alternatively, Turing machines.
Knowing precisely if a function is (algorithmically) computable is valuable.
For example, in programming language design, introducing a new feature without knowing its computablity properties might break compiler termination.

Traditional computability theory relies on Gödel encodings, sometimes obscuring the underlying mathematical structure.
In contrast, synthetic computability theory assumes a mathematical universe in which functions transport computability.
This allows us to forgo Turing machines and focus on the actual mathematical objects, supported by a proof assistant (such as Coq).

Literatur

George S. Boolos, John P. Burgess, and Richard C. Jeffrey. Computability and logic. Cambridge university press, 2002.


Strukturbaum
Keine Einordnung ins Vorlesungsverzeichnis vorhanden. Veranstaltung ist aus dem Semester SoSe 2020 , Aktuelles Semester: WiSe 2020/21