Course Modules
Tait Computability
Tait Computability
Module Completed
Module In Progress
Module Locked
-
External UrlTarski's Theorem Tarski's TheoremScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
External UrlInventing Tait Computability Inventing Tait ComputabilityScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
External UrlTermination for Natural and Unnatural Numbers Termination for Natural and Unnatural NumbersScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
Attachmentweek1.pdf week1.pdfScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Computability of Open Terms
Computability of Open Terms
Module Completed
Module In Progress
Module Locked
-
External UrlKripke Computability Kripke ComputabilityScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
External UrlTait Computability, More Generally Tait Computability, More GenerallyScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
Attachmentweek2.pdf week2.pdfScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Equality for Typed Lambda Calculus
Equality for Typed Lambda Calculus
Module Completed
Module In Progress
Module Locked
-
External UrlSemantic Equality for the Typed Lambda Calculus Semantic Equality for the Typed Lambda CalculusScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
Attachmentweek3.pdf week3.pdfScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Impredicativity
Impredicativity
Module Completed
Module In Progress
Module Locked
-
External UrlGirard's Method Girard's MethodScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Parametricity; Continuations
Parametricity; Continuations
Module Completed
Module In Progress
Module Locked
-
External UrlReynolds' Parametricity Reynolds' ParametricityScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Continuations aka Contradictions
Continuations aka Contradictions
Module Completed
Module In Progress
Module Locked
-
External UrlContinuations aka Contexts aka Contradictions aka staCks Continuations aka Contexts aka Contradictions aka staCksScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
Attachmentweek6.pdf week6.pdfScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Cost and Behavior
Cost and Behavior
Module Completed
Module In Progress
Module Locked
-
External UrlCost Semantics Cost SemanticsScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
Attachmentweek7.pdf week7.pdfScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Call-by-Push-Value aka Polarization
Call-by-Push-Value aka Polarization
Module Completed
Module In Progress
Module Locked
-
External UrlCall-by-Push-Value aka Polarization Call-by-Push-Value aka PolarizationScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Effects: I/O and State
Effects: I/O and State
Module Completed
Module In Progress
Module Locked
-
External UrlEffects in CBPV Effects in CBPVScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Effects: Control and Partiality
Effects: Control and Partiality
Module Completed
Module In Progress
Module Locked
-
External UrlEffects in CBPV Effects in CBPVScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
Attachmentweek10.pdf week10.pdfScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Dependent Types
Dependent Types
Module Completed
Module In Progress
Module Locked
-
External UrlDependent Types Dependent TypesScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
Attachmentweek11.pdf week11.pdfScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Dependent Types
Dependent Types
Module Completed
Module In Progress
Module Locked
-
Context Module Sub Header
(Class cancelled due to illness.)
Score at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Dependent Types
Dependent Types
Module Completed
Module In Progress
Module Locked
-
External UrlDependent Types Dependent TypesScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
Program Modules
Program Modules
Module Completed
Module In Progress
Module Locked
-
External UrlLogical Relations as Types: Proof-Relevant Parametricity for Program Modules Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
-
External UrlAn Equational Logical Framework for Type Theories An Equational Logical Framework for Type TheoriesScore at least Must score at least to complete this module item Scored at least Module item has been completed by scoring at least View Must view in order to complete this module item Viewed Module item has been viewed and is complete Mark done Must mark this module item done in order to complete Marked done Module item marked as done and is complete Contribute Must contribute to this module item to complete it Contributed Contributed to this module item and is complete Submit Must submit this module item to complete it Submitted Module item submitted and is complete
