Kursen är centrerad kring interaktiva föreläsningsseminarier och inbjudna seminarier (ungefär 5 föreläsningsseminarier och 1-2 inbjudna seminarier). Under föreläsningsseminarierna kommer både teoretiska och praktiska aspekter diskuteras, med fokus på Coq-bevisassistenten. Under gästseminarierna kommer externa föreläsare presentera olika aspekter av andra bevisassistenter. Den huvudsakliga lärandeaktiviteten är hemövningar där studenten kommer att utföra omfattande teorembevisning. I slutet av kursen kommer varje student genomföra en muntlig presentation där hen reflekterar över sina erfarenheter kring bevisföring, med fokus på hemövningarna.
FID3217 Interaktiv teorembevisning med beroende typer 7,5 hp
I denna kurs kommer du att lära dig grunderna i interaktiv teorembevisning. Fokus är på bevisassistenten Coq och bevisstrategier för grundläggande logik och programspråkssemantik. Kursen är både teoretisk och praktisk. Teoretiskt är bevisassistenten baserad på en sund teori “calculus of inductive constructions”. Fundamentala aspekter som Curry-Howard-korrespondens och beroende typer kommer också att diskuteras. Kursen är också praktisk: alla studenter kommer att arbeta individuellt med en större mängd övningar för att lära sig praktiska aspekter av bevisföring. Vid slutet av kursen kommer studenten att kunna utföra individuell bevisföring med Coq-bevisassistenten generellt och inom området programspråksteori mer specifikt.
Information för forskarstuderande om när kursen ges
VT2024 och sedan efter behov
Om kursomgång
Gäller för kursomgång
VT 2024 Start 2024-03-18 programstuderande
Målgrupp
Ingen information tillagdDel av program
Ingen information tillagdPerioder
P4 (7,5 hp)Varaktighet
2024-03-18
2024-06-03
Studietakt
50%
Undervisningsform
Distans Dagtid
Undervisningsspråk
Engelska
Studielokalisering
KTH Campus
Antal platser
Ingen platsbegränsning
Planerade schemamoduler
Kurs-PM
Kurs-PM är inte publiceratSchema
Schema är inte publiceratKursval
Gäller för kursomgång
VT 2024 Start 2024-03-18 programstuderande
Anmälningskod
61122
Kontakt
Gäller för kursomgång
VT 2024 Start 2024-03-18 programstuderande
Examinator
Ingen information tillagdKursansvarig
Ingen information tillagdLärare
Ingen information tillagdRubriker med innehåll från kursplan FID3217 (VT 2024–) är markerade med en asterisk ( )
Innehåll och lärandemål
Kursupplägg
Kursinnehåll
Kursen innehåller flertalet aspekter av interaktiv teorembevisning med fokus på Coq-bevisassistenten. Kursen innehåller bland annat följande: induktion, beroende typer, Curry-Howard korrespondens, taktiker, polymorfism, induktiva typer, Hoerelogik, småstegsoperationell semantik, typsystem, typkontroll och den enkelt typade lambdakalkylen (STLC). Gästseminarierna kan även innehålla diskussion kring en eller två andra bevisassistenter, så som Isabelle/Isar, Lean, HOL, and Agda.
Lärandemål
Efter kursen kommer studenten kunna:
- Konstruera bevis i Coq relaterat till grundläggande logik
- Tillämpa taktiker i bevisassistenter
- Konstruera bevis i Coq relaterat till programspråkssemantik
- Förklara konceptet beroende typer
- Förklara skillnaden mellan olika sorters bevisassistenter
- Förklara och reflektera kring etiska aspekter av matematik inom datalogi
Kurslitteratur och förberedelser
Särskild behörighet
Inga
Rekommenderade förkunskaper
En kurs i logik och en kurs i programspråkssemantik.
Utrustning
En dator
Kurslitteratur
Den huvudsakliga kurslitteraturen kommer att vara onlineboken “Software Foundations”, som också innehåller teorembevisningsuppgifter. https://softwarefoundations.cis.upenn.edu/.
Examination och slutförande
När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.
Betygsskala
P, F
Examination
- INL1 - Inlämningsuppgift, 7,5 hp, betygsskala: P, F
Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.
Examinator får medge annan examinationsform vid omexamination av enstaka studenter.
Examinationen sker genom hemövningar och en slutlig presentation.
Övriga krav för slutbetyg
Inga
Möjlighet till komplettering
Ingen information tillagd
Möjlighet till plussning
Ingen information tillagd
Examinator
Etiskt förhållningssätt
- Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
- Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
- Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.
Ytterligare information
Kursrum i Canvas
Registrerade studenter hittar information för genomförande av kursen i kursrummet i Canvas. En länk till kursrummet finns under fliken Studier i Personliga menyn vid kursstart.
Ges av
Huvudområde
Denna kurs tillhör inget huvudområde.
Utbildningsnivå
Forskarnivå
Påbyggnad
Ingen information tillagd