195.090 Constructive Reasoning
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2016S, VU, 2.0h, 3.0EC, wird geblockt abgehalten

Merkmale

Semesterwochenstunden: 2.0
ECTS: 3.0
Typ: VU Vorlesung mit Übung

Ziele der Lehrveranstaltung

tbd

Inhalt der Lehrveranstaltung

* intro: constructive existence and examples
* intro: the BHK interpretation of connectives
* Heyting arithmetic: natural deduction calculus
* realisability 1: realisability interpretation of HA
* applications 1: existence and disjunction property, realisability-with-truth
* Heyting arithmetic in higher types: natural deduction
* realisability 2: realisability interpretation of HA^w
* applications 2: extraction of functional programs
* miscellanea, interspersed with the above: double-negation translation, A-translation, conservatively of HA over PA for \forall-\exists formulae, ...

Weitere Informationen

This is a visiting professor course of the Vienna PhD School of Informatics.

It will be held by Prof. Dirk Pattinson / Australian National University.

Vortragende Personen

Tompits, Hans
Pattinson, Dirk

Institut

E195 Zentrum für Koordination & Kommunikation der Fakultät für Informatik

LVA Termine

Tag	Zeit	Datum	Ort	Beschreibung
Mi.	09:00 - 11:00	18.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Fr.	17:00 - 19:00	20.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mo.	16:30 - 18:30	23.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mi.	09:00 - 11:00	25.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mo.	09:00 - 11:00	30.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mi.	10:00 - 12:00	01.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Fr.	17:00 - 19:00	03.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mo.	16:30 - 18:30	06.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mi.	10:00 - 12:00	08.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Fr.	17:00 - 19:00	10.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mo.	17:00 - 19:00	13.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Di.	16:00 - 18:00	14.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mi.	09:00 - 11:00	15.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture

LVA wird geblockt abgehalten

LVA-Anmeldung

Von	Bis	Abmeldung bis
06.04.2016 00:00	17.05.2016 23:59

Anmeldemodalitäten

Please register in TISS.

Curricula

Studienkennzahl	Verbindlichkeit	Semester	Anm.Bed.	Info
PhD Vienna PhD School of Informatics	Keine Angabe

Literatur

Es wird kein Skriptum zur Lehrveranstaltung angeboten.

Vorkenntnisse

Familiarity with predicate logic and basic recursion theory, the latter for the realisability
interpretation of HA over partial recursive functions.

Weitere Informationen

Anwesenheitspflicht!

Sprache

Englisch