Courses - 2R840

Laatste wijziging: 22.10.2003

Course: Proving with Computer Assistance

Code: 2R840
Dutch name: Bewijzen met Computer Ondersteuning
ECTS Points: 2.9
For: INF-4.2
Teacher: Dr. R.P. Nederpelt Lazarom. G.I. Jojgov
Questions: Rob Nederpelt: Monday to Wednesday, HG 7.20, tel: 2718, r.p.nederpelt@tue.nl. Georgi Jojgov: HG 7.15, tel: 5004, g.i.jojgov@tue.nl

Doel:

Het doel van dit college is om inzicht te geven in de achtergrond van `theorem provers'. Dit zijn computerprogramma's die bedoeld zijn om te helpen bij het bewijzen van de correctheid van wiskundige stellingen en programmatuur. Theorem provers worden ook gebruikt als interactieve tools voor de ontwikkeling van wiskundige theorieën en correcte programma's.

Studiemateriaal:

Wordt tijdens college uitgereikt.
Zie ook: H.P. Barendregt: Lambda calculi with types. In: S. Abramsky, Dov M. Gabbay, T.S.E. Maibaum: Handbook of Logic in Computer Science, Volume 2, Background: Computational Structures, blz. 118 - 310. Clarendon Press, Oxford, 1992.
Afrekening:
'00/'01: opdracht.
'01/'02 en '02/'03:
(a) Deeltentamen 2R844 over theoriedeel, plus
(b) Opdracht (in overleg).
Eindcijfer is het gemiddelde van de cijfers behaald voor (a) en (b), mits beide voldoende zijn.

Inhoudsbeschrijving:

In een serie colleges wordt eerst de noodzakelijke basiskennis gegeven om de principes achter theorem provers te kunnen begrijpen. Zowel de theoretische achtergrond, bekend onder de naam Type Theory, als de praktische uitvoering in de vorm van tools worden besproken. Er wordt ook ingegaan op bestaande theorem provers als Coq en PVS, waarmee praktische oefeningen worden gedaan.

Week 1: Introductie. Lambda-calculus (typevrij), termen, reductie, confluentie, normalisatie.
Week 2: Types. Impliciete typering. Simpel getypeerde lambda-calculus: lambda-pijl-Church.
Week 3: Eigenschappen van lambda-pijl. Polymorfie. Lambda-2.
Week 4: Pi-types. Lambda-omega-streep.
Week 5: Lambda-P. Predikaten. Logica in lambda-P.
Week 6: Lambda-C. Eigenschappen van lambda-C. De codering van wiskunde in Type Theory: verzamelingen, axioma's, definities, stellingen, bewijzen.
Week 7: Inleiding in het werken met de theorem prover Coq.
Week 8: Oefeningen met Coq (computerpracticum).
Week 9: Inleiding in PVS.