|
| Udgave: |
Efterår 2012 NAT |
| Point: |
7,5 |
| Blokstruktur: |
1. blok |
| Skemagruppe: |
C |
| Fagområde: |
dat |
| Varighed: |
7 weeks of regular coursework + final exam
|
| Institutter: |
Computer Science |
| Studieordning: |
Computer Science Master |
| Uddannelsesdel: |
Kandidat niveau |
| Kontaktpersoner: |
Andrzej Filinski; Phone: 3532 1407; E-mail: andrzej@diku.dk |
| Skema- oplysninger: |
 Vis skema for kurset
Samlet oversigt over tid og sted for alle kurser inden for Lektionsplan for Det Naturvidenskabelige Fakultet Efterår 2012 NAT |
| Undervisnings- form: |
Lectures, mandatory homeworks, exercise sessions. |
| Formål: |
The aim of the course is to introduce students to the fundamental concepts and tools of modern programming-language theory. This includes the relevant descriptive approaches (formal semantics and type systems), their applications to concrete situations, and the mathematical principles for reasoning about them.
The theoretical background covered in the course directly supports reliable program and programming-language development, but also provides a standardized terminology and conceptual framework for communicating effectively with other developers and researchers, including in follow-up coursework and projects within the PLS competence profile.
|
| Indhold: |
Basic principles of deductive systems: judgments and inference rules, structural induction, induction on derivations.
Operational semantics (big-step and small-step) of simple imperative and functional languages; equivalence of programs; equivalence of semantics.
Axiomatic semantics (Hoare logic) of imperative languages; soundness and completeness of program logics.
Type systems for functional languages (simple types and selected extensions); type soundness through preservation and progress; type inference.
Machine-supported reasoning: proof assistants, proof-carrying code
|
| Kompetence- beskrivelse: |
The student will develop competences to analyze and design both individual programs and programming languages, to formulate and prove correctness and safety properties, and to read and write technical accounts of programming-language theory.
|
| Målbeskrivelse: |
At course completion, the student should be able to:
- Read and write specifications of deductive systems (formal judgments defined by inference rules), including in particular operational semantics, type systems, and program logics.
- Decide and prove properties of programs or program fragments, including in particular semantic equivalence and correctness (wrt. a specification) of individual programs.
- Decide and prove properties of entire programming languages, including in particular soundness of type systems and program logics, and equivalence of two semantics.
- Communicate rigorously in writing about the relevant constructions and proofs.
|
| Lærebøger: |
Course notes, selected book chapters and articles |
| Tilmelding: |
Via KUnet from May 15th to June 1st. |
| Faglige forudsætninger: |
Basic knowledge of discrete mathematics (elementary set theory, proofs by induction; e.g. DIKU course DiMS/MatIntro/MoB), compilers (context-free grammars, syntax-directed compilation; e.g., DIKU course OV), and functional programming (familiarity with ML, Haskell, or Scheme; e.g., DIKU course IP/FP) will be expected.
Some exposure to basic formal logic (propositional and first-order logic, natural deduction; e.g., DIKU course Logic/LiCS) is recommended, but not required. |
| Formelle krav: |
None |
| Eksamensform: |
Individual, written take-home exam (32 hours). Internal grading on the 7-point scale. 5 out of 6 homework sets must be satisfactorily completed in order to participate in the final exam. Submission in Absalon.
Re-exam: Written assignment + 30 minutes oral examination without preparation. Internal grading on the 7-point scale. Submission in Absalon.
|
| Eksamen: |
32 timers hjemme opgave udleveres den 6. november kl. 9 og afleveres den 7. november kl. 17.00.
Reeksamen: Genaflevering af opgave den 28. januar og mundtlig prøve den 30. januar 2013.
|
| Kursus hjemmeside: |
 |
| Undervisnings- sprog: |
Kun engelsk
|
| Sidst redigeret: |
25/4-2012 |