195.090 Constructive Reasoning
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2016S, VU, 2.0h, 3.0EC, to be held in blocked form

Properties

Semester hours: 2.0
Credits: 3.0
Type: VU Lecture and Exercise

Aim of course

tbd

Subject of course

* 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, ...

Additional information

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

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

Lecturers

Tompits, Hans
Pattinson, Dirk

Institute

E195 Coordination and Communication Center of the Faculty of Informatics

Course dates

Day	Time	Date	Location	Description
Wed	09:00 - 11:00	18.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Fri	17:00 - 19:00	20.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mon	16:30 - 18:30	23.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Wed	09:00 - 11:00	25.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mon	09:00 - 11:00	30.05.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Wed	10:00 - 12:00	01.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Fri	17:00 - 19:00	03.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mon	16:30 - 18:30	06.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Wed	10:00 - 12:00	08.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Fri	17:00 - 19:00	10.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Mon	17:00 - 19:00	13.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Tue	16:00 - 18:00	14.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture
Wed	09:00 - 11:00	15.06.2016	EI 6 Eckert HS (Gusshausstraße 25-29, staircase 10, 6th floor)	Lecture

Course is held blocked

Course registration

Begin	End	Deregistration end
06.04.2016 00:00	17.05.2016 23:59

Registration modalities

Please register in TISS.

Curricula

Study Code	Obligation	Semester	Precon.	Info
PhD Vienna PhD School of Informatics	Not specified

Literature

No lecture notes are available.

Previous knowledge

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

Miscellaneous

Attendance Required!

Language

English