I00111 (I00111)
Typetheorie*
< 2006/2007 > 05-02-2007 t/m 01-07-2007 () L
Informatica - Master variant C (2003) Thematische specialisatie Foundations of computer science (6 ec) Keuze informatica (6 ec)
Informatica - Master variant E (2003) Keuze informatica (6 ec)
Informatica - Master variant MT (2003) Thematische specialisatie Foundations of computer science (6 ec) Foundations of computer science (6 ec) Keuze informatica (6 ec) (6 ec) (6 ec)
Informatica - Master variant O (2003) Thematische specialisatie Foundations of computer science (6 ec) Keuze informatica (6 ec)
Informatica - Master variant O (2005) Thematische specialisatie Foundations of computer science (6 ec) Keuze informatica (6 ec)
Informatica - Master na HBO Computer Security variant MT (2003) Keuze informatica (6 ec)
Informatica - Master na HBO Embedded Systems variant MT (2003) Keuze informatica (6 ec)
Informatica - Master na HBO Information Systems variant MT (2003) Keuze informatica (6 ec)
Informatica - Master na HBO Software Construction variant MT (2003) Keuze informatica (6 ec)
omvang
6 ec (168 uur) : 30 uur plenair college, 30 uur groepsgewijs college, 0 uur computerpracticum, 0 uur 'droog' practicum, 0 uur gesprekken met de docent, 0 uur onderling overleg met medestudenten (werkgroepen, projectwerk e.d.), 108 uur zelfstudie
investering
6 ec * 28 u/ec + #std * (1 + 6ec * 0.15 u/student/ec)
inzet tentatief

examinator
afdeling
tijdbesteding

dr. Freek Wiedijk
sws
80u.

speciale web-site
/~milad/courses/TT2007/

 

Lambdatermen hebben nu types, net als (delen van) programma's in programmeertalen. Getypeerde lambda calculi zijn nauw verbonden met functionele talen. Bovendien is er een sterk verband met logica. Dit geeft aanleiding tot 'proof checkers'. We bestuderen en vergelijken verschillende systemen van getypeerde lambda calculi.

Leerdoelen

Algemene bekwaamheden Kunnen omgaan met een aantal typeringssystemen, in het bijzonder voor de lambda-calculus. Het begrijpen van de twee gezichtspunten: de computationele of programmeer-technische interpretatie, en de logische. Specifieke bekwaamheden * Je kent een aantal typeringssystemen, waaronder simpel getypeerde, tweede-orde (polymorfe) en hogere-orde lambda-calculus op syntactisch niveau, zodanig dat je afleidingen van typeringsuitspraken kunt construeren, en in staat bent om de basiseigenschappen m.b.t. type-afleiding en normalisatie toe te passen in redeneringen over die systemen. Je kunt het formalisme van pure typesystemen (PTS) hanteren, en aan de hand van dit beschrijvingsmiddel relaties tussen verschillende typesystemen beschrijven. * Je kent enkele concrete concepten op het gebied van typering in programmeertalen (zoals impliciete/expliciete typering, polymorfie, inductieve/recursieve types, abstracte datatypes en types voor object-georiënteerd programmeren). Je kunt deze modelleren door een geschikt (formeel) typeringsysteem te kiezen. Je kunt eenvoudige concrete constructies vertalen naar het gekozen systeem. * Je kunt het typeringsalgoritme van Milner en het unificatiealgoritme van Robinson hanteren. * Beheersen van de 'propositions-as-types' interpretatie: je kunt uitspraken en bewijzen in enkele eerste- en hogere-orde logica vertalen naar een PTS. * Aangeven hoe getypeerde lambda-calculus gebruikt wordt bij het machinaal verifi"eren van redeneringen. Je bent in staat een niet al te moeilijk wiskundig bewijs volledig te formaliseren met behulp van een interactief bewijssysteem.

Onderwerpen

aaaaaGetypeerde lambda-calculi a la Curry en a la Church. Simpele type theorie, polymorfe type theorie, dependent type theorie. Typeringsalgoritmen. Sterke normalisatie. Representatie van logica's en datatypes in getypeerde lambda calculus. Logical Framework. Hogere orde logica Record Typen Inductieve typen Pure Type systems. Interactieve bewijsconstructie met Coq

Werkvormen

Hoorcollege, werkcollege en computer practicum met Coq

Vereiste voorkennis

* Je dient over enige basiskennis van de (ongetypeerde) lambda-calculus te beschikken. Deze kennis is aanwezig na het volgen van het vak T3: Semantiek en correctheid * Daarnaast is enige ervaring met propositie- en predicatenlogica van belang. * Voor het doorzien van het verband tussen theorie en praktijk komt ervaring met zowel imperatieve als functionele programmeertalen van pas. Die ervaring is aanwezig na het volgen van de Programmeerlijn in de basisopleiding. * Bekendheid met constructieve of intuïtionistische wiskunde (bijvoorbeeld via het vak Intuïtionistische wiskunde van W.H.M. Veldman) is voor de bewijsvariant zeer nuttig maar niet noodzakelijk (zie verderop). * Enige discipline voor het werken met formalismen is gewenst. Doorgaans is die aanwezig na het volgen van de basisopleiding.

Tentaminering

Schriftelijk tentamen en een schriftelijke opdracht

Literatuur

Collegeaantekeningen worden verspreid op het college en via de website.


Evaluatie: studentenquêtes ; geen docentevaluatie bekend Rendement: 10 begonnen, echt meegedaan, geslaagd met 1e kans, geslaagd totaal
Q: